Developing and Debugging Proof Strategies by Tinkering

Yuhui Lin, Pierre Le Bras, Gudmund Grov

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
EditorsMarsha Chechik, Jean-François Raskin
PublisherSpringer
Pages573-579
Number of pages7
ISBN (Electronic)9783662496749
ISBN (Print)9783662496732
DOIs
Publication statusPublished - 2016
Event22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2016 - Eindhoven, Netherlands
Duration: 2 Apr 20168 Apr 2016

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume9636
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2016
Abbreviated titleTACAS 2016
CountryNetherlands
CityEindhoven
Period2/04/168/04/16

    Fingerprint

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Lin, Y., Le Bras, P., & Grov, G. (2016). Developing and Debugging Proof Strategies by Tinkering. In M. Chechik, & J-F. Raskin (Eds.), Tools and Algorithms for the Construction and Analysis of Systems (pp. 573-579). (Lecture Notes in Computer Science; Vol. 9636). Springer. https://doi.org/10.1007/978-3-662-49674-9_37