694 |
693 |
695 \item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by |
694 \item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by |
696 Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3, |
695 Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3, |
697 set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the |
696 set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the |
698 executable, including the file name, or install the prebuilt CVC3 package from |
697 executable, including the file name, or install the prebuilt CVC3 package from |
699 \download. Sledgehammer has been tested with versions 2.2 and 2.4.1. |
698 \download. |
700 |
699 |
701 \item[\labelitemi] \textbf{\textit{cvc4}:} CVC4 \cite{cvc4} is the successor to |
700 \item[\labelitemi] \textbf{\textit{cvc4}:} CVC4 \cite{cvc4} is the successor to |
702 CVC3. To use CVC4, set the environment variable \texttt{CVC4\_SOLVER} to the |
701 CVC3. To use CVC4, set the environment variable \texttt{CVC4\_SOLVER} to the |
703 complete path of the executable, including the file name, or install the |
702 complete path of the executable, including the file name, or install the |
704 prebuilt CVC4 package from \download. Sledgehammer has been tested with version |
703 prebuilt CVC4 package from \download. |
705 1.5-prerelease. |
|
706 |
704 |
707 \item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover |
705 \item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover |
708 developed by Stephan Schulz \cite{schulz-2019}. To use E, set the environment |
706 developed by Stephan Schulz \cite{schulz-2019}. To use E, set the environment |
709 variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof} |
707 variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof} |
710 executable and \texttt{E\_VERSION} to the version number (e.g., ``1.8''), or |
708 executable and \texttt{E\_VERSION} to the version number (e.g., ``1.8''), or |
711 install the prebuilt E package from \download. Sledgehammer has been tested with |
709 install the prebuilt E package from \download. |
712 versions 1.6 to 1.8. |
|
713 |
710 |
714 \item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure |
711 \item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure |
715 instantiation-based prover developed by Konstantin Korovin |
712 instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}. |
716 \cite{korovin-2009}. To use iProver, set the environment variable |
713 To use iProver, set the environment variable \texttt{IPROVER\_HOME} to the |
717 \texttt{IPROVER\_HOME} to the directory that contains the \texttt{iproveropt} |
714 directory that contains the \texttt{iproveropt} executable. iProver depends on |
718 executable. Sledgehammer has been tested with version 2.8. iProver depends on |
715 Vampire to clausify problems, so make sure that Vampire is installed as well. |
719 E to clausify problems, so make sure that E is installed as well. |
|
720 |
716 |
721 \item[\labelitemi] \textbf{\textit{leo2}:} LEO-II is an automatic |
717 \item[\labelitemi] \textbf{\textit{leo2}:} LEO-II is an automatic |
722 higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2}, |
718 higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2}, |
723 with support for the TPTP typed higher-order syntax (TH0). To use LEO-II, set |
719 with support for the TPTP typed higher-order syntax (TH0). To use LEO-II, set |
724 the environment variable \texttt{LEO2\_HOME} to the directory that contains the |
720 the environment variable \texttt{LEO2\_HOME} to the directory that contains the |
725 \texttt{leo} executable. Sledgehammer has been tested with version 1.3.4. |
721 \texttt{leo} executable. |
726 |
722 |
727 \item[\labelitemi] \textbf{\textit{leo3}:} Leo-III is an automatic |
723 \item[\labelitemi] \textbf{\textit{leo3}:} Leo-III is an automatic |
728 higher-order prover developed by Alexander Steen, Max Wisniewski, Christoph |
724 higher-order prover developed by Alexander Steen, Max Wisniewski, Christoph |
729 Benzm\"uller et al.\ \cite{leo3}, |
725 Benzm\"uller et al.\ \cite{leo3}, |
730 with support for the TPTP typed higher-order syntax (TH0). To use Leo-III, set |
726 with support for the TPTP typed higher-order syntax (TH0). To use Leo-III, set |
731 the environment variable \texttt{LEO3\_HOME} to the directory that contains the |
727 the environment variable \texttt{LEO3\_HOME} to the directory that contains the |
732 \texttt{leo3} executable. Sledgehammer has been tested with version 1.1. |
728 \texttt{leo3} executable. |
733 |
729 |
734 \item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic |
730 \item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic |
735 higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with |
731 higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with |
736 support for the TPTP typed higher-order syntax (TH0). To use Satallax, set the |
732 support for the TPTP typed higher-order syntax (TH0). To use Satallax, set the |
737 environment variable \texttt{SATALLAX\_HOME} to the directory that contains the |
733 environment variable \texttt{SATALLAX\_HOME} to the directory that contains the |
738 \texttt{satallax} executable. Sledgehammer has been tested with version 2.2. |
734 \texttt{satallax} executable. |
739 |
735 |
740 \item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution |
736 \item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution |
741 prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}. |
737 prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}. |
742 To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory |
738 To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory |
743 that contains the \texttt{SPASS} executable and \texttt{SPASS\_VERSION} to the |
739 that contains the \texttt{SPASS} executable and \texttt{SPASS\_VERSION} to the |
744 version number (e.g., ``3.8ds''), or install the prebuilt SPASS package from |
740 version number (e.g., ``3.8ds''), or install the prebuilt SPASS package from |
745 \download. Sledgehammer has been tested with version 3.8ds. |
741 \download. |
746 |
742 |
747 \item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order |
743 \item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order |
748 resolution prover developed by Andrei Voronkov and his colleagues |
744 resolution prover developed by Andrei Voronkov and his colleagues |
749 \cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable |
745 \cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable |
750 \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire} |
746 \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire} |
751 executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g., |
747 executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g., |
752 ``4.2.2''). Sledgehammer has been tested with versions 1.8 to 4.2.2 (in the |
748 ``4.2.2''). |
753 post-2010 numbering scheme). |
|
754 |
749 |
755 \item[\labelitemi] \textbf{\textit{verit}:} veriT \cite{bouton-et-al-2009} is an |
750 \item[\labelitemi] \textbf{\textit{verit}:} veriT \cite{bouton-et-al-2009} is an |
756 SMT solver developed by David D\'eharbe, Pascal Fontaine, and their colleagues. |
751 SMT solver developed by David D\'eharbe, Pascal Fontaine, and their colleagues. |
757 It is designed to produce detailed proofs for reconstruction in proof |
752 It is designed to produce detailed proofs for reconstruction in proof |
758 assistants. To use veriT, set the environment variable \texttt{VERIT\_SOLVER} |
753 assistants. To use veriT, set the environment variable \texttt{VERIT\_SOLVER} |
759 to the complete path of the executable, including the file name. Sledgehammer |
754 to the complete path of the executable, including the file name. |
760 has been tested with version 2020.10-rmx. |
|
761 |
755 |
762 \item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at |
756 \item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at |
763 Microsoft Research \cite{de-moura-2008}. To use Z3, set the environment variable |
757 Microsoft Research \cite{de-moura-2008}. To use Z3, set the environment variable |
764 \texttt{Z3\_SOLVER} to the complete path of the executable, including the |
758 \texttt{Z3\_SOLVER} to the complete path of the executable, including the |
765 file name. Sledgehammer has been tested with a pre-release version of 4.4.0. |
759 file name. |
766 |
760 |
767 \item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to |
761 \item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to |
768 be an ATP, exploiting Z3's support for the TPTP typed first-order format (TF0). |
762 be an ATP, exploiting Z3's support for the TPTP typed first-order format (TF0). |
769 It is included for experimental purposes. Sledgehammer has been tested with |
763 It is included for experimental purposes. To use it, set the environment |
770 version 4.3.1. To use it, set the environment variable \texttt{Z3\_TPTP\_HOME} |
764 variable \texttt{Z3\_TPTP\_HOME} to the directory that contains the |
771 to the directory that contains the \texttt{z3\_tptp} executable. |
765 \texttt{z3\_tptp} executable. |
772 |
766 |
773 \item[\labelitemi] \textbf{\textit{zipperposition}:} Zipperposition |
767 \item[\labelitemi] \textbf{\textit{zipperposition}:} Zipperposition |
774 \cite{cruanes-2014} is a higher-order superposition prover developed by Simon |
768 \cite{cruanes-2014} is a higher-order superposition prover developed by Simon |
775 Cruanes, Petar Vukmirovi\'c, and colleagues. To use Zipperposition, set the |
769 Cruanes, Petar Vukmirovi\'c, and colleagues. To use Zipperposition, set the |
776 environment variable \texttt{ZIPPERPOSITION\_HOME} to the directory that |
770 environment variable \texttt{ZIPPERPOSITION\_HOME} to the directory that |
777 contains the \texttt{zipperposition} executable and |
771 contains the \texttt{zipperposition} executable and |
778 \texttt{ZIPPERPOSITION\_VERSION} to the version number (e.g., ``2.0.1''). |
772 \texttt{ZIPPERPOSITION\_VERSION} to the version number (e.g., ``2.0.1''). |
779 Sledgehammer has been tested with version 2.0.1. |
|
780 \end{enum} |
773 \end{enum} |
781 |
774 |
782 \end{sloppy} |
775 \end{sloppy} |
783 |
776 |
784 Moreover, the following remote provers are supported: |
777 Moreover, the following remote provers are supported: |