781 \item[\labelitemi] \textbf{\textit{ehoh}:} Ehoh is an experimental version of |
781 \item[\labelitemi] \textbf{\textit{ehoh}:} Ehoh is an experimental version of |
782 E that supports a $\lambda$-free fragment of higher-order logic. Use at your |
782 E that supports a $\lambda$-free fragment of higher-order logic. Use at your |
783 own risks. |
783 own risks. |
784 |
784 |
785 \item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure |
785 \item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure |
786 instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}. |
786 instantiation-based prover developed by Konstantin Korovin |
787 To use iProver, set the environment variable \texttt{IPROVER\_HOME} to the |
787 \cite{korovin-2009}. To use iProver, set the environment variable |
788 directory that contains the \texttt{iprover} and \texttt{vclausify\_rel} |
788 \texttt{IPROVER\_HOME} to the directory that contains the \texttt{iproveropt} |
789 executables. Sledgehammer has been tested with version 0.99. |
789 executable. Sledgehammer has been tested with version 2.8. iProver depends on |
|
790 E to clausify problems, so make sure that E is installed as well. |
790 |
791 |
791 \item[\labelitemi] \textbf{\textit{iprover\_eq}:} iProver-Eq is an |
792 \item[\labelitemi] \textbf{\textit{iprover\_eq}:} iProver-Eq is an |
792 instantiation-based prover with native support for equality developed by |
793 instantiation-based prover with native support for equality developed by |
793 Konstantin Korovin and Christoph Sticksel \cite{korovin-sticksel-2010}. To use |
794 Konstantin Korovin and Christoph Sticksel \cite{korovin-sticksel-2010}. To use |
794 iProver-Eq, set the environment variable \texttt{IPROVER\_EQ\_HOME} to the |
795 iProver-Eq, set the environment variable \texttt{IPROVER\_EQ\_HOME} to the |