ee (Mar 22 2024 at 18:22): ee (Mar 22 2024 at 18:22):How bad is it that I get this error while using sledgehammer to do proofs? Is it a sign that my assumptions are contradictory?
Mathias Fleury (Mar 22 2024 at 19:05):It depends
Mathias Fleury (Mar 22 2024 at 19:10):It can indicate that:
1. the used solver is incorrect (in which case the reconstruction will fail). For example, this:
lemma False (*example from https://github.com/m-fleury/isabelle-emacs/issues/86*)
sledgehammer[spass,debug](Unity_def old.unit.exhaust)
oops
2. Your assumptions are contradictory (which can happen in a proof by contradiction indicating that the solver found a faster way to derive false)
3. There is an issue in Sledgehammer because it fails to understand the proof (for example, Sledgehammer removed accidentally some part of the proofs during parsing)
Mathias Fleury (Mar 22 2024 at 19:12):1 is annoying especially since Sledgehammer does ML it will learn and use the incorrect claim. But it is not bad, it just makes sledgehammer worse
Mathias Fleury (Mar 22 2024 at 19:12):2 is bad (for your formalization)
Mathias Fleury (Mar 22 2024 at 19:13):3 is annoying again, but a correctness problem
Mathias Fleury (Mar 22 2024 at 19:17):Some rule of thumb: take the facts and pass them to sledgehammer:
sledgehammer(the-facts-that-lead-to-false)
If several solvers find a proof: it is very unlikely that it is 1 or 3
Mathias Fleury (Mar 22 2024 at 19:18):and if one solver is (cvc4|verit|z3) and another is (spass|vampire|e|zipperposition) then it is nearly impossible to be 1 or 3
Mathias Fleury (Mar 22 2024 at 19:19):(because the solvers work differently, take a different input format, and produce a different proof format)
ee (Mar 23 2024 at 06:18):Mathias Fleury said:
sledgehammer(the-facts-that-lead-to-false)
Sorry I'm not sure how to do this
Mathias Fleury (Mar 23 2024 at 06:23):In the output of sledgehammer you have something like:
by (metis the-facts-that-lead-to-false) (>1s, time out)
So you insert in your theory:
sledgehammer(the-facts-that-lead-to-false)
Mathias Fleury said:
and if one solver is (cvc4|verit|z3) and another is (spass|vampire|e|zipperposition) then it is nearly impossible to be 1 or 3
this is a very cool heuristic, I've never thought about using sledgehammer in this way!
Last updated: Apr 27 2024 at 20:14 UTC