Projects per year
Abstract
We introduce Tinker, a tool for designing and evaluating proof strategies based on proofstrategy graphs, a formalism previously introduced by the authors. We represent proof strategies as opengraphs, 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.
Original language  English 

Title of host publication  In Proceedings of Eleventh Workshop on User Interfaces for Theorem Provers (UITP 2014) 
Publisher  Open Publishing Association 
Pages  2334 
Number of pages  12 
DOIs  
Publication status  Published  2014 
Publication series
Name  Electronic Proceedings in Theoretical Computer Science 

Publisher  Open Publishing Association 
Volume  167 
ISSN (Print)  20752180 
Fingerprint
Dive into the research topics of 'Tinker, Tailor, Solver, Proof'. Together they form a unique fingerprint.Projects
 1 Finished

A14FM : using A1 to aid automation of proof search in formal methods
Bundy, A., Bundy, A., Grov, G., Ireland, A. & Jones, C. B.
1/04/10 → 31/03/14
Project: Research