822 \item[\labelitemi] \textbf{\textit{alt\_ergo}:} Alt-Ergo is a polymorphic |
822 \item[\labelitemi] \textbf{\textit{alt\_ergo}:} Alt-Ergo is a polymorphic |
823 ATP developed by Bobot et al.\ \cite{alt-ergo}. |
823 ATP developed by Bobot et al.\ \cite{alt-ergo}. |
824 It supports the TPTP polymorphic typed first-order format (TFF1) via Why3 |
824 It supports the TPTP polymorphic typed first-order format (TFF1) via Why3 |
825 \cite{why3}. To use Alt-Ergo, set the environment variable \texttt{WHY3\_HOME} |
825 \cite{why3}. To use Alt-Ergo, set the environment variable \texttt{WHY3\_HOME} |
826 to the directory that contains the \texttt{why3} executable. Sledgehammer has |
826 to the directory that contains the \texttt{why3} executable. Sledgehammer has |
827 been tested with Alt-Ergo 0.95.1 and an unidentified development version of |
827 been tested with Alt-Ergo 0.95.2 and Why3 0.83. |
828 Why3. |
|
829 |
828 |
830 \item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by |
829 \item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by |
831 Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3, |
830 Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3, |
832 set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the |
831 set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the |
833 executable, including the file name, or install the prebuilt CVC3 package from |
832 executable, including the file name, or install the prebuilt CVC3 package from |