# HG changeset patch # User desharna # Date 1604599285 -3600 # Node ID 20587c17cb20c0edf39989a7108477a225a9cb00 # Parent c7e2a9bdc585109210e0a2d3c65d0f9c728c1830 Expanded and tuned documentation diff -r c7e2a9bdc585 -r 20587c17cb20 src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Thu Nov 05 18:14:02 2020 +0100 +++ b/src/Doc/Sledgehammer/document/root.tex Thu Nov 05 19:01:25 2020 +0100 @@ -47,6 +47,8 @@ \renewcommand\_{\hbox{\textunderscore\kern-.05ex}} +\hyphenation{Isa-belle super-posi-tion zipper-posi-tion} + \begin{document} %%% TYPESETTING @@ -129,15 +131,15 @@ \newbox\boxA \setbox\boxA=\hbox{\texttt{NOSPAM}} -\newcommand\authoremail{\texttt{blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak -in.\allowbreak tum.\allowbreak de}} +\newcommand\authoremail{\texttt{jasmin.blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak +google.\allowbreak com}} To run Sledgehammer, you must make sure that the theory \textit{Sledgehammer} is imported---this is rarely a problem in practice since it is part of -\textit{Main}. Examples of Sledgehammer use can be found in Isabelle's -\texttt{src/HOL/Metis\_Examples} directory. -Comments and bug reports concerning Sledgehammer or this manual should be -directed to the author at \authoremail. +\textit{Main}. Examples of Sledgehammer use can be found in the +\texttt{src/HOL/Metis\_Examples} directory. Comments and bug reports +concerning Sledgehammer or this manual should be directed to the author at +\authoremail. \section{Installation} @@ -219,7 +221,7 @@ (\texttt{libwww-perl}) installed. If you must use a proxy server to access the Internet, set the \texttt{http\_proxy} environment variable to the proxy, either in the environment in which Isabelle is launched or in your -\texttt{\$ISABELLE\_HOME\_USER/etc/settings} file. Here are a few +\texttt{\$ISABELLE\_HOME\_USER/etc/\allowbreak settings} file. Here are a few examples: \prew @@ -360,16 +362,16 @@ \begin{enum} \item[\labelitemi] -The traditional relevance filter, called \emph{MePo} -(\underline{Me}ng--\underline{Pau}lson), assigns a score to every available fact -(lemma, theorem, definition, or axiom) based upon how many constants that fact -shares with the conjecture. This process iterates to include facts relevant to -those just accepted. The constants are weighted to give unusual ones greater -significance. MePo copes best when the conjecture contains some unusual -constants; if all the constants are common, it is unable to discriminate among -the hundreds of facts that are picked up. The filter is also memoryless: It has -no information about how many times a particular fact has been used in a proof, -and it cannot learn. +The traditional relevance filter, \emph{MePo} +(\underline{Me}ng--\underline{Pau}lson), assigns a score to every available +fact (lemma, theorem, definition, or axiom) based upon how many constants that +fact shares with the conjecture. This process iterates to include facts +relevant to those just accepted. The constants are weighted to give unusual +ones greater significance. MePo copes best when the conjecture contains some +unusual constants; if all the constants are common, it is unable to +discriminate among the hundreds of facts that are picked up. The filter is also +memoryless: It has no information about how many times a particular fact has +been used in a proof, and it cannot learn. \item[\labelitemi] An alternative to MePo is \emph{MaSh} (\underline{Ma}chine Learner for @@ -438,32 +440,7 @@ strongly encouraged to report this to the author at \authoremail. -\point{How can I tell whether a suggested proof is sound?} - -Earlier versions of Sledgehammer often suggested unsound proofs---either proofs -of nontheorems or simply proofs that rely on type-unsound inferences. This -is a thing of the past, unless you explicitly specify an unsound encoding -using \textit{type\_enc} (\S\ref{problem-encoding}). -% -Officially, the only form of ``unsoundness'' that lurks in the sound -encodings is related to missing characteristic theorems of datatypes. For -example, - -\prew -\textbf{lemma}~``$\exists \mathit{xs}.\; \mathit{xs} \neq []$'' \\ -\textbf{sledgehammer} () -\postw - -suggests an argumentless \textit{metis} call that fails. However, the conjecture -does actually hold, and the \textit{metis} call can be repaired by adding -\textit{list.distinct}. -% -We hope to address this problem in a future version of Isabelle. In the -meantime, you can avoid it by passing the \textit{strict} option -(\S\ref{problem-encoding}). - - -\point{What are the \textit{full\_types}, \textit{no\_types}, and +\point{What are the \textit{full\_types}, \textit{no\_types}, and \\ \textit{mono\_tags} arguments to Metis?} The \textit{metis}~(\textit{full\_types}) proof method @@ -499,7 +476,7 @@ \textit{full\_types} option to \textit{metis} directly. -\point{And what are the \textit{lifting} and \textit{hide\_lams} arguments +\point{And what are the \textit{lifting} and \textit{hide\_lams} \\ arguments to Metis?} Orthogonally to the encoding of types, it is important to choose an appropriate @@ -516,12 +493,7 @@ Sledgehammer includes a minimization tool that takes a set of facts returned by a given prover and repeatedly calls a prover or proof method with subsets of those facts to find a minimal set. Reducing the number of facts typically helps -reconstruction, while also removing superfluous clutter from the proof scripts. - -In earlier versions of Sledgehammer, generated proofs were systematically -accompanied by a suggestion to invoke the minimization tool. This step is now -performed by default but can be disabled using the \textit{minimize} option -(\S\ref{mode-of-operation}). +reconstruction, while decluttering the proof scripts. \point{A strange error occurred---what should I do?} @@ -541,9 +513,9 @@ \point{Why are there so many options?} -Sledgehammer's philosophy should work out of the box, without user guidance. -Many of the options are meant to be used mostly by the Sledgehammer developers -for experiments. Of course, feel free to try them out if you are so inclined. +Sledgehammer's philosophy is that it should work out of the box, without user +guidance. Most of the options are meant to be used by the Sledgehammer +developers for experiments. \section{Command Syntax} @@ -825,11 +797,11 @@ \item[\labelitemi] \textbf{\textit{zipperposition}:} Zipperposition \cite{cruanes-2014} is a higher-order superposition prover developed by Simon -Cruanes and colleagues. To use Zipperposition, set the environment variable -\texttt{ZIPPERPOSITION\_HOME} to the directory that contains the -\texttt{zipperposition} executable and \texttt{ZIPPERPOSITION\_VERSION} to the -version number (e.g., ``2.0.1''). Sledgehammer has been tested with version -2.0.1. +Cruanes, Petar Vukmirovi\'c, and colleagues. To use Zipperposition, set the +environment variable \texttt{ZIPPERPOSITION\_HOME} to the directory that +contains the \texttt{zipperposition} executable and +\texttt{ZIPPERPOSITION\_VERSION} to the version number (e.g., ``2.0.1''). +Sledgehammer has been tested with version 2.0.1. \end{enum} \end{sloppy} @@ -1098,10 +1070,10 @@ \item[\labelitemi] \textbf{% \textit{mono\_guards}, \textit{mono\_tags} (sound); -\textit{mono\_args} (unsound):} \\ +\textit{mono\_args} \\ (unsound):} \\ Similar to \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, and -\textit{raw\_mono\_args}, respectively but types are mangled in constant names +\textit{raw\_mono\_\allowbreak args}, respectively but types are mangled in constant names instead of being supplied as ground term arguments. The binary predicate $\const{g}(\tau, t)$ becomes a unary predicate $\const{g\_}\tau(t)$, and the binary function @@ -1112,14 +1084,23 @@ first-order types if the prover supports the TF0, TF1, TH0, or TH1 syntax; otherwise, falls back on \textit{mono\_guards}. The problem is monomorphized. -\item[\labelitemi] \textbf{\textit{mono\_native\_higher} (sound):} Exploits -native higher-order types if the prover supports the TH0 syntax; otherwise, -falls back on \textit{mono\_native} or \textit{mono\_guards}. The problem is -monomorphized. +\item[\labelitemi] \textbf{\textit{mono\_native\_fool} (sound):} Exploits native +first-order types, including Booleans, if the prover supports the TFX0, TFX1, +TH0, or TH1 syntax; otherwise, falls back on \textit{mono\_native}. The problem +is monomorphized. -\item[\labelitemi] \textbf{\textit{poly\_native} (sound):} Exploits native -first-order polymorphic types if the prover supports the TF1 or TH1 syntax; -otherwise, falls back on \textit{mono\_native}. +\item[\labelitemi] \textbf{\textit{mono\_native\_higher}, +\textit{mono\_native\_higher\_fool} \\ (sound):} Exploits native higher-order +types, including Booleans if ending with ``\textit{\_fool}'', if the prover +supports the TH0 syntax; otherwise, falls back on \textit{mono\_native} or +\textit{mono\_native\_fool}. The problem is monomorphized. + +\item[\labelitemi] \textbf{\textit{poly\_native}, \textit{poly\_native\_fool}, +\textit{poly\_native\_higher}, \\ \textit{poly\_native\_higher\_fool} (sound):} +Exploits native first-order polymorphic types if the prover supports the TF1, +TFX1, or TH1 syntax; otherwise, falls back on \textit{mono\_native}, +\textit{mono\_native\_fool}, \textit{mono\_native\_higher}, or +\textit{mono\_native\_higher\_fool}. \item[\labelitemi] \textbf{% @@ -1327,8 +1308,7 @@ \end{verbatim} This command specifies Sledgehammer as the action, using E as the prover with a -timeout of 10 seconds. The results are written to the file -\texttt{output/Huffman.log}. +timeout of 10 seconds. The results are written to \texttt{output/Huffman.log}. \subsection{Example of Benchmarking Another Tool} @@ -1337,7 +1317,7 @@ \end{verbatim} This command specifies the \textbf{try0} command as the action, with a timeout -of 10 seconds. The results are written to the file \texttt{output/Huffman.log}. +of 10 seconds. The results are written to \texttt{output/Huffman.log}. \subsection{Example of Generating TPTP Files}