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.
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
Here's the downloads that I found on the web:
alt_ergo: http://alt-ergo.lri.fr/, http://why3.lri.fr/
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
I wonder if I really need all three of spass, spass_new, and spass_old,
but I leave them all in.
This archive was generated by a fusion of
Pipermail (Mailman edition) and