Abstract
Previously, we have developed a graphical proof strategy language, called PSGraph [4], to support the development and maintenance of large and complex proof tactics for interactive theorem provers. By using labelled hierarchical graphs this formalisation improves upon tactic composition, analysis and maintenance compared with traditional tactic languages. PSGraph has been implemented as the Tinker system, supporting the Isabelle and Proof Power theorem provers [5]. In this paper we present Tinker2, a new version of Tinker, which provides enhancements in user interaction and experience, together with: novel support for controlled inspection; debugging using breakpoints and a logging mechanism; and advanced recording, exporting and reply.
Cite
CITATION STYLE
Lin, Y., Le Bras, P., & Grov, G. (2016). Developing and debugging proof strategies by tinkering. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9636, pp. 573–579). Springer Verlag. https://doi.org/10.1007/978-3-662-49674-9_37
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
