Re: [isabelle] Sledgehammer: "The ATP problem is unprovable"



Hi John,

Am 13.04.2012 um 03:02 schrieb John Munroe:

> I'm trying out sledgehammer on some very simple lemmas. [...] 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?

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






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