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



Put YICES_INSTALLED="yes" in your "~/Isabelle2012/etc/settings" file,
and yices will be one of the available solvers when you use the command
"sledgehammer supported_provers" under a theorem. The pertinent thread
is "sledgehammer / yices":

http://www.mail-archive.com/search?q=sledgehammer+%2F+yices&l=isabelle-dev%40mailbroy.informatik.tu-muenchen.de
<http://www.mail-archive.com/search?q=sledgehammer+%2F+yices&l=isabelle-dev%40mailbroy.informatik.tu-muenchen.de>

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

PS: Z3_NON_COMMERCIAL="yes" (in your etc/settings) is also a way to add an additional prover and works out of the box.





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