[isabelle] sledge-hammer



I tried the example (suggested in the User's Guide to Sledgehammer)
theory Scratch
imports Main
begin
  lemma "[a] = [b] â a = b"

I apply sledgehammer (with the button sledgehammer clicked) with
provers cvc4 remote_vampire z3 spass e
and the button Isar proofs clicked

I have in the output window
"cvc4": Try this: by (metis list.inject ) (28 ms ms) .
Warning : Isar proof construction failed.
"z3" : Try this: by auto (0.0 ms).
(No Isar proof available.)
"spass" : Try this : by (metis list.inject) (16 ms)
(No Isar proof available.)
"remote_vampire : Try this : by (metis list.inject) (8 ms)
(No Isar proof available.)
"e" : Try this: by (metis the_elem_set) (12 ms).
(No Isar proof available.)

What that means ? Is the lemma proved ?
Why there is no Isar proof available ?



-- email : michel.levy at imag.fr
http://membres-liglab.imag.fr/michel.levy



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.