[isabelle] Sledgehammer oddities



On Fri, 17 Apr 2015, Lars Hupel wrote:

I've attached a small demo theory which exhibits some strange behaviour
when using Sledgehammer on a goal containing a conjunction. I've marked
the problematic statement with (* HERE *).

Steps to reproduce:

1) Go to the blank line between 'defer' and 'sorry'.
2) In the Sledgehammer panel, select provers 'e spass z3 remote_vampire
cvc4' and click 'Apply'.
3) All provers will suggest 'apply simp'.
4) 'apply simp' doesn't solve the first subgoal.

What's even more confusing is that if I invoke sledgehammer via the
command, I get different results for cvc4:

"cvc4": One-line proof reconstruction failed: apply (smt term.collapse(1)).

I've suspected that somehow the 'defer' is at fault here, but even if it
is removed, there's more strange behaviour. In that case, the panel
correctly suggests 'apply auto[1]' (which in fact solves the subgoal),
but the sledgehammer command suggests:

"cvc4": One-line proof reconstruction failed: apply (smt term.collapse(1)).
"remote_vampire": Try this: using term.collapse(1) apply presburger (0.0
ms).

The latter invocation does not solve the subgoal. While I know that
sometimes Sledgehammer suggests an invocation of 'metis' which takes too
long (and might not be able to solve it?), I've never encountered this
with the new (and very helpful) suggestions of 'simp' or 'auto'.

This is still open, as far as I can see. Is there anything to add for the purpose of Isabelle2015 release candidates?


	Makarius





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