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

Debugging
Inspection
Maintenance
Chemical analysis
User Experience
User Interaction
Formalization
Theorem
Enhancement
Graph in graph theory
Strategy
Language

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
Lin, Yuhui ; Le Bras, Pierre ; Grov, Gudmund. / Developing and Debugging Proof Strategies by Tinkering. Tools and Algorithms for the Construction and Analysis of Systems. editor / Marsha Chechik ; Jean-François Raskin. Springer, 2016. pp. 573-579 (Lecture Notes in Computer Science).
@inproceedings{6085c989c4f04780b50cd7f469e08da3,
title = "Developing and Debugging Proof Strategies by Tinkering",
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.",
author = "Yuhui Lin and {Le Bras}, Pierre and Gudmund Grov",
year = "2016",
doi = "10.1007/978-3-662-49674-9_37",
language = "English",
isbn = "9783662496732",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "573--579",
editor = "Marsha Chechik and Jean-Fran{\cc}ois Raskin",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",

}

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. Lecture Notes in Computer Science, vol. 9636, Springer, pp. 573-579, 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2016, Eindhoven, Netherlands, 2/04/16. https://doi.org/10.1007/978-3-662-49674-9_37

Developing and Debugging Proof Strategies by Tinkering. / Lin, Yuhui; Le Bras, Pierre; Grov, Gudmund.

Tools and Algorithms for the Construction and Analysis of Systems. ed. / Marsha Chechik; Jean-François Raskin. Springer, 2016. p. 573-579 (Lecture Notes in Computer Science; Vol. 9636).

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

TY - GEN

T1 - Developing and Debugging Proof Strategies by Tinkering

AU - Lin, Yuhui

AU - Le Bras, Pierre

AU - Grov, Gudmund

PY - 2016

Y1 - 2016

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84964031036&partnerID=8YFLogxK

U2 - 10.1007/978-3-662-49674-9_37

DO - 10.1007/978-3-662-49674-9_37

M3 - Conference contribution

SN - 9783662496732

T3 - Lecture Notes in Computer Science

SP - 573

EP - 579

BT - Tools and Algorithms for the Construction and Analysis of Systems

A2 - Chechik, Marsha

A2 - Raskin, Jean-François

PB - Springer

ER -

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