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.
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.
- - Basic Drag and Drawing Editing
- - Supports for Hierarchy
- - PSGraph Library
- - Evaluation and Debugging
- - Breakpoint
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, 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]