diff -r 9fa58cacf95d -r b2c8422833da doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Wed Nov 16 10:09:44 2011 +0100 +++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Nov 16 10:34:08 2011 +0100 @@ -15,6 +15,8 @@ \def\qty#1{\ensuremath{\left<\mathit{#1\/}\right>}} \def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1\/}}\right>}$} +\newcommand\const[1]{\textsf{#1}} + %\oddsidemargin=4.6mm %\evensidemargin=4.6mm %\textwidth=150mm @@ -40,6 +42,10 @@ \begin{document} +%%% TYPESETTING +%\renewcommand\labelitemi{$\bullet$} +\renewcommand\labelitemi{\raise.065ex\hbox{\small\textbullet}} + \selectlanguage{english} \title{\includegraphics[scale=0.5]{isabelle_sledgehammer} \\[4ex] @@ -149,13 +155,13 @@ There are three main ways to install ATPs on your machine: \begin{enum} -\item[$\bullet$] If you installed an official Isabelle package with everything +\item[\labelitemi] If you installed an official Isabelle package with everything inside, it should already include properly setup executables for E and SPASS, ready to use.% \footnote{Vampire's license prevents us from doing the same for this otherwise wonderful tool.} -\item[$\bullet$] Alternatively, you can download the Isabelle-aware E and SPASS +\item[\labelitemi] Alternatively, you can download the Isabelle-aware E and SPASS binary packages from Isabelle's download page. Extract the archives, then add a line to your \texttt{\$ISABELLE\_HOME\_USER/etc/components}% \footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at @@ -172,7 +178,7 @@ in it. -\item[$\bullet$] If you prefer to build E or SPASS yourself, or obtained a +\item[\labelitemi] If you prefer to build E or SPASS yourself, or obtained a Vampire executable from somewhere (e.g., \url{http://www.vprover.org/}), set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof}, @@ -215,7 +221,7 @@ There are two main ways of installing SMT solvers locally. \begin{enum} -\item[$\bullet$] If you installed an official Isabelle package with everything +\item[\labelitemi] If you installed an official Isabelle package with everything inside, it should already include properly setup executables for CVC3 and Z3, ready to use.% \footnote{Yices's license prevents us from doing the same for this otherwise @@ -224,7 +230,7 @@ \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a noncommercial user. -\item[$\bullet$] Otherwise, follow the instructions documented in the \emph{SMT} +\item[\labelitemi] Otherwise, follow the instructions documented in the \emph{SMT} theory (\texttt{\$ISABELLE\_HOME/src/HOL/SMT.thy}). \end{enum} @@ -330,25 +336,25 @@ familiarize themselves with the following options: \begin{enum} -\item[$\bullet$] \textbf{\textit{provers}} (\S\ref{mode-of-operation}) specifies +\item[\labelitemi] \textbf{\textit{provers}} (\S\ref{mode-of-operation}) specifies the automatic provers (ATPs and SMT solvers) that should be run whenever Sledgehammer is invoked (e.g., ``\textit{provers}~= \textit{e spass remote\_vampire}''). For convenience, you can omit ``\textit{provers}~='' and simply write the prover names as a space-separated list (e.g., ``\textit{e spass remote\_vampire}''). -\item[$\bullet$] \textbf{\textit{max\_relevant}} (\S\ref{relevance-filter}) +\item[\labelitemi] \textbf{\textit{max\_relevant}} (\S\ref{relevance-filter}) specifies the maximum number of facts that should be passed to the provers. By default, the value is prover-dependent but varies between about 150 and 1000. If the provers time out, you can try lowering this value to, say, 100 or 50 and see if that helps. -\item[$\bullet$] \textbf{\textit{isar\_proof}} (\S\ref{output-format}) specifies +\item[\labelitemi] \textbf{\textit{isar\_proof}} (\S\ref{output-format}) specifies that Isar proofs should be generated, instead of one-liner \textit{metis} or \textit{smt} proofs. The length of the Isar proofs can be controlled by setting \textit{isar\_shrink\_factor} (\S\ref{output-format}). -\item[$\bullet$] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the +\item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the provers' time limit. It is set to 30 seconds, but since Sledgehammer runs asynchronously you should not hesitate to raise this limit to 60 or 120 seconds if you are the kind of user who can think clearly while ATPs are active. @@ -377,17 +383,17 @@ solutions: \begin{enum} -\item[$\bullet$] Try the \textit{isar\_proof} option (\S\ref{output-format}) to +\item[\labelitemi] Try the \textit{isar\_proof} option (\S\ref{output-format}) to obtain a step-by-step Isar proof where each step is justified by \textit{metis}. Since the steps are fairly small, \textit{metis} is more likely to be able to replay them. -\item[$\bullet$] Try the \textit{smt} proof method instead of \textit{metis}. It +\item[\labelitemi] Try the \textit{smt} proof method instead of \textit{metis}. It is usually stronger, but you need to either have Z3 available to replay the proofs, trust the SMT solver, or use certificates. See the documentation in the \emph{SMT} theory (\texttt{\$ISABELLE\_HOME/src/HOL/SMT.thy}) for details. -\item[$\bullet$] Try the \textit{blast} or \textit{auto} proof methods, passing +\item[\labelitemi] Try the \textit{blast} or \textit{auto} proof methods, passing the necessary facts via \textbf{unfolding}, \textbf{using}, \textit{intro}{:}, \textit{elim}{:}, \textit{dest}{:}, or \textit{simp}{:}, as appropriate. \end{enum} @@ -487,7 +493,7 @@ The \textit{metis}~(\textit{full\_types}) proof method is the fully-typed version of Metis. It is somewhat slower than \textit{metis}, but the proof search is fully typed, and it also includes more powerful rules such as the -axiom ``$x = \mathit{True} \mathrel{\lor} x = \mathit{False}$'' for reasoning in +axiom ``$x = \const{True} \mathrel{\lor} x = \const{False}$'' for reasoning in higher-order places (e.g., in set comprehensions). The method kicks in automatically as a fallback when \textit{metis} fails, and it is sometimes generated by Sledgehammer instead of \textit{metis} if the proof obviously @@ -580,31 +586,31 @@ In the general syntax, the \qty{subcommand} may be any of the following: \begin{enum} -\item[$\bullet$] \textbf{\textit{run} (the default):} Runs Sledgehammer on +\item[\labelitemi] \textbf{\textit{run} (the default):} Runs Sledgehammer on subgoal number \qty{num} (1 by default), with the given options and facts. -\item[$\bullet$] \textbf{\textit{min}:} Attempts to minimize the facts +\item[\labelitemi] \textbf{\textit{min}:} Attempts to minimize the facts specified in the \qty{facts\_override} argument to obtain a simpler proof involving fewer facts. The options and goal number are as for \textit{run}. -\item[$\bullet$] \textbf{\textit{messages}:} Redisplays recent messages issued +\item[\labelitemi] \textbf{\textit{messages}:} Redisplays recent messages issued by Sledgehammer. This allows you to examine results that might have been lost due to Sledgehammer's asynchronous nature. The \qty{num} argument specifies a limit on the number of messages to display (5 by default). -\item[$\bullet$] \textbf{\textit{supported\_provers}:} Prints the list of +\item[\labelitemi] \textbf{\textit{supported\_provers}:} Prints the list of automatic provers supported by Sledgehammer. See \S\ref{installation} and \S\ref{mode-of-operation} for more information on how to install automatic provers. -\item[$\bullet$] \textbf{\textit{running\_provers}:} Prints information about +\item[\labelitemi] \textbf{\textit{running\_provers}:} Prints information about currently running automatic provers, including elapsed runtime and remaining time until timeout. -\item[$\bullet$] \textbf{\textit{kill\_provers}:} Terminates all running +\item[\labelitemi] \textbf{\textit{kill\_provers}:} Terminates all running automatic provers. -\item[$\bullet$] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote +\item[\labelitemi] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}. \end{enum} @@ -686,16 +692,16 @@ The descriptions below refer to the following syntactic quantities: \begin{enum} -\item[$\bullet$] \qtybf{string}: A string. -\item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}. -\item[$\bullet$] \qtybf{smart\_bool\/}: \textit{true}, \textit{false}, or +\item[\labelitemi] \qtybf{string}: A string. +\item[\labelitemi] \qtybf{bool\/}: \textit{true} or \textit{false}. +\item[\labelitemi] \qtybf{smart\_bool\/}: \textit{true}, \textit{false}, or \textit{smart}. -\item[$\bullet$] \qtybf{int\/}: An integer. -%\item[$\bullet$] \qtybf{float\/}: A floating-point number (e.g., 2.5). -\item[$\bullet$] \qtybf{float\_pair\/}: A pair of floating-point numbers +\item[\labelitemi] \qtybf{int\/}: An integer. +%\item[\labelitemi] \qtybf{float\/}: A floating-point number (e.g., 2.5). +\item[\labelitemi] \qtybf{float\_pair\/}: A pair of floating-point numbers (e.g., 0.6 0.95). -\item[$\bullet$] \qtybf{smart\_int\/}: An integer or \textit{smart}. -\item[$\bullet$] \qtybf{float\_or\_none\/}: A floating-point number (e.g., 60 or +\item[\labelitemi] \qtybf{smart\_int\/}: An integer or \textit{smart}. +\item[\labelitemi] \qtybf{float\_or\_none\/}: A floating-point number (e.g., 60 or 0.5) expressing a number of seconds, or the keyword \textit{none} ($\infty$ seconds). \end{enum} @@ -714,68 +720,68 @@ provers are supported: \begin{enum} -\item[$\bullet$] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by +\item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3, set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the executable, including the file name. Sledgehammer has been tested with version 2.2. -\item[$\bullet$] \textbf{\textit{e}:} E is a first-order resolution prover +\item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover developed by Stephan Schulz \cite{schulz-2002}. To use E, set the environment variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof} executable, or install the prebuilt E package from Isabelle's download page. See \S\ref{installation} for details. -\item[$\bullet$] \textbf{\textit{leo2}:} LEO-II is an automatic +\item[\labelitemi] \textbf{\textit{leo2}:} LEO-II is an automatic higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2}, -with support for the TPTP many-typed higher-order syntax (THF0). Sledgehammer +with support for the TPTP typed higher-order syntax (THF0). Sledgehammer requires version 1.2.9 or above. -\item[$\bullet$] \textbf{\textit{metis}:} Although it is much less powerful than +\item[\labelitemi] \textbf{\textit{metis}:} Although it is much less powerful than the external provers, Metis itself can be used for proof search. -\item[$\bullet$] \textbf{\textit{metis\_full\_types}:} Fully typed version of +\item[\labelitemi] \textbf{\textit{metis\_full\_types}:} Fully typed version of Metis, corresponding to \textit{metis} (\textit{full\_types}). -\item[$\bullet$] \textbf{\textit{metis\_no\_types}:} Untyped version of Metis, +\item[\labelitemi] \textbf{\textit{metis\_no\_types}:} Untyped version of Metis, corresponding to \textit{metis} (\textit{no\_types}). -\item[$\bullet$] \textbf{\textit{satallax}:} Satallax is an automatic +\item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with -support for the TPTP many-typed higher-order syntax (THF0). Sledgehammer +support for the TPTP typed higher-order syntax (THF0). Sledgehammer requires version 2.2 or above. -\item[$\bullet$] \textbf{\textit{smt}:} The \textit{smt} proof method with the +\item[\labelitemi] \textbf{\textit{smt}:} The \textit{smt} proof method with the current settings (typically, Z3 with proof reconstruction). -\item[$\bullet$] \textbf{\textit{spass}:} SPASS is a first-order resolution +\item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}. To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory that contains the \texttt{SPASS} executable, or install the prebuilt SPASS package from Isabelle's download page. Sledgehammer requires version 3.5 or above. See \S\ref{installation} for details. -\item[$\bullet$] \textbf{\textit{vampire}:} Vampire is a first-order resolution +\item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order resolution prover developed by Andrei Voronkov and his colleagues \cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire} executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g., ``1.8''). Sledgehammer has been tested with versions 0.6, 1.0, and 1.8. Vampire 1.8 -supports the TPTP many-typed first-order format (TFF0). +supports the TPTP typed first-order format (TFF0). -\item[$\bullet$] \textbf{\textit{yices}:} Yices is an SMT solver developed at +\item[\labelitemi] \textbf{\textit{yices}:} Yices is an SMT solver developed at SRI \cite{yices}. To use Yices, set the environment variable \texttt{YICES\_SOLVER} to the complete path of the executable, including the file name. Sledgehammer has been tested with version 1.0. -\item[$\bullet$] \textbf{\textit{z3}:} Z3 is an SMT solver developed at +\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\_SOLVER} to the complete path of the executable, including the file name, and set \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a noncommercial user. Sledgehammer has been tested with versions 2.7 to 2.18. -\item[$\bullet$] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be -an ATP, exploiting Z3's support for the TPTP untyped and many-typed first-order +\item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be +an ATP, exploiting Z3's support for the TPTP untyped and typed first-order formats (FOF and TFF0). It is included for experimental purposes. It requires version 3.0 or above. \end{enum} @@ -783,28 +789,28 @@ In addition, the following remote provers are supported: \begin{enum} -\item[$\bullet$] \textbf{\textit{remote\_cvc3}:} The remote version of CVC3 runs +\item[\labelitemi] \textbf{\textit{remote\_cvc3}:} The remote version of CVC3 runs on servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to point). -\item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E runs +\item[\labelitemi] \textbf{\textit{remote\_e}:} The remote version of E runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. -\item[$\bullet$] \textbf{\textit{remote\_e\_sine}:} E-SInE is a metaprover +\item[\labelitemi] \textbf{\textit{remote\_e\_sine}:} E-SInE is a metaprover developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of SInE runs on Geoff Sutcliffe's Miami servers. -\item[$\bullet$] \textbf{\textit{remote\_e\_tofof}:} E-ToFoF is a metaprover +\item[\labelitemi] \textbf{\textit{remote\_e\_tofof}:} E-ToFoF is a metaprover developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami -servers. This ATP supports the TPTP many-typed first-order format (TFF0). The +servers. This ATP supports the TPTP typed first-order format (TFF0). The remote version of E-ToFoF runs on Geoff Sutcliffe's Miami servers. -\item[$\bullet$] \textbf{\textit{remote\_iprover}:} iProver is a pure +\item[\labelitemi] \textbf{\textit{remote\_iprover}:} iProver is a pure instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}. The remote version of iProver runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. -\item[$\bullet$] \textbf{\textit{remote\_iprover\_eq}:} iProver-Eq is an +\item[\labelitemi] \textbf{\textit{remote\_iprover\_eq}:} iProver-Eq is an instantiation-based prover with native support for equality developed by Konstantin Korovin and Christoph Sticksel \cite{korovin-sticksel-2010}. The remote version of iProver-Eq runs on Geoff Sutcliffe's Miami servers @@ -813,31 +819,31 @@ The remote version of LEO-II runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. -\item[$\bullet$] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II +\item[\labelitemi] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. -\item[$\bullet$] \textbf{\textit{remote\_satallax}:} The remote version of +\item[\labelitemi] \textbf{\textit{remote\_satallax}:} The remote version of Satallax runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. -\item[$\bullet$] \textbf{\textit{remote\_snark}:} SNARK is a first-order +\item[\labelitemi] \textbf{\textit{remote\_snark}:} SNARK is a first-order resolution prover developed by Stickel et al.\ \cite{snark}. It supports the -TPTP many-typed first-order format (TFF0). The remote version of SNARK runs on +TPTP typed first-order format (TFF0). The remote version of SNARK runs on Geoff Sutcliffe's Miami servers. -\item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of +\item[\labelitemi] \textbf{\textit{remote\_vampire}:} The remote version of Vampire runs on Geoff Sutcliffe's Miami servers. Version 1.8 is used. -\item[$\bullet$] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit +\item[\labelitemi] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit equality prover developed by Hillenbrand et al.\ \cite{waldmeister}. It can be used to prove universally quantified equations using unconditional equations, corresponding to the TPTP CNF UEQ division. The remote version of Waldmeister runs on Geoff Sutcliffe's Miami servers. -\item[$\bullet$] \textbf{\textit{remote\_z3}:} The remote version of Z3 runs on +\item[\labelitemi] \textbf{\textit{remote\_z3}:} The remote version of Z3 runs on servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to point). -\item[$\bullet$] \textbf{\textit{remote\_z3\_tptp}:} The remote version of ``Z3 +\item[\labelitemi] \textbf{\textit{remote\_z3\_tptp}:} The remote version of ``Z3 with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers. \end{enum} @@ -901,7 +907,44 @@ \subsection{Problem Encoding} \label{problem-encoding} +\newcommand\comb[1]{\const{#1}} + \begin{enum} +\opdefault{lam\_trans}{string}{smart} +Specifies the $\lambda$ translation scheme to use in ATP problems. The supported +translation schemes are listed below: + +\begin{enum} +\item[\labelitemi] \textbf{\textit{hide\_lams}:} Hide the $\lambda$-abstractions +by replacing them by unspecified fresh constants, effectively disabling all +reasoning under $\lambda$-abstractions. + +\item[\labelitemi] \textbf{\textit{lam\_lifting}:} Introduce a new +supercombinator \const{c} for each cluster of $n$~$\lambda$-abstractions, +defined using an equation $\const{c}~x_1~\ldots~x_n = t$ ($\lambda$-lifting). + +\item[\labelitemi] \textbf{\textit{combinators}:} Rewrite lambdas to the Curry +combinators (\comb{I}, \comb{K}, \comb{S}, \comb{B}, \comb{C}). Combinators +enable the ATPs to synthesize $\lambda$-terms but tend to yield bulkier formulas +than $\lambda$-lifting: The translation is quadratic in the worst case, and the +equational definitions of the combinators are very prolific in the context of +resolution. + +\item[\labelitemi] \textbf{\textit{hybrid\_lams}:} Introduce a new +supercombinator \const{c} for each cluster of $\lambda$-abstractions and characterize it both using a +lifted equation $\const{c}~x_1~\ldots~x_n = t$ and via Curry combinators. + +\item[\labelitemi] \textbf{\textit{keep\_lams}:} +Keep the $\lambda$-abstractions in the generated problems. This is available +only with provers that support the THF0 syntax. + +\item[\labelitemi] \textbf{\textit{smart}:} The actual translation scheme used +depends on the ATP and should be the most efficient scheme for that ATP. +\end{enum} + +For SMT solvers, the $\lambda$ translation scheme is always +\textit{lam\_lifting}, irrespective of the value of this option. + \opdefault{type\_enc}{string}{smart} Specifies the type encoding to use in ATP problems. Some of the type encodings are unsound, meaning that they can give rise to spurious proofs @@ -909,23 +952,23 @@ listed below, with an indication of their soundness in parentheses: \begin{enum} -\item[$\bullet$] \textbf{\textit{erased} (very unsound):} No type information is +\item[\labelitemi] \textbf{\textit{erased} (very unsound):} No type information is supplied to the ATP. Types are simply erased. -\item[$\bullet$] \textbf{\textit{poly\_guards} (sound):} Types are encoded using +\item[\labelitemi] \textbf{\textit{poly\_guards} (sound):} Types are encoded using a predicate \textit{has\_\allowbreak type\/}$(\tau, t)$ that guards bound variables. Constants are annotated with their types, supplied as additional arguments, to resolve overloading. -\item[$\bullet$] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is -tagged with its type using a function $\mathit{type\/}(\tau, t)$. +\item[\labelitemi] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is +tagged with its type using a function $\const{type\/}(\tau, t)$. -\item[$\bullet$] \textbf{\textit{poly\_args} (unsound):} +\item[\labelitemi] \textbf{\textit{poly\_args} (unsound):} Like for \textit{poly\_guards} constants are annotated with their types to resolve overloading, but otherwise no type information is encoded. This coincides with the default encoding used by the \textit{metis} command. -\item[$\bullet$] +\item[\labelitemi] \textbf{% \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags} (sound); \\ \textit{raw\_mono\_args} (unsound):} \\ @@ -935,7 +978,7 @@ Monomorphization can simplify reasoning but also leads to larger fact bases, which can slow down the ATPs. -\item[$\bullet$] +\item[\labelitemi] \textbf{% \textit{mono\_guards}, \textit{mono\_tags} (sound); \textit{mono\_args} (unsound):} \\ @@ -943,20 +986,20 @@ \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, and \textit{raw\_mono\_args}, respectively but types are mangled in constant names instead of being supplied as ground term arguments. The binary predicate -$\mathit{has\_type\/}(\tau, t)$ becomes a unary predicate -$\mathit{has\_type\_}\tau(t)$, and the binary function -$\mathit{type\/}(\tau, t)$ becomes a unary function -$\mathit{type\_}\tau(t)$. +$\const{has\_type\/}(\tau, t)$ becomes a unary predicate +$\const{has\_type\_}\tau(t)$, and the binary function +$\const{type\/}(\tau, t)$ becomes a unary function +$\const{type\_}\tau(t)$. -\item[$\bullet$] \textbf{\textit{mono\_simple} (sound):} Exploits simple +\item[\labelitemi] \textbf{\textit{mono\_simple} (sound):} Exploits simple first-order types if the prover supports the TFF0 or THF0 syntax; otherwise, falls back on \textit{mono\_guards}. The problem is monomorphized. -\item[$\bullet$] \textbf{\textit{mono\_simple\_higher} (sound):} Exploits simple +\item[\labelitemi] \textbf{\textit{mono\_simple\_higher} (sound):} Exploits simple higher-order types if the prover supports the THF0 syntax; otherwise, falls back on \textit{mono\_simple} or \textit{mono\_guards}. The problem is monomorphized. -\item[$\bullet$] +\item[\labelitemi] \textbf{% \textit{poly\_guards}?, \textit{poly\_tags}?, \textit{raw\_mono\_guards}?, \\ \textit{raw\_mono\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\ @@ -972,7 +1015,7 @@ mark is replaced by a \hbox{``\textit{\_query}''} suffix. If the \emph{sound} option is enabled, these encodings are fully sound. -\item[$\bullet$] +\item[\labelitemi] \textbf{% \textit{poly\_guards}??, \textit{poly\_tags}??, \textit{raw\_mono\_guards}??, \\ \textit{raw\_mono\_tags}??, \textit{mono\_guards}??, \textit{mono\_tags}?? \\ @@ -981,7 +1024,7 @@ \textit{metis} proof method, the `\hbox{??}' suffix is replaced by \hbox{``\textit{\_query\_query}''}. -\item[$\bullet$] +\item[\labelitemi] \textbf{% \textit{poly\_guards}@?, \textit{poly\_tags}@?, \textit{raw\_mono\_guards}@?, \\ \textit{raw\_mono\_tags}@? (quasi-sound):} \\ @@ -989,7 +1032,7 @@ \textit{metis} proof method, the `\hbox{@?}' suffix is replaced by \hbox{``\textit{\_at\_query}''}. -\item[$\bullet$] +\item[\labelitemi] \textbf{% \textit{poly\_guards}!, \textit{poly\_tags}!, \textit{raw\_mono\_guards}!, \\ \textit{raw\_mono\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \\ @@ -1005,7 +1048,7 @@ \textit{metis} proof method, the exclamation mark is replaced by the suffix \hbox{``\textit{\_bang}''}. -\item[$\bullet$] +\item[\labelitemi] \textbf{% \textit{poly\_guards}!!, \textit{poly\_tags}!!, \textit{raw\_mono\_guards}!!, \\ \textit{raw\_mono\_tags}!!, \textit{mono\_guards}!!, \textit{mono\_tags}!! \\ @@ -1014,7 +1057,7 @@ \textit{metis} proof method, the `\hbox{!!}' suffix is replaced by \hbox{``\textit{\_bang\_bang}''}. -\item[$\bullet$] +\item[\labelitemi] \textbf{% \textit{poly\_guards}@!, \textit{poly\_tags}@!, \textit{raw\_mono\_guards}@!, \\ \textit{raw\_mono\_tags}@! (mildly unsound):} \\ @@ -1022,7 +1065,7 @@ \textit{metis} proof method, the `\hbox{@!}' suffix is replaced by \hbox{``\textit{\_at\_bang}''}. -\item[$\bullet$] \textbf{\textit{smart}:} The actual encoding used depends on +\item[\labelitemi] \textbf{\textit{smart}:} The actual encoding used depends on the ATP and should be the most efficient virtually sound encoding for that ATP. \end{enum} @@ -1116,11 +1159,11 @@ Specifies the expected outcome, which must be one of the following: \begin{enum} -\item[$\bullet$] \textbf{\textit{some}:} Sledgehammer found a (potentially +\item[\labelitemi] \textbf{\textit{some}:} Sledgehammer found a (potentially unsound) proof. -\item[$\bullet$] \textbf{\textit{none}:} Sledgehammer found no proof. -\item[$\bullet$] \textbf{\textit{timeout}:} Sledgehammer timed out. -\item[$\bullet$] \textbf{\textit{unknown}:} Sledgehammer encountered some +\item[\labelitemi] \textbf{\textit{none}:} Sledgehammer found no proof. +\item[\labelitemi] \textbf{\textit{timeout}:} Sledgehammer timed out. +\item[\labelitemi] \textbf{\textit{unknown}:} Sledgehammer encountered some problem. \end{enum}