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

Am 13.04.2012 um 14:30 schrieb Jean Martina:

> 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.

Since Isabelle2011-1, the default (partially typed) translation scheme is type sound, getting rid of these annoying unreconstructible proofs. (See the manual for details.)


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