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


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 ( 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
Number of pages4
Publication statusPublished - 27 Jan 2017

Publication series

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

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'The Tinker GUI for graphical proof strategies (tool demo)'. Together they form a unique fingerprint.

Cite this