The Tinker GUI for graphical proof strategies (tool demo)

Gudmund Grov, Yuhui Lin, Pierre Le Bras

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

Abstract

With the exception of simple proof visualisation (e.g. [5]), we are not familiar with any other graphical proof tools to support theorem provers. While there are tactic languages that support robust tactics (e.g. Ltac [1] for Coq or Eisbach [8] for Isabelle), we believe that the development and debugging features of Tinker are novel. Several features of the tool have been motivated by working with DRisQ (www.drisq.com) in encoding their highly complex Supertac proof strategy in ProofPower [6]. In the future, we would like to improve static checking of PSGraph? for example that all atomic tactics used in the graph exist. We are also interested in investigating (semi) automatic translations from traditional tactic language into PSGraph. This will also include more modern tactic languages, such as Ltac and Eisbach. We also plan to improve the layout algorithm, and develop and implement a better framework for combining evaluation and user edits of PSGraphs.

Original languageEnglish
Title of host publicationProceedings of the Third Workshop on Formal Integrated Development Environment
PublisherOpen Publishing Association
Pages98-101
Number of pages4
DOIs
Publication statusPublished - 27 Jan 2017

Publication series

NameElectronic Proceedings in Theoretical Computer Science
PublisherOpen Publishing Association
Volume240
ISSN (Electronic)2075-2180

Fingerprint

Graphical user interfaces
Visualization

ASJC Scopus subject areas

  • Software

Cite this

Grov, G., Lin, Y., & Le Bras, P. (2017). The Tinker GUI for graphical proof strategies (tool demo). In Proceedings of the Third Workshop on Formal Integrated Development Environment (pp. 98-101). (Electronic Proceedings in Theoretical Computer Science; Vol. 240). Open Publishing Association. https://doi.org/10.4204/EPTCS.240
Grov, Gudmund ; Lin, Yuhui ; Le Bras, Pierre. / The Tinker GUI for graphical proof strategies (tool demo). Proceedings of the Third Workshop on Formal Integrated Development Environment. Open Publishing Association, 2017. pp. 98-101 (Electronic Proceedings in Theoretical Computer Science).
@inproceedings{246a329ebdd74a2f889353d6e00a4a07,
title = "The Tinker GUI for graphical proof strategies (tool demo)",
abstract = "With the exception of simple proof visualisation (e.g. [5]), we are not familiar with any other graphical proof tools to support theorem provers. While there are tactic languages that support robust tactics (e.g. Ltac [1] for Coq or Eisbach [8] for Isabelle), we believe that the development and debugging features of Tinker are novel. Several features of the tool have been motivated by working with DRisQ (www.drisq.com) in encoding their highly complex Supertac proof strategy in ProofPower [6]. In the future, we would like to improve static checking of PSGraph? for example that all atomic tactics used in the graph exist. We are also interested in investigating (semi) automatic translations from traditional tactic language into PSGraph. This will also include more modern tactic languages, such as Ltac and Eisbach. We also plan to improve the layout algorithm, and develop and implement a better framework for combining evaluation and user edits of PSGraphs.",
author = "Gudmund Grov and Yuhui Lin and {Le Bras}, Pierre",
year = "2017",
month = "1",
day = "27",
doi = "10.4204/EPTCS.240",
language = "English",
series = "Electronic Proceedings in Theoretical Computer Science",
publisher = "Open Publishing Association",
pages = "98--101",
booktitle = "Proceedings of the Third Workshop on Formal Integrated Development Environment",
address = "Australia",

}

Grov, G, Lin, Y & Le Bras, P 2017, The Tinker GUI for graphical proof strategies (tool demo). in Proceedings of the Third Workshop on Formal Integrated Development Environment. Electronic Proceedings in Theoretical Computer Science, vol. 240, Open Publishing Association, pp. 98-101. https://doi.org/10.4204/EPTCS.240

The Tinker GUI for graphical proof strategies (tool demo). / Grov, Gudmund; Lin, Yuhui; Le Bras, Pierre.

Proceedings of the Third Workshop on Formal Integrated Development Environment. Open Publishing Association, 2017. p. 98-101 (Electronic Proceedings in Theoretical Computer Science; Vol. 240).

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

TY - GEN

T1 - The Tinker GUI for graphical proof strategies (tool demo)

AU - Grov, Gudmund

AU - Lin, Yuhui

AU - Le Bras, Pierre

PY - 2017/1/27

Y1 - 2017/1/27

N2 - With the exception of simple proof visualisation (e.g. [5]), we are not familiar with any other graphical proof tools to support theorem provers. While there are tactic languages that support robust tactics (e.g. Ltac [1] for Coq or Eisbach [8] for Isabelle), we believe that the development and debugging features of Tinker are novel. Several features of the tool have been motivated by working with DRisQ (www.drisq.com) in encoding their highly complex Supertac proof strategy in ProofPower [6]. In the future, we would like to improve static checking of PSGraph? for example that all atomic tactics used in the graph exist. We are also interested in investigating (semi) automatic translations from traditional tactic language into PSGraph. This will also include more modern tactic languages, such as Ltac and Eisbach. We also plan to improve the layout algorithm, and develop and implement a better framework for combining evaluation and user edits of PSGraphs.

AB - With the exception of simple proof visualisation (e.g. [5]), we are not familiar with any other graphical proof tools to support theorem provers. While there are tactic languages that support robust tactics (e.g. Ltac [1] for Coq or Eisbach [8] for Isabelle), we believe that the development and debugging features of Tinker are novel. Several features of the tool have been motivated by working with DRisQ (www.drisq.com) in encoding their highly complex Supertac proof strategy in ProofPower [6]. In the future, we would like to improve static checking of PSGraph? for example that all atomic tactics used in the graph exist. We are also interested in investigating (semi) automatic translations from traditional tactic language into PSGraph. This will also include more modern tactic languages, such as Ltac and Eisbach. We also plan to improve the layout algorithm, and develop and implement a better framework for combining evaluation and user edits of PSGraphs.

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

U2 - 10.4204/EPTCS.240

DO - 10.4204/EPTCS.240

M3 - Conference contribution

T3 - Electronic Proceedings in Theoretical Computer Science

SP - 98

EP - 101

BT - Proceedings of the Third Workshop on Formal Integrated Development Environment

PB - Open Publishing Association

ER -

Grov G, Lin Y, Le Bras P. The Tinker GUI for graphical proof strategies (tool demo). In Proceedings of the Third Workshop on Formal Integrated Development Environment. Open Publishing Association. 2017. p. 98-101. (Electronic Proceedings in Theoretical Computer Science). https://doi.org/10.4204/EPTCS.240