updated Sledgehammer documentation
authorblanchet
Wed Sep 07 09:10:41 2011 +0200 (2011-09-07)
changeset 4476915102294a166
parent 44768 a7bc1bdb8bb4
child 44770 3b1b4d805441
updated Sledgehammer documentation
doc-src/Sledgehammer/sledgehammer.tex
     1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Wed Sep 07 09:10:41 2011 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Wed Sep 07 09:10:41 2011 +0200
     1.3 @@ -883,13 +883,7 @@
     1.4  Specifies the type encoding to use in ATP problems. Some of the type encodings
     1.5  are unsound, meaning that they can give rise to spurious proofs
     1.6  (unreconstructible using Metis). The supported type encodings are listed below,
     1.7 -with an indication of their soundness in parentheses.
     1.8 -%
     1.9 -All the encodings with \textit{guards} or \textit{tags} in their name are
    1.10 -available in a ``uniform'' and a ``nonuniform'' variant. The nonuniform variants
    1.11 -are generally more efficient and are the default; the uniform variants are
    1.12 -identified by the suffix \textit{\_uniform} (e.g.,
    1.13 -\textit{mono\_guards\_uniform}{?}).
    1.14 +with an indication of their soundness in parentheses:
    1.15  
    1.16  \begin{enum}
    1.17  \item[$\bullet$] \textbf{\textit{erased} (very unsound):} No type information is
    1.18 @@ -933,12 +927,11 @@
    1.19  
    1.20  \item[$\bullet$] \textbf{\textit{mono\_simple} (sound):} Exploits simple
    1.21  first-order types if the prover supports the TFF0 or THF0 syntax; otherwise,
    1.22 -falls back on \textit{mono\_guards\_uniform}. The problem is monomorphized.
    1.23 +falls back on \textit{mono\_guards}. The problem is monomorphized.
    1.24  
    1.25  \item[$\bullet$] \textbf{\textit{mono\_simple\_higher} (sound):} Exploits simple
    1.26  higher-order types if the prover supports the THF0 syntax; otherwise, falls back
    1.27 -on \textit{mono\_simple} or \textit{mono\_guards\_uniform}. The problem is
    1.28 -monomorphized.
    1.29 +on \textit{mono\_simple} or \textit{mono\_guards}. The problem is monomorphized.
    1.30  
    1.31  \item[$\bullet$]
    1.32  \textbf{%
    1.33 @@ -958,6 +951,13 @@
    1.34  
    1.35  \item[$\bullet$]
    1.36  \textbf{%
    1.37 +\textit{poly\_guards}??, \textit{poly\_tags}??, \textit{raw\_mono\_guards}??, \\
    1.38 +\textit{raw\_mono\_tags}??, \textit{mono\_guards}??, \textit{mono\_tags}?? \\
    1.39 +(quasi-sound):} \\
    1.40 +Even lighter versions of the `{?}' encodings.
    1.41 +
    1.42 +\item[$\bullet$]
    1.43 +\textbf{%
    1.44  \textit{poly\_guards}!, \textit{poly\_tags}!, \textit{raw\_mono\_guards}!, \\
    1.45  \textit{raw\_mono\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \\
    1.46  \textit{mono\_simple}!, \textit{mono\_simple\_higher}! (mildly unsound):} \\
    1.47 @@ -972,6 +972,13 @@
    1.48  \textit{metis} proof method, the exclamation mark is replaced by the suffix
    1.49  \hbox{``\textit{\_bang}''}.
    1.50  
    1.51 +\item[$\bullet$]
    1.52 +\textbf{%
    1.53 +\textit{poly\_guards}!!, \textit{poly\_tags}!!, \textit{raw\_mono\_guards}!!, \\
    1.54 +\textit{raw\_mono\_tags}!!, \textit{mono\_guards}!!, \textit{mono\_tags}!! \\
    1.55 +(mildly unsound):} \\
    1.56 +Even lighter versions of the `{!}' encodings.
    1.57 +
    1.58  \item[$\bullet$] \textbf{\textit{smart}:} The actual encoding used depends on
    1.59  the ATP and should be the most efficient virtually sound encoding for that ATP.
    1.60  \end{enum}