Developing and Debugging Proof Strategies by Tinkering

Yuhui Lin; Pierre Le Bras; Gudmund Grov

doi:10.1007/978-3-662-49674-9_37

Developing and Debugging Proof Strategies by Tinkering

Yuhui Lin^*, Pierre Le Bras, Gudmund Grov

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

5 Citations (Scopus)

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 language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems
Editors	Marsha Chechik, Jean-François Raskin
Publisher	Springer
Pages	573-579
Number of pages	7
ISBN (Electronic)	9783662496749
ISBN (Print)	9783662496732
DOIs	https://doi.org/10.1007/978-3-662-49674-9_37
Publication status	Published - 2016
Event	22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2016 - Eindhoven, Netherlands Duration: 2 Apr 2016 → 8 Apr 2016

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	9636
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2016
Abbreviated title	TACAS 2016
Country/Territory	Netherlands
City	Eindhoven
Period	2/04/16 → 8/04/16

ASJC Scopus subject areas

General Computer Science
Theoretical Computer Science

Access to Document

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

Cite this

@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{\c c}ois Raskin",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",

note = "22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2016, TACAS 2016 ; Conference date: 02-04-2016 Through 08-04-2016",

}

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 proceeding › Conference 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

AN - SCOPUS:84964031036

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

T2 - 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2016

Y2 - 2 April 2016 through 8 April 2016

ER -

Developing and Debugging Proof Strategies by Tinkering

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this