# HG changeset patch # User blanchet # Date 1412080848 -7200 # Node ID 20aaa307c0ff07336d757e82f45ea886bbffe6ac # Parent 2ba52ecc49960c0156999dbdf71c18a56d0fdc20 updated docs with two provers: veriT and Zipperposition diff -r 2ba52ecc4996 -r 20aaa307c0ff src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Tue Sep 30 14:19:25 2014 +0200 +++ b/src/Doc/Sledgehammer/document/root.tex Tue Sep 30 14:40:48 2014 +0200 @@ -107,11 +107,12 @@ \cite{schulz-2002}, E-SInE \cite{sine}, E-ToFoF \cite{tofof}, iProver \cite{korovin-2009}, iProver-Eq \cite{korovin-sticksel-2010}, LEO-II \cite{leo2}, Satallax \cite{satallax}, SNARK \cite{snark}, SPASS -\cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002}, and -Waldmeister \cite{waldmeister}. The ATPs are run either locally or remotely via -the System\-On\-TPTP web service \cite{sutcliffe-2000}. The supported SMT -solvers are CVC3 \cite{cvc3}, CVC4 \cite{cvc4}, and Z3 \cite{z3}. These are -always run locally. +\cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002}, +Waldmeister \cite{waldmeister}, and Zipperposition \cite{cruanes-2014}. +The ATPs are run either locally or remotely via the System\-On\-TPTP web service +\cite{sutcliffe-2000}. The supported SMT solvers are CVC3 \cite{cvc3}, CVC4 +\cite{cvc4}, veriT \cite{bouton-et-al-2009}, and Z3 \cite{z3}. These are always +run locally. The problem passed to the external provers (or solvers) consists of your current goal together with a heuristic selection of hundreds of facts (theorems) from the @@ -152,12 +153,11 @@ Sledgehammer is part of Isabelle, so you do not need to install it. However, it relies on third-party automatic provers (ATPs and SMT solvers). -Among the ATPs, AgsyHOL, Alt-Ergo, E, LEO-II, Satallax, SPASS, and Vampire can -be run locally; in addition, AgsyHOL, E, E-SInE, E-ToFoF, iProver, iProver-Eq, -LEO-II, Satallax, SNARK, Vampire, and Waldmeister are available remotely via -System\-On\-TPTP \cite{sutcliffe-2000}. If you want better performance, you -should at least install E and SPASS locally. The SMT solvers CVC3, CVC4, and Z3 -can be run locally. +Among the ATPs, AgsyHOL, Alt-Ergo, E, LEO-II, Satallax, SPASS, Vampire, and +Zipperposition can be run locally; in addition, AgsyHOL, E, E-SInE, E-ToFoF, +iProver, iProver-Eq, LEO-II, Satallax, SNARK, Vampire, and Waldmeister are +available remotely via System\-On\-TPTP \cite{sutcliffe-2000}. The SMT solvers +CVC3, CVC4, veriT, and Z3 can be run locally. There are three main ways to install automatic provers on your machine: @@ -212,16 +212,15 @@ \texttt{SATALLAX\_VERSION}, \texttt{SPASS\_VERSION}, or \texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``3.0''). -Similarly, if you want to build CVC3 or CVC4, or found a -Z3 executable somewhere (e.g., \url{http://z3.codeplex.com/}), -set the environment variable \texttt{CVC3\_\allowbreak SOLVER}, -\texttt{CVC4\_\allowbreak SOLVER}, or \texttt{Z3\_SOLVER} to the complete path +Similarly, if you want to install CVC3, CVC4, veriT, or Z3, set the environment +variable \texttt{CVC3\_\allowbreak SOLVER}, \texttt{CVC4\_\allowbreak SOLVER}, +\texttt{VERIT\_\allowbreak SOLVER}, or \texttt{Z3\_SOLVER} to the complete path of the executable, \emph{including the file name}. Sledgehammer has been tested -with CVC3 2.2 and 2.4.1, CVC4 1.2, and Z3 4.3.2. Since Z3's output format is -somewhat unstable, other versions of the solver might not work well with -Sledgehammer. Ideally, also set -\texttt{CVC3\_VERSION}, \texttt{CVC4\_VERSION}, or \texttt{Z3\_NEW\_VERSION} to -the solver's version number (e.g., ``4.3.2''). +with CVC3 2.2 and 2.4.1, CVC4 1.2, veriT smtcomp2014, and Z3 4.3.2. Since Z3's +output format is somewhat unstable, other versions of the solver might not work +well with Sledgehammer. Ideally, also set +\texttt{CVC3\_VERSION}, \texttt{CVC4\_VERSION}, \texttt{VERIT\_VERSION}, or +\texttt{Z3\_NEW\_VERSION} to the solver's version number (e.g., ``4.3.2''). \end{enum} \end{sloppy} @@ -858,6 +857,13 @@ ``3.0''). Sledgehammer has been tested with versions 0.6 to 3.0. Versions strictly above 1.8 support the TPTP typed first-order format (TFF0). +\item[\labelitemi] \textbf{\textit{veriT}:} veriT \cite{bouton-et-al-2009} is an +SMT solver developed by David Déharbe, Pascal Fontaine, and their colleagues. +It is specifically designed to produce detailed proofs for reconstruction in +proof assistants. To use veriT, set the environment variable +\texttt{VERIT\_SOLVER} to the complete path of the executable, including the +file name. Sledgehammer has been tested with version smtcomp2014. + \item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at Microsoft Research \cite{z3}. To use Z3, set the environment variable \texttt{Z3\_NEW\_SOLVER} to the complete path of the executable, including the file @@ -874,6 +880,12 @@ version 4.3.1 of Z3 or above. To use it, set the environment variable \texttt{Z3\_TPTP\_HOME} to the directory that contains the \texttt{z3\_tptp} executable. + +\item[\labelitemi] \textbf{\textit{zipperposition}:} Zipperposition +\cite{cruanes-2014} is an experimental first-order resolution prover developed +by Simon Cruane. To use Zipperposition, set the environment variable +\texttt{ZIPPERPOSITION\_HOME} to the directory that contains the +\texttt{zipperposition} executable. \end{enum} \end{sloppy} diff -r 2ba52ecc4996 -r 20aaa307c0ff src/Doc/manual.bib --- a/src/Doc/manual.bib Tue Sep 30 14:19:25 2014 +0200 +++ b/src/Doc/manual.bib Tue Sep 30 14:40:48 2014 +0200 @@ -389,6 +389,22 @@ pages = "107--121", year=2010} +@inproceedings{bouton-et-al-2009, + author = {Thomas Bouton and + Diego Caminha B. de Oliveira and + David D{\'{e}}harbe and + Pascal Fontaine}, + title = {{veriT}: An Open, Trustable and Efficient {SMT}-Solver}, + year = {2009}, + pages = {151--156}, + editor = {Renate A. Schmidt}, + booktitle = {Automated Deduction --- CADE-22}, + series = {Lecture Notes in Computer Science}, + year = {2009}, + volume = {5663}, + publisher = {Springer} +} + @Article{boyer86, author = {Robert Boyer and Ewing Lusk and William McCune and Ross Overbeek and Mark Stickel and Lawrence Wos}, @@ -517,6 +533,12 @@ publisher = Prentice, year = 1986} +@inproceedings{cruanes-2014, + author = "Simon Cruanes", + title = "Logtk: A {Logic ToolKit} for Automated Reasoning, and its Implementation", + year = 2014, + note = {Presented at the Practical Aspects of Automated Reasoning (PAAR) workshop}} + %D @Book{davey-priestley,