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.:
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:
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.
Rippling provides evidence for such high-level strategy language. Items (from rippling) that we expect to play a major part include: