1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Fri Jul 01 15:53:37 2011 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Fri Jul 01 15:53:37 2011 +0200
     1.3 @@ -772,36 +772,39 @@
     1.4  on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
     1.5  
     1.6  \item[$\bullet$] \textbf{\textit{remote\_leo2}:} LEO-II is an automatic
     1.7 -higher-order prover developed by Christoph Benzm\"uller et al. \cite{leo2}. The
     1.8 -remote version of LEO-II runs on Geoff Sutcliffe's Miami servers. In the current
     1.9 -setup, the problems given to LEO-II are only mildly higher-order.
    1.10 +higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
    1.11 +with support for the TPTP higher-order syntax (THF). The remote version of
    1.12 +LEO-II runs on Geoff Sutcliffe's Miami servers. In the current setup, the
    1.13 +problems given to LEO-II are only mildly higher-order.
    1.14  
    1.15  \item[$\bullet$] \textbf{\textit{remote\_satallax}:} Satallax is an automatic
    1.16 -higher-order prover developed by Chad Brown et al. \cite{satallax}. The remote
    1.17 -version of Satallax runs on Geoff Sutcliffe's Miami servers. In the current
    1.18 -setup, the problems given to Satallax are only mildly higher-order.
    1.19 +higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with
    1.20 +support for the TPTP higher-order syntax (THF). The remote version of Satallax
    1.21 +runs on Geoff Sutcliffe's Miami servers. In the current setup, the problems
    1.22 +given to Satallax are only mildly higher-order.
    1.23  
    1.24  \item[$\bullet$] \textbf{\textit{remote\_sine\_e}:} SInE-E is a metaprover
    1.25  developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of
    1.26  SInE runs on Geoff Sutcliffe's Miami servers.
    1.27  
    1.28  \item[$\bullet$] \textbf{\textit{remote\_snark}:} SNARK is a first-order
    1.29 -resolution prover developed by Stickel et al.\ \cite{snark}. The remote version
    1.30 -of SNARK runs on Geoff Sutcliffe's Miami servers.
    1.31 +resolution prover developed by Stickel et al.\ \cite{snark}. It supports the
    1.32 +TPTP many-typed first-order format (TFF). The remote version of SNARK runs on
    1.33 +Geoff Sutcliffe's Miami servers.
    1.34  
    1.35  \item[$\bullet$] \textbf{\textit{remote\_tofof\_e}:} ToFoF-E is a metaprover
    1.36  developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
    1.37 -servers. This ATP supports a fragment of the TPTP many-typed first-order format
    1.38 -(TFF). It is supported primarily for experimenting with the
    1.39 -\textit{type\_sys} $=$ \textit{simple} option (\S\ref{problem-encoding}).
    1.40 +servers. This ATP supports the TPTP many-typed first-order format (TFF). The
    1.41 +remote version of ToFoF-E runs on Geoff Sutcliffe's Miami servers.
    1.42  
    1.43  \item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of
    1.44  Vampire runs on Geoff Sutcliffe's Miami servers. Version 9 is used.
    1.45  
    1.46  \item[$\bullet$] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit
    1.47  equality prover developed by Hillenbrand et al.\ \cite{waldmeister}. It can be
    1.48 -used to prove universally quantified equations using unconditional equations.
    1.49 -The remote version of Waldmeister runs on Geoff Sutcliffe's Miami servers.
    1.50 +used to prove universally quantified equations using unconditional equations,
    1.51 +corresponding to the TPTP CNF UEQ division. The remote version of Waldmeister
    1.52 +runs on Geoff Sutcliffe's Miami servers.
    1.53  
    1.54  \item[$\bullet$] \textbf{\textit{remote\_z3}:} The remote version of Z3 runs on
    1.55  servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
    1.56 @@ -919,39 +922,44 @@
    1.57  $\mathit{type\_info\/}(\tau, t)$ becomes a unary function
    1.58  $\mathit{type\_info\_}\tau(t)$.
    1.59  
    1.60 -\item[$\bullet$] \textbf{\textit{simple} (sound):} Use the prover's support for
    1.61 -simple types if available; otherwise, fall back on \textit{mangled\_preds}. The
    1.62 -problem is monomorphized.
    1.63 +\item[$\bullet$] \textbf{\textit{simple} (sound):} Exploit simple first-order
    1.64 +types if the prover supports the TFF or THF syntax; otherwise, fall back on
    1.65 +\textit{mangled\_preds}. The problem is monomorphized.
    1.66 +
    1.67 +\item[$\bullet$] \textbf{\textit{simple\_higher} (sound):} Exploit simple
    1.68 +higher-order types if the prover supports the THF syntax; otherwise, fall back
    1.69 +on \textit{simple} or \textit{mangled\_preds\_heavy}. The problem is
    1.70 +monomorphized.
    1.71  
    1.72  \item[$\bullet$]
    1.73  \textbf{%
    1.74  \textit{poly\_preds}?, \textit{poly\_tags}?, \textit{mono\_preds}?, \textit{mono\_tags}?, \\
    1.75 -\textit{mangled\_preds}?, \textit{mangled\_tags}?, \textit{simple}? (quasi-sound):} \\
    1.76 +\textit{mangled\_preds}?, \textit{mangled\_tags}?, \textit{simple}?, \textit{simple\_higher}? (quasi-sound):} \\
    1.77  The type systems \textit{poly\_preds}, \textit{poly\_tags},
    1.78  \textit{mono\_preds}, \textit{mono\_tags}, \textit{mangled\_preds},
    1.79 -\textit{mangled\_tags}, and \textit{simple} are fully typed and sound. For each
    1.80 -of these, Sledgehammer also provides a lighter, virtually sound variant
    1.81 -identified by a question mark (`{?}')\ that detects and erases monotonic types,
    1.82 -notably infinite types. (For \textit{simple}, the types are not actually erased
    1.83 -but rather replaced by a shared uniform type of individuals.) As argument to the
    1.84 -\textit{metis} proof method, the question mark is replaced by a
    1.85 -``\textit{\_query}'' suffix. If the \emph{sound} option is enabled, these
    1.86 -encodings are fully sound.
    1.87 +\textit{mangled\_tags}, \textit{simple}, and \textit{simple\_higher} are fully
    1.88 +typed and sound. For each of these, Sledgehammer also provides a lighter,
    1.89 +virtually sound variant identified by a question mark (`{?}')\ that detects and
    1.90 +erases monotonic types, notably infinite types. (For \textit{simple} and
    1.91 +\textit{simple\_higher}, the types are not actually erased but rather replaced
    1.92 +by a shared uniform type of individuals.) As argument to the \textit{metis}
    1.93 +proof method, the question mark is replaced by a \hbox{``\textit{\_query}''}
    1.94 +suffix. If the \emph{sound} option is enabled, these encodings are fully sound.
    1.95  
    1.96  \item[$\bullet$]
    1.97  \textbf{%
    1.98  \textit{poly\_preds}!, \textit{poly\_tags}!, \textit{mono\_preds}!, \textit{mono\_tags}!, \\
    1.99 -\textit{mangled\_preds}!, \textit{mangled\_tags}!, \textit{simple}! \\
   1.100 +\textit{mangled\_preds}!, \textit{mangled\_tags}!, \textit{simple}!, \textit{simple\_higher}! \\
   1.101  (mildly unsound):} \\
   1.102  The type systems \textit{poly\_preds}, \textit{poly\_tags},
   1.103  \textit{mono\_preds}, \textit{mono\_tags}, \textit{mangled\_preds},
   1.104 -\textit{mangled\_tags}, and \textit{simple} also admit a mildly unsound (but
   1.105 -very efficient) variant identified by an exclamation mark (`{!}') that detects
   1.106 -and erases erases all types except those that are clearly finite (e.g.,
   1.107 -\textit{bool}). (For \textit{simple}, the types are not actually erased but
   1.108 -rather replaced by a shared uniform type of individuals.) As argument to the
   1.109 -\textit{metis} proof method, the exclamation mark is replaced by a
   1.110 -``\textit{\_bang}'' suffix.
   1.111 +\textit{mangled\_tags}, \textit{simple}, and \textit{simple\_higher} also admit
   1.112 +a mildly unsound (but very efficient) variant identified by an exclamation mark
   1.113 +(`{!}') that detects and erases erases all types except those that are clearly
   1.114 +finite (e.g., \textit{bool}). (For \textit{simple} and \textit{simple\_higher},
   1.115 +the types are not actually erased but rather replaced by a shared uniform type
   1.116 +of individuals.) As argument to the \textit{metis} proof method, the exclamation
   1.117 +mark is replaced by a \hbox{``\textit{\_bang}''} suffix.
   1.118  
   1.119  \item[$\bullet$] \textbf{\textit{smart}:} The actual encoding used depends on
   1.120  the ATP and should be the most efficient virtually sound encoding for that ATP.
   1.121 @@ -963,8 +971,8 @@
   1.122  variants are identified by a \textit{\_heavy} suffix (e.g.,
   1.123  \textit{mangled\_preds\_heavy}{?}).
   1.124  
   1.125 -For SMT solvers and ToFoF-E, the type system is always \textit{simple},
   1.126 -irrespective of the value of this option.
   1.127 +For SMT solvers, the type system is always \textit{simple}, irrespective of the
   1.128 +value of this option.
   1.129  
   1.130  \nopagebreak
   1.131  {\small See also \textit{max\_new\_mono\_instances} (\S\ref{relevance-filter})