[isabelle] Frst order automation with external provers



Dear All,

Larry Paulson's project to integrate external provers (vampire, E, spass) with Isabelle is in a usable state in the current development versions. In tests, it seems to work pretty well. It's performance far surpasses auto, force, and blast in my opinion (at least for the goals I've looked at).

At the moment, one gives a command, ProofGeneral.call_atp, which returns with the goals that are proved. Unfortunately, this does not progress the proof :(

What would be truly useful (for me, and I presume others) is a way to call the external prover as a tactic, e.g.

apply(vampire add: lemma1 lemma2 ...)

Ideally this should operate on the current goal, not on all goals (i.e. force rather than auto), and use only the lemmas supplied (not all the library lemmas, which is what happens currently- maybe this could be and option to the apply call).

Unfortunately, my understanding of Isabelle is not sufficient to allow me to code this interface myself. But surely there is someone who could do this? I feel it would have significant benefits for the entire community.

Is there someone who could do this?


Thanks

Tom





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