Tinker, tailor, solver, proof

Gudmund Grov
(Heriot-Watt University)
Aleks Kissinger
(University of Oxford)
Yuhui Lin
(Heriot-Watt University)

We introduce Tinker, a tool for designing and evaluating proof strategies based on proof-strategy graphs, a formalism previously introduced by the authors. We represent proof strategies as open-graphs, which are directed graphs with additional input/output edges. Tactics appear as nodes in a graph, and can be `piped' together by adding edges between them. Goals are added to the input edges of such a graph, and flow through the graph as the strategy is evaluated. Properties of the edges ensure that only the right `type' of goals are accepted. In this paper, we detail the Tinker tool and show how it can be integrated with two different theorem provers: Isabelle and ProofPower.

In Christoph Benzmüller and Bruno Woltzenlogel Paleo: Proceedings Eleventh Workshop on User Interfaces for Theorem Provers (UITP 2014), Vienna, Austria, 17th July 2014, Electronic Proceedings in Theoretical Computer Science 167, pp. 23–34.
Published: 29th October 2014.

ArXived at: https://dx.doi.org/10.4204/EPTCS.167.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org