update Sledgehammer docs
authorblanchet
Wed Sep 07 21:31:21 2011 +0200 (2011-09-07)
changeset 44816efa1f532508b
parent 44815 19b70980a1bb
child 44817 b63e445c8f6d
update Sledgehammer docs
doc-src/Sledgehammer/sledgehammer.tex
     1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Wed Sep 07 21:31:21 2011 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Wed Sep 07 21:31:21 2011 +0200
     1.3 @@ -942,19 +942,29 @@
     1.4  \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
     1.5  \textit{mono\_tags}, and \textit{mono\_simple} are fully
     1.6  typed and sound. For each of these, Sledgehammer also provides a lighter,
     1.7 -virtually sound variant identified by a question mark (`{?}')\ that detects and
     1.8 -erases monotonic types, notably infinite types. (For \textit{mono\_simple}, the
     1.9 -types are not actually erased but rather replaced by a shared uniform type of
    1.10 -individuals.) As argument to the \textit{metis} proof method, the question mark
    1.11 -is replaced by a \hbox{``\textit{\_query}''} suffix. If the \emph{sound} option
    1.12 -is enabled, these encodings are fully sound.
    1.13 +virtually sound variant identified by a question mark (`\hbox{?}')\ that detects
    1.14 +and erases monotonic types, notably infinite types. (For \textit{mono\_simple},
    1.15 +the types are not actually erased but rather replaced by a shared uniform type
    1.16 +of individuals.) As argument to the \textit{metis} proof method, the question
    1.17 +mark is replaced by a \hbox{``\textit{\_query}''} suffix. If the \emph{sound}
    1.18 +option is enabled, these encodings are fully sound.
    1.19  
    1.20  \item[$\bullet$]
    1.21  \textbf{%
    1.22  \textit{poly\_guards}??, \textit{poly\_tags}??, \textit{raw\_mono\_guards}??, \\
    1.23  \textit{raw\_mono\_tags}??, \textit{mono\_guards}??, \textit{mono\_tags}?? \\
    1.24  (quasi-sound):} \\
    1.25 -Even lighter versions of the `{?}' encodings.
    1.26 +Even lighter versions of the `\hbox{?}' encodings. As argument to the
    1.27 +\textit{metis} proof method, the `\hbox{??}' suffix is replaced by
    1.28 +\hbox{``\textit{\_query\_query}''}.
    1.29 +
    1.30 +\item[$\bullet$]
    1.31 +\textbf{%
    1.32 +\textit{poly\_guards}@?, \textit{poly\_tags}@?, \textit{raw\_mono\_guards}@?, \\
    1.33 +\textit{raw\_mono\_tags}@? (quasi-sound):} \\
    1.34 +Alternative versions of the `\hbox{??}' encodings. As argument to the
    1.35 +\textit{metis} proof method, the `\hbox{@?}' suffix is replaced by
    1.36 +\hbox{``\textit{\_at\_query}''}.
    1.37  
    1.38  \item[$\bullet$]
    1.39  \textbf{%
    1.40 @@ -965,9 +975,9 @@
    1.41  \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
    1.42  \textit{mono\_tags}, \textit{mono\_simple}, and \textit{mono\_simple\_higher}
    1.43  also admit a mildly unsound (but very efficient) variant identified by an
    1.44 -exclamation mark (`{!}') that detects and erases erases all types except those
    1.45 -that are clearly finite (e.g., \textit{bool}). (For \textit{mono\_simple} and
    1.46 -\textit{mono\_simple\_higher}, the types are not actually erased but rather
    1.47 +exclamation mark (`\hbox{!}') that detects and erases erases all types except
    1.48 +those that are clearly finite (e.g., \textit{bool}). (For \textit{mono\_simple}
    1.49 +and \textit{mono\_simple\_higher}, the types are not actually erased but rather
    1.50  replaced by a shared uniform type of individuals.) As argument to the
    1.51  \textit{metis} proof method, the exclamation mark is replaced by the suffix
    1.52  \hbox{``\textit{\_bang}''}.
    1.53 @@ -977,7 +987,17 @@
    1.54  \textit{poly\_guards}!!, \textit{poly\_tags}!!, \textit{raw\_mono\_guards}!!, \\
    1.55  \textit{raw\_mono\_tags}!!, \textit{mono\_guards}!!, \textit{mono\_tags}!! \\
    1.56  (mildly unsound):} \\
    1.57 -Even lighter versions of the `{!}' encodings.
    1.58 +Even lighter versions of the `\hbox{!}' encodings. As argument to the
    1.59 +\textit{metis} proof method, the `\hbox{!!}' suffix is replaced by
    1.60 +\hbox{``\textit{\_bang\_bang}''}.
    1.61 +
    1.62 +\item[$\bullet$]
    1.63 +\textbf{%
    1.64 +\textit{poly\_guards}@!, \textit{poly\_tags}@!, \textit{raw\_mono\_guards}@!, \\
    1.65 +\textit{raw\_mono\_tags}@! (mildly unsound):} \\
    1.66 +Alternative versions of the `\hbox{!!}' encodings. As argument to the
    1.67 +\textit{metis} proof method, the `\hbox{@!}' suffix is replaced by
    1.68 +\hbox{``\textit{\_at\_bang}''}.
    1.69  
    1.70  \item[$\bullet$] \textbf{\textit{smart}:} The actual encoding used depends on
    1.71  the ATP and should be the most efficient virtually sound encoding for that ATP.