A graphical strategy language to enable proof re-use

Within interactive theorem proving, and in particular conjectures arising from formal methods, many proofs follows a similar pattern. The ability to re-use expert provided proofs to automatically discharge proof within the same "family" could therefore greatly improve automation of such proofs.

An observation we have made is that in order to capture sufficiently generic strategies, properties from both the goals and the underlying proof techniques (tactics) much be captured, which is not well-supported by current tactic languages.

In this talk we introduce a graph based language to represent such proof strategies. Here, the vertices represent the proof techniques, the edges contains goal properties, and evaluation is achieved by "sending" goals along the edges of the graph between the techniques. We will show some properties of this language and outline how we plan to use it to extract strategies from user provided proofs.