The AI4FM approach

Even though two POs have a similar proof pattern or are of "similar form", it does not necessarily mean that they have the same proof, e.g.:

• different intermediate lemmas are required;
• different instantiations of quantifiers;
• different data structures are used.

Thus, a high-level representation is required in order to capture such variations, and AI4FM's research hypothesis is:

We believe that it is possible (to devise a high-level strategy language for proofs and) to extract strategies from successful proofs that will facilitate automatic proofs of similar POs.

The key to achieving this is classification of the POs - and in AI4FM we envisage several dimensions:

• the data structures;
• the shape of the PO;
• the information from the PO generator;
• the domain of the variables.

These will be analysed separately. Then using the information from the PO shape and PO generator (POG), the proof obligations can be classified into "families".

The expert produces a proof attempt for each "family" - from which a high-level strategy S(?ds) is extracted, with a "hole" ?ds. AI4FM will then automatically discharge all other POs in the same "family", by (for each PO) first instantiating ?ds with data structure information (data_struct) gathered from the particular PO - and then using the strategy to automatically discharge the PO.

Towards a strategy language

Rippling provides evidence for such high-level strategy language. Items (from rippling) that we expect to play a major part include:

• "Standard" proof plans and patches. The expert provided proof attempt will typically exhibit a new plan or a patch to an existing plan. We also aim to capture "dead ends" in proof attempts and expert recovery from them.
• Choices of unusual induction rules and variables. Choice of an alternative induction rule/variable as a patch.
• Intermediate lemmas. We should be able to construct and prove key intermediate lemmas.
• Generalisation. Generalise the original PO as a patch.
• Insert case-analysis.