--- a/doc-src/Sledgehammer/sledgehammer.tex Tue Jun 07 08:52:35 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Jun 07 08:58:23 2011 +0200
@@ -495,7 +495,8 @@
set the \textit{isar\_shrink\_factor} option (\S\ref{output-format}) to a larger
value or to try several provers and keep the nicest-looking proof.
-\point{What is the \textit{full\_types}/\textit{no\_types} argument to Metis?}
+\point{What are the \textit{full\_types} and \textit{no\_types} arguments to
+Metis?}
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
@@ -510,7 +511,12 @@
actually work and to display timing information. This can be configured using
the \textit{preplay\_timeout} option (\S\ref{timeouts}).)
-If you see the warning
+At the other end of the soundness spectrum, \textit{metis} (\textit{no\_types})
+uses no type information at all during the proof search, which is more efficient
+but often fails. Calls to \textit{metis} (\textit{no\_types}) are occasionally
+generated by Sledgehammer.
+
+Incidentally, if you see the warning
\prew
\slshape
@@ -520,11 +526,6 @@
in a successful Metis proof, you can advantageously pass the
\textit{full\_types} option to \textit{metis} directly.
-At the other end of the soundness spectrum, \textit{metis} (\textit{no\_types})
-uses no type information at all during the proof search, which is more efficient
-but often fails. Calls to \textit{metis} (\textit{no\_types}) are occasionally
-generated by Sledgehammer.
-
\point{Are generated proofs minimal?}
Automatic provers frequently use many more facts than are necessary.
@@ -534,11 +535,11 @@
improves Metis's speed and success rate, while also removing superfluous clutter
from the proof scripts.
-In earlier versions of Sledgehammer, generated proofs were accompanied by a
-suggestion to invoke the minimization tool. This step is now performed
-implicitly if it can be done in a reasonable amount of time (something that can
-be guessed from the number of facts in the original proof and the time it took
-to find it or replay it).
+In earlier versions of Sledgehammer, generated proofs were systematically
+accompanied by a suggestion to invoke the minimization tool. This step is now
+performed implicitly if it can be done in a reasonable amount of time (something
+that can be guessed from the number of facts in the original proof and the time
+it took to find it or replay it).
In addition, some provers (notably CVC3, Satallax, and Yices) do not provide
proofs or sometimes provide incomplete proofs. The minimizer is then invoked to
@@ -667,10 +668,11 @@
where \qty{type\_sys} is a type system specification with the same semantics as
Sledgehammer's \textit{type\_sys} option (\S\ref{problem-encoding}) and
-\qty{facts} is a list of arbitrary facts. \qty{type\_sys} may also be
-\textit{full\_types}, in which case an appropriate type-sound encoding is
-chosen, \textit{partial\_types} (the default), or \textit{no\_types}, a synonym
-for \textit{erased}.
+\qty{facts} is a list of arbitrary facts. In addition to the values listed in
+\S\ref{problem-encoding}, \qty{type\_sys} may also be \textit{full\_types}, in
+which case an appropriate type-sound encoding is chosen, \textit{partial\_types}
+(the default type-unsound encoding), or \textit{no\_types}, a synonym for
+\textit{erased}.
\section{Option Reference}
\label{option-reference}