100 and satisfiability-modulo-theories (SMT) solvers on the current goal.% |
100 and satisfiability-modulo-theories (SMT) solvers on the current goal.% |
101 \footnote{The distinction between ATPs and SMT solvers is convenient but mostly |
101 \footnote{The distinction between ATPs and SMT solvers is convenient but mostly |
102 historical.} |
102 historical.} |
103 % |
103 % |
104 The supported ATPs are AgsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E |
104 The supported ATPs are AgsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E |
105 \cite{schulz-2002}, E-SInE \cite{sine}, E-ToFoF \cite{tofof}, iProver |
105 \cite{schulz-2002}, E-ToFoF \cite{tofof}, iProver \cite{korovin-2009}, LEO-II |
106 \cite{korovin-2009}, LEO-II \cite{leo2}, Leo-III \cite{leo3}, Satallax |
106 \cite{leo2}, Leo-III \cite{leo3}, Satallax \cite{satallax}, SNARK |
107 \cite{satallax}, SNARK \cite{snark}, SPASS \cite{weidenbach-et-al-2009}, |
107 \cite{snark}, SPASS \cite{weidenbach-et-al-2009}, Vampire |
108 Vampire \cite{riazanov-voronkov-2002}, Waldmeister \cite{waldmeister}, and |
108 \cite{riazanov-voronkov-2002}, Waldmeister \cite{waldmeister}, and |
109 Zipperposition \cite{cruanes-2014}. The ATPs are run either locally or |
109 Zipperposition \cite{cruanes-2014}. The ATPs are run either locally or |
110 remotely via the System\-On\-TPTP web service \cite{sutcliffe-2000}. The |
110 remotely via the System\-On\-TPTP web service \cite{sutcliffe-2000}. The |
111 supported SMT solvers are CVC3 \cite{cvc3}, CVC4 \cite{cvc4}, veriT |
111 supported SMT solvers are CVC3 \cite{cvc3}, CVC4 \cite{cvc4}, veriT |
112 \cite{bouton-et-al-2009}, and Z3 \cite{z3}. These are always run locally. |
112 \cite{bouton-et-al-2009}, and Z3 \cite{z3}. These are always run locally. |
113 |
113 |
145 |
145 |
146 Sledgehammer is part of Isabelle, so you do not need to install it. However, it |
146 Sledgehammer is part of Isabelle, so you do not need to install it. However, it |
147 relies on third-party automatic provers (ATPs and SMT solvers). |
147 relies on third-party automatic provers (ATPs and SMT solvers). |
148 |
148 |
149 Among the ATPs, AgsyHOL, Alt-Ergo, E, LEO-II, Leo-III, Satallax, SPASS, Vampire, and |
149 Among the ATPs, AgsyHOL, Alt-Ergo, E, LEO-II, Leo-III, Satallax, SPASS, Vampire, and |
150 Zipperposition can be run locally; in addition, AgsyHOL, E, E-SInE, E-ToFoF, |
150 Zipperposition can be run locally; in addition, AgsyHOL, E, E-ToFoF, iProver, |
151 iProver, LEO-II, Leo-III, Satallax, SNARK, Vampire, and Waldmeister are |
151 LEO-II, Leo-III, Satallax, SNARK, Vampire, and Waldmeister are available |
152 available remotely via System\-On\-TPTP \cite{sutcliffe-2000}. The SMT solvers |
152 remotely via System\-On\-TPTP \cite{sutcliffe-2000}. The SMT solvers CVC3, |
153 CVC3, CVC4, veriT, and Z3 can be run locally. |
153 CVC4, veriT, and Z3 can be run locally. |
154 |
154 |
155 There are three main ways to install automatic provers on your machine: |
155 There are three main ways to install automatic provers on your machine: |
156 |
156 |
157 \begin{sloppy} |
157 \begin{sloppy} |
158 \begin{enum} |
158 \begin{enum} |
857 AgsyHOL runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. |
857 AgsyHOL runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. |
858 |
858 |
859 \item[\labelitemi] \textbf{\textit{remote\_e}:} The remote version of E runs |
859 \item[\labelitemi] \textbf{\textit{remote\_e}:} The remote version of E runs |
860 on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. |
860 on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. |
861 |
861 |
862 \item[\labelitemi] \textbf{\textit{remote\_e\_sine}:} E-SInE is a metaprover |
|
863 developed by Kry\v stof Hoder \cite{sine} based on E. It runs on Geoff |
|
864 Sutcliffe's Miami servers. |
|
865 |
|
866 \item[\labelitemi] \textbf{\textit{remote\_e\_tofof}:} E-ToFoF is a metaprover |
862 \item[\labelitemi] \textbf{\textit{remote\_e\_tofof}:} E-ToFoF is a metaprover |
867 developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami |
863 developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami |
868 servers. This ATP supports the TPTP typed first-order format (TFF0). The |
864 servers. This ATP supports the TPTP typed first-order format (TFF0). The |
869 remote version of E-ToFoF runs on Geoff Sutcliffe's Miami servers. |
865 remote version of E-ToFoF runs on Geoff Sutcliffe's Miami servers. |
870 |
866 |
895 used to prove universally quantified equations using unconditional equations, |
891 used to prove universally quantified equations using unconditional equations, |
896 corresponding to the TPTP CNF UEQ division. The remote version of Waldmeister |
892 corresponding to the TPTP CNF UEQ division. The remote version of Waldmeister |
897 runs on Geoff Sutcliffe's Miami servers. |
893 runs on Geoff Sutcliffe's Miami servers. |
898 \end{enum} |
894 \end{enum} |
899 |
895 |
900 By default, Sledgehammer runs a subset of CVC4, E, E-SInE, SPASS, Vampire, |
896 By default, Sledgehammer runs a subset of CVC4, E, SPASS, Vampire, veriT, and |
901 veriT, and Z3 in parallel, either locally or remotely---depending on the number |
897 Z3 in parallel, either locally or remotely---depending on the number of |
902 of processor cores available and on which provers are actually installed. It is |
898 processor cores available and on which provers are actually installed. It is |
903 generally a good idea to run several provers in parallel. |
899 generally a good idea to run several provers in parallel. |
904 |
900 |
905 \opnodefault{prover}{string} |
901 \opnodefault{prover}{string} |
906 Alias for \textit{provers}. |
902 Alias for \textit{provers}. |
907 |
903 |