Email Gateway (Aug 22 2022 at 15:51): Email Gateway (Aug 22 2022 at 15:51):From: Ian Hayes <Ian.Hayes@itee.uq.edu.au>
Dear Isabelle experts,
I'm getting strange Isabelle behaviour which I've narrowed down to the
following theory.
section {* remote_vampire complains about inconsistent axioms *}
theory Issue
imports Main
begin
lemma "Inf {} = (top::'a::complete_lattice)"
end
When I run sledgehammer on the lemma I get the following output.
Proof found...
"z3": Try this: by simp (0.3 ms)
"cvc4": Try this: by simp (0.3 ms)
"e": Try this: by simp (0.2 ms)
"spass": Try this: by simp (0.3 ms)
"remote_vampire": The prover derived "False", which could be due to
inconsistent axioms (including "sorry"s) or to a bug in Sledgehammer
What I'm concerned about is the response from remote_vampire:
are there inconsistencies in the axioms for a complete lattice,
or a bug in Sledgehammer,
or (what remote_vampire fails to acknowledge) a bug in remote_vampire,
or have I done some obvious stupid error that I can't see for looking?
The lemma in question follows directly from the axiom
Inf_empty [simp]: "⨅{} = ⊤"
i.e. Inf_empty [simp]: Inf {} = top"
in complete_lattice in Complete_Lattices.thy.
Thanks in advance
Ian
Email Gateway (Aug 22 2022 at 15:51):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m getting this all the time (though with the development version). My guess is that the version of Vampire in Miami has been updated.
In the development version, cvc4 also goes wrong.
Larry
Email Gateway (Aug 22 2022 at 15:52):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
On 14 Aug 2017, at 16:36, Lawrence Paulson <lp15@cam.ac.uk> wrote:
I’m getting this all the time (though with the development version). My guess is that the version of Vampire in Miami has been updated.
Indeed, they're now at version 4.2.
In the development version, cvc4 also goes wrong.
I presume this is a reference to the isabelle-dev thread called "cvc4". That thread has exactly two emails in it, the second one of which asks you for details that should be quite simple for you to provide. Until you provide me with those details, or somebody else who has the same issue helps me debug this, there isn't much I can do.
Jasmin
Last updated: Apr 26 2024 at 12:28 UTC