Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem



On 7/19/2012 7:58 PM, Christian Sternagel wrote:

Just to clarify: YICES_INSTALLED="yes" alone won't work if the yices binary is not installed and set up correctly (as described in `isabelle doc sledgehammer`), since the standard Isabelle bundle does not include this binary due to licensing issues.

cheers

chris

That's good info because I would have missed that. The auto-provers return lots of errors, and it wasn't apparent to me that yices wasn't installed. I searched the web based on provers that showed up for "sledgehammer supported_provers", but I did my web search before doing my YICES_INSTALLED="yes".

Here's the downloads that I found on the web:

Yices: http://yices.csl.sri.com/download.shtml

Vampire: http://www.vprover.org/

alt_ergo: http://alt-ergo.lri.fr/, http://why3.lri.fr/

leo2: http://www.ags.uni-sb.de/~leo/

satallax: http://www.ps.uni-saarland.de/~cebrown/satallax/

Yices has a Cygwin binary, and it works if I correctly use Cygwin's path naming like /cygdrive/e/.../yices-1.0.35/bin/yices. I wouldn't be able to use it without the binary, since there's no remote yices.

I couldn't get Vampire working on Cygwin last year, and I don't expect better results this year, plus I can't get the file off of their web site. But there's remote_vampire.

The alt_ergo installer got deleted by Norton, plus Why3 has to be installed to use it, so I forget about that one for now.

Leo2 and Satallax don't come with a Cygwin binary, so I forget about them, since I don't try to make anything with Cygwin. But there are remote versions for both of these.

I have them all in now. I count twenty-one of them. I wonder about that dummy_thf. It doesn't ever solve anything. That "dummy" sounds a little suspicious.

I wonder if I really need all three of spass, spass_new, and spass_old, but I leave them all in.

Regards,
GB






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