# HG changeset patch
# User blanchet
# Date 1304267845 -7200
# Node ID 6321d0dc3d72cf7a6e991eda6c08327da7463153
# Parent  398fff2c6b8f21134724964e73511a6ba2884b40
document new type system syntax

diff -r 398fff2c6b8f -r 6321d0dc3d72 NEWS
--- a/NEWS	Sun May 01 18:37:25 2011 +0200
+++ b/NEWS	Sun May 01 18:37:25 2011 +0200
@@ -60,7 +60,9 @@
 * Sledgehammer:
   - sledgehammer available_provers ~> sledgehammer supported_provers
     INCOMPATIBILITY.
-  - Added "monomorphize", "monomorphize_limit", and "type_sys" options.
+  - Added support for SNARK and ToFoF-E on SystemOnTPTP and for simply typed
+    TPTP problems (TFF).
+  - Added "type_sys" and "monomorphize_limit" options.
 
 * "try":
   - Added "simp:", "intro:", and "elim:" options.
diff -r 398fff2c6b8f -r 6321d0dc3d72 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Sun May 01 18:37:25 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Sun May 01 18:37:25 2011 +0200
@@ -571,37 +571,67 @@
 following values:
 
 \begin{enum}
-\item[$\bullet$] \textbf{\textit{tags}:} Each term (and subterm) is tagged with
-its type.
-
-\item[$\bullet$] \textbf{\textit{args}:} Constants are annotated with
-their type parameters, which are passed as extra arguments.
-
-\item[$\bullet$] \textbf{\textit{mangled}:} Types are mangled in constant names.
-This value implicitly enables \textit{monomorphize}.
-
 \item[$\bullet$] \textbf{\textit{many\_typed}:} Use the prover's support for
 many-typed first-order logic if available; otherwise, fall back on
-\textit{mangled}. This value implicitly enables \textit{monomorphize}.
+\textit{mangled}. The problem is monomorphized, meaning that the problem's type
+variables are instantiated with heuristically chosen ground types.
+Monomorphization can simplify reasoning but also leads to larger fact bases,
+which can slow down the ATPs.
+
+\item[$\bullet$] \textbf{\textit{mangled}:} Types are mangled in constant names,
+and predicates restrict the range of bound variables. The problem is
+monomorphized. This corresponds to the traditional encoding of types in an
+untyped logic without overloading (e.g., such as performed by the ToFoF-E
+wrapper).
+
+\item[$\bullet$] \textbf{\textit{args}:} Constants are annotated with their
+types, which are supplied as extra arguments.
+
+\item[$\bullet$] \textbf{\textit{mono\_args}:} Similar to \textit{args}, but
+the problem is additionally monomorphized.
+
+\item[$\bullet$] \textbf{\textit{tags}:} Each term (and subterm) is tagged with
+its type using a special uninterpreted function symbol.
+
+\item[$\bullet$] \textbf{\textit{mono\_tags}:} Similar to \textit{tags}, but
+the problem is additionally monomorphized.
 
 \item[$\bullet$] \textbf{\textit{none}:} No type information is supplied to the
-ATP. This value is ignored if \textit{full\_types} is enabled.
+ATP.
+
+\item[$\bullet$]
+\textbf{%
+\textit{many\_typed}!,
+\textit{mangled}!,
+\textit{args}!,
+\textit{mono\_args}!,
+\textit{tags}!, \\ %% TYPESETTING
+\textit{mono\_tags}!:}
+The type systems \textit{many\_typed}, \textit{mangled},
+(\textit{mono\_})\allowbreak\textit{args}, and
+(\textit{mono\_})\allowbreak\textit{tags} are fully typed and (virtually) sound.
+For each of these, Sledgehammer also provides a mildly unsound variant
+identified by one exclamation mark suffix (!).
+
+\item[$\bullet$]
+\textbf{%
+\textit{many\_typed}!!,
+\textit{mangled}!!,
+\textit{args}!!,
+\textit{mono\_args}!!,
+\textit{tags}!!, \\ %% TYPESETTING
+\textit{mono\_tags}!!:}
+More strongly unsound variants of \textit{many\_typed}, \textit{mangled},
+(\textit{mono\_})\allowbreak\textit{args}, and
+(\textit{mono\_})\allowbreak\textit{tags}, identified by two exclamation marks
+(!!).
 
 \item[$\bullet$] \textbf{\textit{smart}:} If \textit{full\_types} is enabled,
-this is the same as \textit{tags}; otherwise, this is the
-same as \textit{args}.
+uses a fully typed encoding; otherwise, uses a partially typed encoding. The
+actual encoding used depends on the ATP.
 \end{enum}
 
-For SMT solvers, the type system is always \textit{many\_typed}.
-
-\opfalse{monomorphize}{dont\_monomorphize}
-Specifies whether the relevant facts should be monomorphized---i.e., whether
-their type variables should be instantiated with relevant ground types.
-Monomorphization is always performed for SMT solvers, irrespective of this
-option. Monomorphization can simplify reasoning but also leads to larger fact
-bases, which can slow down the ATPs. If the type system is \textit{mangled} or
-\textit{many\_typed}, monomorphization is implicitly enabled irrespective of
-this option.
+For SMT solvers and ToFoF-E, the type system is always \textit{many\_typed}.
 
 \opdefault{monomorphize\_limit}{int}{\upshape 4}
 Specifies the maximum number of iterations for the monomorphization fixpoint