The Tinker GUI for graphical proof strategies (tool demo)

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.