Email Gateway (Aug 18 2022 at 10:09): Email Gateway (Aug 18 2022 at 10:09):From: Tom Ridge <tjr22@cam.ac.uk>
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
Email Gateway (Aug 18 2022 at 10:09):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Email Gateway (Aug 18 2022 at 10:10):From: Tom Ridge <tjr22@cam.ac.uk>
Dear All,
I received this from Jia, which seems to fit the bill.
Thanks
Tom
Email Gateway (Aug 18 2022 at 10:32):From: Lawrence Paulson <lp15@cam.ac.uk>
This command has recently been renamed to sledgehammer, which is more
evocative.
With recent versions of PG, invoke with Isabelle > Commands >
sledgehammer.
Larry
Email Gateway (Aug 18 2022 at 10:33):From: Till Mossakowski <Till.Mossakowski@dfki.de>
With the following script:
theory Scratch
imports Main
begin
theorem test : "A-->A"
proof -
ProofGeneral.call_atp
I get the follwowing response:
*** Outer syntax error: end of input expected,
*** but long identifier "ProofGeneral.call_atp" was found
I am using Isabelle_May_21_2007.
What goes wrong?
Till Mossakowski
Lawrence Paulson schrieb:
Last updated: May 03 2024 at 12:27 UTC