Email Gateway (Aug 18 2022 at 19:33): Email Gateway (Aug 18 2022 at 19:33):From: John Munroe <munddr@gmail.com>
Hi,
I'm trying out sledgehammer on some very simple lemmas. For instance:
lemma "(1::nat) > (0::nat)"
sledgehammer
All both SPASS and remote_vampire return a proof. However, for
lemma "(1::real) > (0::real)"
sledgehammer
E works fine, but both SPASS and remote_vampire fail. For SPASS, I get
"The ATP problem is unprovable" while remote_vampire gives "An ATP
error occurred". Is there something wrong with my set up or are SPASS
and remote_vampire really this weak?
Thanks
John
Email Gateway (Aug 18 2022 at 19:33):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi John,
This is strange. Perhaps it depends on the theories imported. I just tried
theory Scratch
imports Complex_Main
begin
lemma "(1::real) > (0::real)"
sledgehammer [remote_vampire spass e]
with Isabelle2011-1 (and a recent repository version), and all three provers were quick to find the proof
by (metis zero_less_one)
very quickly. If you want to investigate this further, please send me a complete ".thy" file and Sledgehammer's output with the "debug" option:
sledgehammer [debug]
Regards,
Jasmin
Email Gateway (Aug 18 2022 at 19:33):From: Jean Martina <jean.martina@cl.cam.ac.uk>
In general it does not have anything to do with the qualities of the First Order Prover. It has to do with translations from HOL to FOL. Sometimes you can help sledgehammer with that. In the first case the proof search will use much less translation. I believe in the second case you may be hitting something inherently HOL, thus sledgehammer does not know how to properly translate that.
I had very different experiences by tweaking the options for Sledgehammer. My main problem with it has been the finding of bad proofs that metis was not able to reconstruct. For that, enabling full type translations practically solves the issue.
Anyway, Sledgehammer is good for what it is for.
Jean
Email Gateway (Aug 18 2022 at 19:33):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Since Isabelle2011-1, the default (partially typed) translation scheme is type sound, getting rid of these annoying unreconstructible proofs. (See the manual for details.)
Jasmin
Last updated: Apr 26 2024 at 16:20 UTC