document new type system syntax
authorblanchet
Sun May 01 18:37:25 2011 +0200 (2011-05-01)
changeset 425826321d0dc3d72
parent 42581 398fff2c6b8f
child 42583 84b134118616
document new type system syntax
NEWS
doc-src/Sledgehammer/sledgehammer.tex
     1.1 --- a/NEWS	Sun May 01 18:37:25 2011 +0200
     1.2 +++ b/NEWS	Sun May 01 18:37:25 2011 +0200
     1.3 @@ -60,7 +60,9 @@
     1.4  * Sledgehammer:
     1.5    - sledgehammer available_provers ~> sledgehammer supported_provers
     1.6      INCOMPATIBILITY.
     1.7 -  - Added "monomorphize", "monomorphize_limit", and "type_sys" options.
     1.8 +  - Added support for SNARK and ToFoF-E on SystemOnTPTP and for simply typed
     1.9 +    TPTP problems (TFF).
    1.10 +  - Added "type_sys" and "monomorphize_limit" options.
    1.11  
    1.12  * "try":
    1.13    - Added "simp:", "intro:", and "elim:" options.
     2.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Sun May 01 18:37:25 2011 +0200
     2.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Sun May 01 18:37:25 2011 +0200
     2.3 @@ -571,37 +571,67 @@
     2.4  following values:
     2.5  
     2.6  \begin{enum}
     2.7 -\item[$\bullet$] \textbf{\textit{tags}:} Each term (and subterm) is tagged with
     2.8 -its type.
     2.9 -
    2.10 -\item[$\bullet$] \textbf{\textit{args}:} Constants are annotated with
    2.11 -their type parameters, which are passed as extra arguments.
    2.12 -
    2.13 -\item[$\bullet$] \textbf{\textit{mangled}:} Types are mangled in constant names.
    2.14 -This value implicitly enables \textit{monomorphize}.
    2.15 -
    2.16  \item[$\bullet$] \textbf{\textit{many\_typed}:} Use the prover's support for
    2.17  many-typed first-order logic if available; otherwise, fall back on
    2.18 -\textit{mangled}. This value implicitly enables \textit{monomorphize}.
    2.19 +\textit{mangled}. The problem is monomorphized, meaning that the problem's type
    2.20 +variables are instantiated with heuristically chosen ground types.
    2.21 +Monomorphization can simplify reasoning but also leads to larger fact bases,
    2.22 +which can slow down the ATPs.
    2.23 +
    2.24 +\item[$\bullet$] \textbf{\textit{mangled}:} Types are mangled in constant names,
    2.25 +and predicates restrict the range of bound variables. The problem is
    2.26 +monomorphized. This corresponds to the traditional encoding of types in an
    2.27 +untyped logic without overloading (e.g., such as performed by the ToFoF-E
    2.28 +wrapper).
    2.29 +
    2.30 +\item[$\bullet$] \textbf{\textit{args}:} Constants are annotated with their
    2.31 +types, which are supplied as extra arguments.
    2.32 +
    2.33 +\item[$\bullet$] \textbf{\textit{mono\_args}:} Similar to \textit{args}, but
    2.34 +the problem is additionally monomorphized.
    2.35 +
    2.36 +\item[$\bullet$] \textbf{\textit{tags}:} Each term (and subterm) is tagged with
    2.37 +its type using a special uninterpreted function symbol.
    2.38 +
    2.39 +\item[$\bullet$] \textbf{\textit{mono\_tags}:} Similar to \textit{tags}, but
    2.40 +the problem is additionally monomorphized.
    2.41  
    2.42  \item[$\bullet$] \textbf{\textit{none}:} No type information is supplied to the
    2.43 -ATP. This value is ignored if \textit{full\_types} is enabled.
    2.44 +ATP.
    2.45 +
    2.46 +\item[$\bullet$]
    2.47 +\textbf{%
    2.48 +\textit{many\_typed}!,
    2.49 +\textit{mangled}!,
    2.50 +\textit{args}!,
    2.51 +\textit{mono\_args}!,
    2.52 +\textit{tags}!, \\ %% TYPESETTING
    2.53 +\textit{mono\_tags}!:}
    2.54 +The type systems \textit{many\_typed}, \textit{mangled},
    2.55 +(\textit{mono\_})\allowbreak\textit{args}, and
    2.56 +(\textit{mono\_})\allowbreak\textit{tags} are fully typed and (virtually) sound.
    2.57 +For each of these, Sledgehammer also provides a mildly unsound variant
    2.58 +identified by one exclamation mark suffix (!).
    2.59 +
    2.60 +\item[$\bullet$]
    2.61 +\textbf{%
    2.62 +\textit{many\_typed}!!,
    2.63 +\textit{mangled}!!,
    2.64 +\textit{args}!!,
    2.65 +\textit{mono\_args}!!,
    2.66 +\textit{tags}!!, \\ %% TYPESETTING
    2.67 +\textit{mono\_tags}!!:}
    2.68 +More strongly unsound variants of \textit{many\_typed}, \textit{mangled},
    2.69 +(\textit{mono\_})\allowbreak\textit{args}, and
    2.70 +(\textit{mono\_})\allowbreak\textit{tags}, identified by two exclamation marks
    2.71 +(!!).
    2.72  
    2.73  \item[$\bullet$] \textbf{\textit{smart}:} If \textit{full\_types} is enabled,
    2.74 -this is the same as \textit{tags}; otherwise, this is the
    2.75 -same as \textit{args}.
    2.76 +uses a fully typed encoding; otherwise, uses a partially typed encoding. The
    2.77 +actual encoding used depends on the ATP.
    2.78  \end{enum}
    2.79  
    2.80 -For SMT solvers, the type system is always \textit{many\_typed}.
    2.81 -
    2.82 -\opfalse{monomorphize}{dont\_monomorphize}
    2.83 -Specifies whether the relevant facts should be monomorphized---i.e., whether
    2.84 -their type variables should be instantiated with relevant ground types.
    2.85 -Monomorphization is always performed for SMT solvers, irrespective of this
    2.86 -option. Monomorphization can simplify reasoning but also leads to larger fact
    2.87 -bases, which can slow down the ATPs. If the type system is \textit{mangled} or
    2.88 -\textit{many\_typed}, monomorphization is implicitly enabled irrespective of
    2.89 -this option.
    2.90 +For SMT solvers and ToFoF-E, the type system is always \textit{many\_typed}.
    2.91  
    2.92  \opdefault{monomorphize\_limit}{int}{\upshape 4}
    2.93  Specifies the maximum number of iterations for the monomorphization fixpoint