[isabelle] Frst order automation with external provers
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and