TINKER

A Graph Based Proof Strategy Tool

View project onGitHub

PSGraph

Proof-strategy graphs (PSGraphs) is a formalism that represents proof strategies as graphs, where tactics appear on nodes in a graph, and are connected by ‘piping’ them together. To prove a goal in such strategies, the goal is wrapped in a particular graph node, called goal node, and put in one of the input pipes of the graph. The tactic at the end of this pipe, will then consume this goal node, apply the tactic to the goal, and send any (wrapped) sub-goals to the output pipes. Properties of the pipes ensure that only the right ‘type’ of goals are accepted.

Tinker

The Tinker tool, which is a first implementation of PSGraphs. It adopts a generic theorem prover independent framework. We have currently connected it to Isabelle, ProofPower and Rodin. Tinker provides a range of novel features to develop, debug, maintain, record and export hierarchical proof strategies, such as library and hierarchical graphs; richer tactic and debugging options; and recording and replay.

Tinker viz

Tinker allows users to record evaluation/proof steps and then export to a light-weight web application (written in HTML / CSS and JavaScript) via a generated JSON file. A demo of replaying a recorded evaluation is showed as follows. Uers can also try their own recorded evaluation HERE.

Tool demo

Publication

  • Gudmund Grov and Yuhui Lin. The Tinker tool for graphical tactic development. Int J Softw Tools Technol Transfer (2017). doi:10.1007/s10009-017-0452-7. [link][paper resource]

  • Yuhui Lin, Gudmund Grov and Rob Arthan. Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC. In Journal of Formalized Reasoning, Volume 9, No 2 (2016), pages 69-130. [link][paper resource]

  • Gudmund Grov, Yuhui Lin and Pierre Le Bras. ‘The Tinker GUI for graphical proof strategies (tool demo).. In In Proceedings of 3rd Workshop on Formal Integrated Development Environment, Volume 240, pages 98-101. EPTCS, 2016. [link]

  • Yibo Liang, Yuhui Lin and Gudmund Grov. ‘The Tinker’ for Rodin. In 5th International ABZ Conference, ABZ 2016, in Linz, Austria. [paper resources]

  • Yuhui Lin, Pierre Le Bras and Gudmund Grov. Developing & Debugging Proof Strategies by Tinkering. In TACAS 2016, in Eindhoven, The Netherlands. [paper resources] [talk]

  • Yuhui Lin, Gudmund Grov, Colin O’Halloran and Priiya G. ‘A super industrial application of PSGraph. In 5th International ABZ Conference, ABZ 2016, in Linz, Austria.

  • Gudmund Grov, Aleks Kissinger and Yuhui Lin. Tinker, tailor, solver, proof. In User Interfaces for Theorem Provers, UITP 2014, in Vienna, Austria. [talk]

  • Gudmund Grov, Aleks Kissinger and Yuhui Lin. A Graphical Language for Proof Strategies. In Logic for Programming Artificial Intelligence and Reasoning, LPAR-19th, in Stellenbosch, South Africa. [talk]

Talks