# HG changeset patch # User blanchet # Date 1315423881 -7200 # Node ID efa1f532508b739005fa386300d7aeaf55b1d367 # Parent 19b70980a1bb3976c2de58ce20a15d9ed6920faa update Sledgehammer docs diff -r 19b70980a1bb -r efa1f532508b doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Wed Sep 07 21:31:21 2011 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Sep 07 21:31:21 2011 +0200 @@ -942,19 +942,29 @@ \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards}, \textit{mono\_tags}, and \textit{mono\_simple} are fully typed and sound. For each of these, Sledgehammer also provides a lighter, -virtually sound variant identified by a question mark (`{?}')\ that detects and -erases monotonic types, notably infinite types. (For \textit{mono\_simple}, the -types are not actually erased but rather replaced by a shared uniform type of -individuals.) As argument to the \textit{metis} proof method, the question mark -is replaced by a \hbox{``\textit{\_query}''} suffix. If the \emph{sound} option -is enabled, these encodings are fully sound. +virtually sound variant identified by a question mark (`\hbox{?}')\ that detects +and erases monotonic types, notably infinite types. (For \textit{mono\_simple}, +the types are not actually erased but rather replaced by a shared uniform type +of individuals.) As argument to the \textit{metis} proof method, the question +mark is replaced by a \hbox{``\textit{\_query}''} suffix. If the \emph{sound} +option is enabled, these encodings are fully sound. \item[$\bullet$] \textbf{% \textit{poly\_guards}??, \textit{poly\_tags}??, \textit{raw\_mono\_guards}??, \\ \textit{raw\_mono\_tags}??, \textit{mono\_guards}??, \textit{mono\_tags}?? \\ (quasi-sound):} \\ -Even lighter versions of the `{?}' encodings. +Even lighter versions of the `\hbox{?}' encodings. As argument to the +\textit{metis} proof method, the `\hbox{??}' suffix is replaced by +\hbox{``\textit{\_query\_query}''}. + +\item[$\bullet$] +\textbf{% +\textit{poly\_guards}@?, \textit{poly\_tags}@?, \textit{raw\_mono\_guards}@?, \\ +\textit{raw\_mono\_tags}@? (quasi-sound):} \\ +Alternative versions of the `\hbox{??}' encodings. As argument to the +\textit{metis} proof method, the `\hbox{@?}' suffix is replaced by +\hbox{``\textit{\_at\_query}''}. \item[$\bullet$] \textbf{% @@ -965,9 +975,9 @@ \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards}, \textit{mono\_tags}, \textit{mono\_simple}, and \textit{mono\_simple\_higher} also admit a mildly unsound (but very efficient) variant identified by an -exclamation mark (`{!}') that detects and erases erases all types except those -that are clearly finite (e.g., \textit{bool}). (For \textit{mono\_simple} and -\textit{mono\_simple\_higher}, the types are not actually erased but rather +exclamation mark (`\hbox{!}') that detects and erases erases all types except +those that are clearly finite (e.g., \textit{bool}). (For \textit{mono\_simple} +and \textit{mono\_simple\_higher}, the types are not actually erased but rather replaced by a shared uniform type of individuals.) As argument to the \textit{metis} proof method, the exclamation mark is replaced by the suffix \hbox{``\textit{\_bang}''}. @@ -977,7 +987,17 @@ \textit{poly\_guards}!!, \textit{poly\_tags}!!, \textit{raw\_mono\_guards}!!, \\ \textit{raw\_mono\_tags}!!, \textit{mono\_guards}!!, \textit{mono\_tags}!! \\ (mildly unsound):} \\ -Even lighter versions of the `{!}' encodings. +Even lighter versions of the `\hbox{!}' encodings. As argument to the +\textit{metis} proof method, the `\hbox{!!}' suffix is replaced by +\hbox{``\textit{\_bang\_bang}''}. + +\item[$\bullet$] +\textbf{% +\textit{poly\_guards}@!, \textit{poly\_tags}@!, \textit{raw\_mono\_guards}@!, \\ +\textit{raw\_mono\_tags}@! (mildly unsound):} \\ +Alternative versions of the `\hbox{!!}' encodings. As argument to the +\textit{metis} proof method, the `\hbox{@!}' suffix is replaced by +\hbox{``\textit{\_at\_bang}''}. \item[$\bullet$] \textbf{\textit{smart}:} The actual encoding used depends on the ATP and should be the most efficient virtually sound encoding for that ATP.