Pierre Le Bras (with contributions from Gudmund Grov and Yuhui Lin)
Tinker is a tool that implements the proof-strategy graph (PSGraph) formalism. Here, tactics are represented as nodes and are linked with each other with edges. Each tactic will consume goals on input edges and generate new sub-goals which are sent to the output edges. The tool is generic w.r.t. theorem provers, and currently supports Isabelle and ProofPower. Users will use the normal interface provided by the theorem proving system, with the additional support for creating and evaluating proof strategy using Tinker's GUI. Tinker is built on top of Quantomatic.
The first version of the GUI was very limited and highly integrated with the Quantomatic GUI. This document presents a new version of the GUI with several new features; including support for hierarchies and mode guided evaluation. The new version is decoupled further from Quantomatic. It is the outcome of the employment of the first author on EPSRC platform grant EP/J001058/1 over the summer of 2014.