updated Sledgehammer's docs
authorblanchet
Tue Sep 06 11:31:01 2011 +0200 (2011-09-06)
changeset 44743804dfa6d35b6
parent 44742 68e34e7f01ab
child 44744 bdf8eb8f126b
updated Sledgehammer's docs
doc-src/Sledgehammer/sledgehammer.tex
     1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Tue Sep 06 11:31:01 2011 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Tue Sep 06 11:31:01 2011 +0200
     1.3 @@ -108,11 +108,11 @@
     1.4  results are correct by construction.
     1.5  
     1.6  In this manual, we will explicitly invoke the \textbf{sledgehammer} command.
     1.7 -Sledgehammer also provides an automatic mode that can be enabled via the
     1.8 -``Auto Sledgehammer'' option from the ``Isabelle'' menu in Proof General. In
     1.9 -this mode, Sledgehammer is run on every newly entered theorem. The time limit
    1.10 -for Auto Sledgehammer and other automatic tools can be set using the ``Auto
    1.11 -Tools Time Limit'' option.
    1.12 +Sledgehammer also provides an automatic mode that can be enabled via the ``Auto
    1.13 +Sledgehammer'' option in Proof General's ``Isabelle'' menu. In this mode,
    1.14 +Sledgehammer is run on every newly entered theorem. The time limit for Auto
    1.15 +Sledgehammer and other automatic tools can be set using the ``Auto Tools Time
    1.16 +Limit'' option.
    1.17  
    1.18  \newbox\boxA
    1.19  \setbox\boxA=\hbox{\texttt{nospam}}
    1.20 @@ -633,8 +633,8 @@
    1.21  highly-relevant and \qty{facts\/_{\mathrm{2}}} fully irrelevant.
    1.22  
    1.23  You can instruct Sledgehammer to run automatically on newly entered theorems by
    1.24 -enabling the ``Auto Sledgehammer'' option from the ``Isabelle'' menu in Proof
    1.25 -General. For automatic runs, only the first prover set using \textit{provers}
    1.26 +enabling the ``Auto Sledgehammer'' option in Proof General's ``Isabelle'' menu.
    1.27 +For automatic runs, only the first prover set using \textit{provers}
    1.28  (\S\ref{mode-of-operation}) is considered, fewer facts are passed to the prover,
    1.29  \textit{slicing} (\S\ref{mode-of-operation}) is disabled, \textit{sound}
    1.30  (\S\ref{problem-encoding}) is enabled, \textit{verbose} (\S\ref{output-format})
    1.31 @@ -724,7 +724,7 @@
    1.32  
    1.33  \item[$\bullet$] \textbf{\textit{leo2}:} LEO-II is an automatic
    1.34  higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
    1.35 -with support for the TPTP higher-order syntax (THF).
    1.36 +with support for the TPTP many-typed higher-order syntax (THF0).
    1.37  
    1.38  \item[$\bullet$] \textbf{\textit{metis}:} Although it is much less powerful than
    1.39  the external provers, Metis itself can be used for proof search.
    1.40 @@ -737,7 +737,7 @@
    1.41  
    1.42  \item[$\bullet$] \textbf{\textit{satallax}:} Satallax is an automatic
    1.43  higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with
    1.44 -support for the TPTP higher-order syntax (THF).
    1.45 +support for the TPTP many-typed higher-order syntax (THF0).
    1.46  
    1.47  \item[$\bullet$] \textbf{\textit{spass}:} SPASS is a first-order resolution
    1.48  prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}.
    1.49 @@ -752,7 +752,7 @@
    1.50  \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire}
    1.51  executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g., ``1.8'').
    1.52  Sledgehammer has been tested with versions 0.6, 1.0, and 1.8. Vampire 1.8
    1.53 -supports the TPTP many-typed first-order format (TFF).
    1.54 +supports the TPTP many-typed first-order format (TFF0).
    1.55  
    1.56  \item[$\bullet$] \textbf{\textit{yices}:} Yices is an SMT solver developed at
    1.57  SRI \cite{yices}. To use Yices, set the environment variable
    1.58 @@ -767,7 +767,7 @@
    1.59  
    1.60  \item[$\bullet$] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be
    1.61  an ATP, exploiting Z3's support for the TPTP untyped and many-typed first-order
    1.62 -formats (FOF and TFF). It is included for experimental purposes. It requires
    1.63 +formats (FOF and TFF0). It is included for experimental purposes. It requires
    1.64  version 3.0 or above.
    1.65  \end{enum}
    1.66  
    1.67 @@ -787,7 +787,7 @@
    1.68  
    1.69  \item[$\bullet$] \textbf{\textit{remote\_e\_tofof}:} E-ToFoF is a metaprover
    1.70  developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
    1.71 -servers. This ATP supports the TPTP many-typed first-order format (TFF). The
    1.72 +servers. This ATP supports the TPTP many-typed first-order format (TFF0). The
    1.73  remote version of E-ToFoF runs on Geoff Sutcliffe's Miami servers.
    1.74  
    1.75  \item[$\bullet$] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II
    1.76 @@ -798,7 +798,7 @@
    1.77  
    1.78  \item[$\bullet$] \textbf{\textit{remote\_snark}:} SNARK is a first-order
    1.79  resolution prover developed by Stickel et al.\ \cite{snark}. It supports the
    1.80 -TPTP many-typed first-order format (TFF). The remote version of SNARK runs on
    1.81 +TPTP many-typed first-order format (TFF0). The remote version of SNARK runs on
    1.82  Geoff Sutcliffe's Miami servers.
    1.83  
    1.84  \item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of
    1.85 @@ -818,17 +818,16 @@
    1.86  with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers.
    1.87  \end{enum}
    1.88  
    1.89 -By default, Sledgehammer will run E, E-SInE, SPASS, Vampire, Z3 (or whatever
    1.90 +By default, Sledgehammer runs E, E-SInE, SPASS, Vampire, Z3 (or whatever
    1.91  the SMT module's \textit{smt\_solver} configuration option is set to), and (if
    1.92  appropriate) Waldmeister in parallel---either locally or remotely, depending on
    1.93  the number of processor cores available. For historical reasons, the default
    1.94  value of this option can be overridden using the option ``Sledgehammer:
    1.95 -Provers'' from the ``Isabelle'' menu in Proof General.
    1.96 +Provers'' in Proof General's ``Isabelle'' menu.
    1.97  
    1.98 -It is a good idea to run several provers in parallel, although it could slow
    1.99 -down your machine. Running E, SPASS, and Vampire for 5~seconds yields a similar
   1.100 -success rate to running the most effective of these for 120~seconds
   1.101 -\cite{boehme-nipkow-2010}.
   1.102 +It is generally a good idea to run several provers in parallel. Running E,
   1.103 +SPASS, and Vampire for 5~seconds yields a similar success rate to running the
   1.104 +most effective of these for 120~seconds \cite{boehme-nipkow-2010}.
   1.105  
   1.106  For the \textit{min} subcommand, the default prover is \textit{metis}. If
   1.107  several provers are set, the first one is used.
   1.108 @@ -884,7 +883,13 @@
   1.109  Specifies the type encoding to use in ATP problems. Some of the type encodings
   1.110  are unsound, meaning that they can give rise to spurious proofs
   1.111  (unreconstructible using Metis). The supported type encodings are listed below,
   1.112 -with an indication of their soundness in parentheses:
   1.113 +with an indication of their soundness in parentheses.
   1.114 +%
   1.115 +All the encodings with \textit{guards} or \textit{tags} in their name are
   1.116 +available in a ``uniform'' and a ``nonuniform'' variant. The nonuniform variants
   1.117 +are generally more efficient and are the default; the uniform variants are
   1.118 +identified by the suffix \textit{\_uniform} (e.g.,
   1.119 +\textit{mono\_guards\_uniform}{?}).
   1.120  
   1.121  \begin{enum}
   1.122  \item[$\bullet$] \textbf{\textit{erased} (very unsound):} No type information is
   1.123 @@ -926,27 +931,27 @@
   1.124  $\mathit{type\/}(\tau, t)$ becomes a unary function
   1.125  $\mathit{type\_}\tau(t)$.
   1.126  
   1.127 -\item[$\bullet$] \textbf{\textit{simple} (sound):} Exploit simple first-order
   1.128 -types if the prover supports the TFF or THF syntax; otherwise, fall back on
   1.129 -\textit{mono\_guards}. The problem is monomorphized.
   1.130 +\item[$\bullet$] \textbf{\textit{mono\_simple} (sound):} Exploits simple
   1.131 +first-order types if the prover supports the TFF0 or THF0 syntax; otherwise,
   1.132 +falls back on \textit{mono\_guards\_uniform}. The problem is monomorphized.
   1.133  
   1.134 -\item[$\bullet$] \textbf{\textit{simple\_higher} (sound):} Exploit simple
   1.135 -higher-order types if the prover supports the THF syntax; otherwise, fall back
   1.136 -on \textit{simple} or \textit{mono\_guards\_uniform}. The problem is
   1.137 +\item[$\bullet$] \textbf{\textit{mono\_simple\_higher} (sound):} Exploits simple
   1.138 +higher-order types if the prover supports the THF0 syntax; otherwise, falls back
   1.139 +on \textit{mono\_simple} or \textit{mono\_guards\_uniform}. The problem is
   1.140  monomorphized.
   1.141  
   1.142  \item[$\bullet$]
   1.143  \textbf{%
   1.144  \textit{poly\_guards}?, \textit{poly\_tags}?, \textit{raw\_mono\_guards}?, \\
   1.145  \textit{raw\_mono\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\
   1.146 -\textit{simple}? (quasi-sound):} \\
   1.147 +\textit{mono\_simple}? (quasi-sound):} \\
   1.148  The type encodings \textit{poly\_guards}, \textit{poly\_tags},
   1.149  \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
   1.150 -\textit{mono\_tags}, and \textit{simple} are fully
   1.151 +\textit{mono\_tags}, and \textit{mono\_simple} are fully
   1.152  typed and sound. For each of these, Sledgehammer also provides a lighter,
   1.153  virtually sound variant identified by a question mark (`{?}')\ that detects and
   1.154 -erases monotonic types, notably infinite types. (For \textit{simple}, the types
   1.155 -are not actually erased but rather replaced by a shared uniform type of
   1.156 +erases monotonic types, notably infinite types. (For \textit{mono\_simple}, the
   1.157 +types are not actually erased but rather replaced by a shared uniform type of
   1.158  individuals.) As argument to the \textit{metis} proof method, the question mark
   1.159  is replaced by a \hbox{``\textit{\_query}''} suffix. If the \emph{sound} option
   1.160  is enabled, these encodings are fully sound.
   1.161 @@ -954,30 +959,25 @@
   1.162  \item[$\bullet$]
   1.163  \textbf{%
   1.164  \textit{poly\_guards}!, \textit{poly\_tags}!, \textit{raw\_mono\_guards}!, \\
   1.165 -\textit{raw\_mono\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \textit{simple}!, \\
   1.166 -\textit{simple\_higher}! (mildly unsound):} \\
   1.167 +\textit{raw\_mono\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \\
   1.168 +\textit{mono\_simple}!, \textit{mono\_simple\_higher}! (mildly unsound):} \\
   1.169  The type encodings \textit{poly\_guards}, \textit{poly\_tags},
   1.170  \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
   1.171 -\textit{mono\_tags}, \textit{simple}, and \textit{simple\_higher} also admit
   1.172 -a mildly unsound (but very efficient) variant identified by an exclamation mark
   1.173 -(`{!}') that detects and erases erases all types except those that are clearly
   1.174 -finite (e.g., \textit{bool}). (For \textit{simple} and \textit{simple\_higher},
   1.175 -the types are not actually erased but rather replaced by a shared uniform type
   1.176 -of individuals.) As argument to the \textit{metis} proof method, the exclamation
   1.177 -mark is replaced by the suffix \hbox{``\textit{\_bang}''}.
   1.178 +\textit{mono\_tags}, \textit{mono\_simple}, and \textit{mono\_simple\_higher}
   1.179 +also admit a mildly unsound (but very efficient) variant identified by an
   1.180 +exclamation mark (`{!}') that detects and erases erases all types except those
   1.181 +that are clearly finite (e.g., \textit{bool}). (For \textit{mono\_simple} and
   1.182 +\textit{mono\_simple\_higher}, the types are not actually erased but rather
   1.183 +replaced by a shared uniform type of individuals.) As argument to the
   1.184 +\textit{metis} proof method, the exclamation mark is replaced by the suffix
   1.185 +\hbox{``\textit{\_bang}''}.
   1.186  
   1.187  \item[$\bullet$] \textbf{\textit{smart}:} The actual encoding used depends on
   1.188  the ATP and should be the most efficient virtually sound encoding for that ATP.
   1.189  \end{enum}
   1.190  
   1.191 -In addition, all the \textit{guards} and \textit{tags} type encodings are
   1.192 -available in two variants, a ``uniform'' and a ``nonuniform'' variant. The
   1.193 -nonuniform variants are generally more efficient and are the default; the
   1.194 -uniform variants are identified by the suffix \textit{\_uniform} (e.g.,
   1.195 -\textit{mono\_guards\_uniform}{?}).
   1.196 -
   1.197 -For SMT solvers, the type encoding is always \textit{simple}, irrespective of
   1.198 -the value of this option.
   1.199 +For SMT solvers, the type encoding is always \textit{mono\_simple}, irrespective
   1.200 +of the value of this option.
   1.201  
   1.202  \nopagebreak
   1.203  {\small See also \textit{max\_new\_mono\_instances} (\S\ref{relevance-filter})
   1.204 @@ -1091,8 +1091,7 @@
   1.205  Specifies the maximum number of seconds that the automatic provers should spend
   1.206  searching for a proof. This excludes problem preparation and is a soft limit.
   1.207  For historical reasons, the default value of this option can be overridden using
   1.208 -the option ``Sledgehammer: Time Limit'' from the ``Isabelle'' menu in Proof
   1.209 -General.
   1.210 +the option ``Sledgehammer: Time Limit'' in Proof General's ``Isabelle'' menu.
   1.211  
   1.212  \opdefault{preplay\_timeout}{float\_or\_none}{\upshape 4}
   1.213  Specifies the maximum number of seconds that Metis should be spent trying to