Edinburgh Research Explorer

Developing and Debugging Proof Strategies by Tinkering

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

Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings
PublisherSpringer Berlin Heidelberg
Pages573-579
Number of pages7
ISBN (Electronic)978-3-662-49674-9
ISBN (Print)978-3-662-49673-2
DOIs
Publication statusPublished - 9 Apr 2016
Event22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Eindhoven, Netherlands
Duration: 2 Apr 20168 Apr 2016
https://www.etaps.org/index.php/2016/tacas

Publication series

NameLecture Notes in Computer Science
PublisherSpringer, Berlin, Heidelberg
Volume 9636
ISSN (Print)0302-9743

Conference

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

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.

Download statistics

No data available

ID: 41132941