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/ research/hvg/Isabelle/atp-linkup.html>

Larry


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 MHonArc.