Skip to main content

Research Repository

Advanced Search

Developing and Debugging Proof Strategies by Tinkering

Lin, Yuhui; Le Bras, Pierre; Grov, Gudmund

Authors

Yuhui Lin

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.

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