Towards Automated Proof Strategy Generalisation
This addresses a hard, unsolved problem in automated theorem proving, but the work appears incremental as it builds on existing concepts with a new technique.
The paper tackles the unsolved problem of automatically generalizing interactive proofs to discharge related conjectures by developing goal types to capture key properties of goals, enabling abstractions over sub-goals in tactic composition, and demonstrates the approach with an example.
The ability to automatically generalise (interactive) proofs and use such generalisations to discharge related conjectures is a very hard problem which remains unsolved. Here, we develop a notion of goal types to capture key properties of goals, which enables abstractions over the specific order and number of sub-goals arising when composing tactics. We show that the goal types form a lattice, and utilise this property in the techniques we develop to automatically generalise proof strategies in order to reuse it for proofs of related conjectures. We illustrate our approach with an example.