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. © 2014 Springer International Publishing.
Author supplied keywords
Cite
CITATION STYLE
Hupel, L. (2014). Interactive simplifier tracing and debugging in Isabelle. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8543 LNAI, pp. 328–343). Springer Verlag. https://doi.org/10.1007/978-3-319-08434-3_24
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
