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



In general it does not have anything to do with the qualities of the First Order Prover. It has to do with translations from HOL to FOL. Sometimes you can help sledgehammer with that. In the first case the proof search will use much less translation. I believe in the second case you may be hitting something inherently HOL, thus sledgehammer does not know how to properly translate that.

I had very different experiences by tweaking the options for Sledgehammer. My main problem with it has been the finding of bad proofs that metis was not able to reconstruct. For that, enabling full type translations practically solves the issue.

Anyway, Sledgehammer is good for what it is for. 

Jean
On 12 Apr 2012, at 22:02, John Munroe wrote:

> Hi,
> 
> I'm trying out sledgehammer on some very simple lemmas. For instance:
> 
> lemma "(1::nat) > (0::nat)"
> sledgehammer
> 
> All both SPASS and remote_vampire return a proof. However, 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?
> 
> Thanks
> 
> John
> 






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