1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex Mon Jun 27 14:56:10 2011 +0200
1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex Mon Jun 27 14:56:26 2011 +0200
1.3 @@ -337,12 +337,6 @@
1.4 and simply write the prover names as a space-separated list (e.g., ``\textit{e
1.5 spass remote\_vampire}'').
1.6
1.7 -\item[$\bullet$] \textbf{\textit{full\_types}} (\S\ref{problem-encoding})
1.8 -specifies whether type-sound encodings should be used. By default, Sledgehammer
1.9 -employs a mixture of type-sound and type-unsound encodings, occasionally
1.10 -yielding unsound ATP proofs. In contrast, SMT solver proofs should always be
1.11 -sound.
1.12 -
1.13 \item[$\bullet$] \textbf{\textit{max\_relevant}} (\S\ref{relevance-filter})
1.14 specifies the maximum number of facts that should be passed to the provers. By
1.15 default, the value is prover-dependent but varies between about 150 and 1000. If
1.16 @@ -404,13 +398,11 @@
1.17 Proof reconstruction failed.
1.18 \postw
1.19
1.20 -This usually indicates that Sledgehammer found a type-incorrect proof.
1.21 -Sledgehammer erases some type information to speed up the search. Try
1.22 -Sledgehammer again with full type information: \textit{full\_types}
1.23 -(\S\ref{problem-encoding}), or choose a specific type encoding with
1.24 -\textit{type\_sys} (\S\ref{problem-encoding}). Older versions of Sledgehammer
1.25 -were frequent victims of this problem. Now this should very seldom be an issue,
1.26 -but if you notice many unsound proofs, contact the author at \authoremail.
1.27 +This message usually indicates that Sledgehammer found a type-incorrect proof.
1.28 +This was a frequent issue with older versions of Sledgehammer, which did not
1.29 +supply enough typing information to the ATPs by default. If you notice many
1.30 +unsound proofs and are not using \textit{type\_sys} (\S\ref{problem-encoding}),
1.31 +contact the author at \authoremail.
1.32
1.33 \point{How can I tell whether a generated proof is sound?}
1.34
1.35 @@ -427,14 +419,14 @@
1.36 quickly if it is sound, and the \textit{type\_sys} $=$ \textit{poly\_tags}
1.37 option (\S\ref{problem-encoding}) ensures that no unsound proofs are found.
1.38
1.39 -The \textit{full\_types} option (\S\ref{problem-encoding}) can also be used
1.40 -here, but it is unsound in extremely rare degenerate cases such as the
1.41 -following:
1.42 -
1.43 -\prew
1.44 -\textbf{lemma} ``$\forall x\> y\Colon{'}\!a.\ x = y \,\Longrightarrow \exists f\> g\Colon\mathit{nat} \Rightarrow {'}\!a.\ f \not= g$'' \\
1.45 -\textbf{sledgehammer} [\textit{full\_types}] (\textit{nat.distinct\/}(1))
1.46 -\postw
1.47 +%The \textit{full\_types} option (\S\ref{problem-encoding}) can also be used
1.48 +%here, but it is unsound in extremely rare degenerate cases such as the
1.49 +%following:
1.50 +%
1.51 +%\prew
1.52 +%\textbf{lemma} ``$\forall x\> y\Colon{'}\!a.\ x = y \,\Longrightarrow \exists f\> g\Colon\mathit{nat} \Rightarrow {'}\!a.\ f \not= g$'' \\
1.53 +%\textbf{sledgehammer} [\textit{full\_types}] (\textit{nat.distinct\/}(1))
1.54 +%\postw
1.55
1.56 \point{Which facts are passed to the automatic provers?}
1.57
1.58 @@ -654,8 +646,9 @@
1.59 enabling the ``Auto Sledgehammer'' option from the ``Isabelle'' menu in Proof
1.60 General. For automatic runs, only the first prover set using \textit{provers}
1.61 (\S\ref{mode-of-operation}) is considered, fewer facts are passed to the prover,
1.62 -\textit{slicing} (\S\ref{mode-of-operation}) is disabled, \textit{full\_types}
1.63 -(\S\ref{problem-encoding}) is enabled, \textit{verbose} (\S\ref{output-format})
1.64 +\textit{slicing} (\S\ref{mode-of-operation}) is disabled,
1.65 +%\textit{full\_types} (\S\ref{problem-encoding}) is enabled,
1.66 +\textit{verbose} (\S\ref{output-format})
1.67 and \textit{debug} (\S\ref{output-format}) are disabled, and \textit{timeout}
1.68 (\S\ref{timeouts}) is superseded by the ``Auto Tools Time Limit'' in Proof
1.69 General's ``Isabelle'' menu. Sledgehammer's output is also more concise.
1.70 @@ -890,13 +883,13 @@
1.71 \label{problem-encoding}
1.72
1.73 \begin{enum}
1.74 -\opfalse{full\_types}{partial\_types}
1.75 -Specifies whether a type-sound encoding should be used when translating
1.76 -higher-order types to untyped first-order logic. Enabling this option virtually
1.77 -prevents the discovery of type-incorrect proofs, but it can slow down the ATP
1.78 -slightly. This option is implicitly enabled for automatic runs. For historical
1.79 -reasons, the default value of this option can be overridden using the option
1.80 -``Sledgehammer: Full Types'' from the ``Isabelle'' menu in Proof General.
1.81 +%\opfalse{full\_types}{partial\_types}
1.82 +%Specifies whether a type-sound encoding should be used when translating
1.83 +%higher-order types to untyped first-order logic. Enabling this option virtually
1.84 +%prevents the discovery of type-incorrect proofs, but it can slow down the ATP
1.85 +%slightly. This option is implicitly enabled for automatic runs. For historical
1.86 +%reasons, the default value of this option can be overridden using the option
1.87 +%``Sledgehammer: Full Types'' from the ``Isabelle'' menu in Proof General.
1.88
1.89 \opdefault{type\_sys}{string}{smart}
1.90 Specifies the type system to use in ATP problems. Some of the type systems are
1.91 @@ -977,9 +970,8 @@
1.92 \textit{metis} proof method, the exclamation mark is replaced by a
1.93 ``\textit{\_bang}'' suffix.
1.94
1.95 -\item[$\bullet$] \textbf{\textit{smart}:} If \textit{full\_types} is enabled,
1.96 -uses a sound or virtually sound encoding; otherwise, uses any encoding. The actual
1.97 -encoding used depends on the ATP and should be the most efficient for that ATP.
1.98 +\item[$\bullet$] \textbf{\textit{smart}:} The actual encoding used depends on
1.99 +the ATP and should be the most efficient virtually sound encoding for that ATP.
1.100 \end{enum}
1.101
1.102 In addition, all the \textit{preds} and \textit{tags} type systems are available