Re: [isabelle] Frst order automation with external provers
Thanks for your message. As you know, this work is still in progress,
and the tool only delivers advice. At present, you can use it to find
out which of the 6000+ theorems known to Isabelle are sufficient to
prove your subgoal.
* The most important task (undertaken by Kong Woei Susanto) is to
port Joe Hurd's metis prover to Isabelle. Then the tool will be able
to display an appropriate series of calls to metis, for proving the
subgoal within Isabelle. I hope this will be finished in a month or two.
* We also need a button in Proof General so that users don't have to
type "ProofGeneral.call_atp". I don't know when that will be ready.
* Much other tuning will also be necessary, e.g. for issues like
whether to work on just the first subgoal, or whether to accept hints
from the user about which lemmas to use.
An oracle that simply accepts the output of an automatic theorem
prover would be risky, due to the complexity of the system and the
information loss in the translations. Proof reconstruction catches
any such errors, and also eliminates the need to run expensive ATP
calls repeatedly. Even so, Jia Meng has written oracle-based methods
such as you describe.
We are already working on these things, but there are the CADE
deadlines too, and I don't know how to make things happen any faster.
More details on the linkup are here: <http://www.cl.cam.ac.uk/
On 9 Feb 2007, at 13:11, Tom Ridge wrote:
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