Interactive simplifier tracing and debugging in Isabelle

DOI10.1007/978-3-319-08434-3_24MaRDI QIDQ5495933zbMATH OpenOpenAlexWikidataFDO

Authors Lars Hupel

Publication date 7 August 2014

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1406.0292

zbMATH Keywords

tracingterm rewritingdebuggingIsabellesimplifier

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Abstract: The Isabelle proof assistant comes equipped with a very powerful tactic for term simplification. While tremendously useful, the results of simplifying a term do not always match the user's expectation: sometimes, the resulting term is not in the form the user expected, or the simplifier fails to apply a rule. We describe a new, interactive tracing facility which offers insight into the hierarchical structure of the simplification with user-defined filtering, memoization and search. The new simplifier trace is integrated into the Isabelle/jEdit Prover IDE.

Recommendations

• Interactive theorem proving from the perspective of Isabelle/Isar
• Automatic proof and disproof in Isabelle/HOL
• Term rewriting and beyond -- theorem proving in Isabelle
• The Isabelle Framework
• Asynchronous user interaction and tool integration in Isabelle/PIDE

Cites work

• scientific article; zbMATH DE number 1629953 (Why is no real title available?)
• scientific article; zbMATH DE number 1231537 (Why is no real title available?)
• scientific article; zbMATH DE number 1971503 (Why is no real title available?)
• scientific article; zbMATH DE number 788036 (Why is no real title available?)
• Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit
• Automatic proof and disproof in Isabelle/HOL
• Isabelle/jEdit – A Prover IDE within the PIDE Framework

Cited in

(2)

• Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
• More SPASS with Isabelle

Describes a project that uses

Uses Software

• GDB
• Poly/ML
• iJulienne
• jEdit
• Sledgehammer
• Isabelle/jEdit
• PIDE
• Maude
• Proof General
• Isar
• Isabelle/Isar
• Isabelle

This page was built for publication: Interactive simplifier tracing and debugging in Isabelle

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5495933)