Re: [isabelle] Extracting Goal Information from Proof Terms

On Tue, 12 May 2015, Colin Farquhar wrote:

I?m currently working on something which requires proofs constructed in Isabelle to be translated into Prolog in order to work with a machine learning tool. After some testing I have found that using proof terms is the easiest way to find the structure of a proof and which tactics are being used and in which order, but I also need the details of the goals the tactics are applied to.

Using ?full_prf a? gives me the proof term, while using ?val pterm_a = Proofterm.Proof_of (Proofterm.strip_thm (Thm.proof_body_of @{thm a}))? gives a detailed description. The code I have written already provides a list of tactics in the order they are used, where each nested list contains the tactic(s) applied to the subgoal(s) generated by the previous tactic, eg. here the list would be [impI [conje [conjI [assumption,assumption]]]]. I?m trying to get something similar for goals where each nested list contains the subgoal(s) generated by applying a tactic to the previous goal ( eg. [A /\ B à B /\ A [A /\ B è B /\ A [ A è B è B /\ A [A è B è B, A è B è A]]]] ) which I can then map to the list of tactics to get a list of (tactic, goal) pairs. The problem is, I can?t find a way to extract the details of the subgoals in the middle of the proof. Is this even possible using proof terms in this way? If so, can anyone help me with where I can find the information I?m looking for?

I am not sure if you've got any further in this quest in the meantime.

Proof terms are sometimes useful to see the foundational reasoning going on deep in the bottom of the inference engine, but they are hard to work with productively. For two reasons:

  (1) Proof terms are very expensive for anything but rather small
    applications of Isabelle/HOL.

  (2) Analyzing proof terms is relatively difficult, because most of the
    original resoning structure is lost; in particular, the original
    tactical goal state is no longer there, as you have already noticed.

So we are back to what "proofs constructed in Isabelle to be translated into Prolog" really means. Does it refer to arbitrary proofs found in the wild of actual applications, lets say the Archive of formal Proof? Or does it mean some specific proof examples that you construct yourself?

Moreover, when you say "tactic" above, I guess that you mean "theorem". Is this correct?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.