Yuhui Lin
Developing and Debugging Proof Strategies by Tinkering
Lin, Yuhui; Le Bras, Pierre; Grov, Gudmund
Authors
Pierre Le Bras
Gudmund Grov
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 ProofPower 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.
Citation
Lin, Y., Le Bras, P., & Grov, G. (2016). Developing and Debugging Proof Strategies by Tinkering. In Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2016 (573-579). https://doi.org/10.1007/978-3-662-49674-9_37
Presentation Conference Type | Conference Paper (Published) |
---|---|
Conference Name | 22nd International Conference, TACAS 2016 |
Start Date | Apr 2, 2016 |
End Date | Apr 8, 2016 |
Online Publication Date | Apr 9, 2016 |
Publication Date | 2016 |
Deposit Date | Jul 6, 2022 |
Publisher | Springer |
Pages | 573-579 |
Series Title | Lecture Notes in Computer Science |
Series Number | 9636 |
Book Title | Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2016 |
ISBN | 978-3-662-49673-2 |
DOI | https://doi.org/10.1007/978-3-662-49674-9_37 |
Public URL | http://researchrepository.napier.ac.uk/Output/2884481 |
Downloadable Citations
About Edinburgh Napier Research Repository
Administrator e-mail: repository@napier.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2024
Advanced Search