Interactive Simplifier Tracing and Debugging in Isabelle
Mathematical Software
2014-09-18 v1 Logic in Computer Science
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.
Keywords
Cite
@article{arxiv.1406.0292,
title = {Interactive Simplifier Tracing and Debugging in Isabelle},
author = {Lars Hupel},
journal= {arXiv preprint arXiv:1406.0292},
year = {2014}
}
Comments
Conferences on Intelligent Computer Mathematics, 2014