Tinker, tailor, solver, proof

TL;DR

Tinker is a new tool that uses proof-strategy graphs to design, evaluate, and integrate proof strategies with theorem provers like Isabelle and ProofPower, enhancing proof automation and strategy management.

Contribution

The paper introduces Tinker, a tool for creating and evaluating proof strategies using proof-strategy graphs, and demonstrates its integration with multiple theorem provers.

Findings

Successful implementation of Tinker with Isabelle and ProofPower.

Proof-strategy graphs effectively model and manage proof tactics.

Tinker improves proof strategy design and evaluation processes.

Abstract

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.