Geoff Sutcliffe
University of Miami geoff[@]cs.miami.edu
Introduction
The syntax for simply typed first order form, and typed higher order form,
is now reasonably stable.
The THF is now in use by a few people, including Chris Benzmueller and
Viktor Kunak.
No-one is using the TFF syntax, but if the SPASS people ever get off the
DFG horse maybe they'll find it appropriate.
Some further information about the simply typed first order form is available
from the
original proposal with Koen Claessen.
There have been a few improvements to the THF syntax since its first release,
and the latest version is given at the end of this document.
A key change was motivated by Florian Rabe, to relax the syntax somewhat
so that it is easier to use, but makes more nonsense syntactically legal.
The final goal is to add THF problems to the TPTP, as proposed by
Chris Benzmueller and Chad Brown in
this TPHOLs paper.
Is this all too Overwhelming?
The combined THF, TFF, FOF, and CNF syntax is quite large.
In order to make it more managable I plan to split it into pieces:
A base syntax, which includes the FOF and CNF components, and common
elements.
A TFF extension, which can be added to the base
A THF extension, which can be added to the base
Status wrt Semantics
While FOL semantics is simple and standard, in HOL there are
alternative semantics, e.g., standard semantics, Henkin semantics,
non-extensional semantics, etc.
A full discussion is in
this JSL paper by Chris Benzmueller, Chad Brown, and Michael Kohlhase.
Different semantics lead to different
(SZS) statuses for problems.
The TPTP syntax (original and THF) does not provide any way of regording
these alternatives.
Generally, the THF needs ways of specifying the semantics information.
This requires a simple extension of the header section conventions for
TPTP problem files.
Question: Does a THF ATP system need to know the semantics wrt which the user
wants an answer?
If so, this information will have to be specified, but it seems most likely
to be a command line option for the system rather than a statement in the
problem.
Libraries of Axioms
Just like for the FOF and CNF cases, there is a need for someone to
develop librarues of THF axioms that can be used in THF problems.
Viktor Kunak has sugggested that the most important things are:
sets and relations
transitive closure
inductive definitions
integers
algebraic data types, sequences
Looking at e.g. Isabelle or HOL libraries, would be a good starting point.
%----v3.2.0.10 (TPTP version.internal development number)
%------------------------------------------------------------------------------
%----README ... this header provides important meta- and usage information
%----
%----Intended uses of the various parts of the TPTP syntax are explained
%----in the TPTP technical manual, linked from www.tptp.org.
%----
%----Four kinds of separators are used, to indicate different types of rules:
%---- ::= is used for regular grammar rules, for syntactic parsing.
%---- :== is used for semantic grammar rules. These define specific values
%---- that make semantic sense when more general syntactic rules apply.
%---- ::- is used for rules that produce tokens.
%---- ::: is used for rules that define character classes used in the
%---- construction of tokens.
%----
%----White space may occur between any two tokens. White space is not specified
%----in the grammar, but there are some restrictions to ensure that the grammar
%----is compatible with standard Prolog: a should be readable with
%----read/1.
%----
%----The syntax of comments is defined by the rule. Comments may
%----occur between any two tokens, but do not act as white space. Comments
%----will normally be discarded at the lexical level, but may be processed
%----by systems that understand them (e.g., if the system comment convention
%----is followed).
%------------------------------------------------------------------------------
%----Files. Empty file is OK.
::= *
::= |
%----Formula records
::= | | |
%----Future languages may include ... english | efof | tfof | mathml | ...
::= thf(,,).
::= tff(,,).
::= fof(,,).
::= cnf(,,).
::= | ,
%----In derivations the annotated formulae names must be unique, so that
%----parent references (see ) are unambiguous.
%----Types for problems.
%----Note: The previous from ...
%---- ::= -
%----... is now gone. Parsers may choose to be tolerant of it for backwards
%----compatibility.
::= :== axiom | hypothesis | definition | lemma | theorem |
conjecture | negated_conjecture | plain | fi_domain |
fi_functors | fi_predicates | type | unknown
%----"axiom"s are accepted, without proof, as a basis for proving "conjecture"s
%----in FOF problems. In CNF problems "axiom"s are accepted as part of the set
%----whose satisfiability has to be established. There is no guarantee that the
%----axioms of a problem are consistent.
%----"hypothesis"s are assumed to be true for a particular problem, and are
%----used like "axiom"s.
%----"definition"s are used to define symbols, and are used like "axiom"s.
%----See for details of thf usage.
%----"lemma"s and "theorem"s have been proven from the "axiom"s, can be used
%----like "axiom"s, but are redundant wrt the "axiom"s. A problem containing
%----a non-redundant "lemma" or theorem" is ill-formed. "theorem"s are more
%----important than "lemma"s from the user perspective.
%----"conjecture"s occur in only FOF problems, and all are to be proven from
%----the "axiom"(-like) formulae. A problem is solved only when all
%----"conjecture"s are proven.
%----"negated_conjecture"s occur in only CNF problems, and are formed from
%----negation of a "conjecture" in a FOF to CNF conversion.
%----"plain"s have no special user semantics, and can be used like "axiom"s.
%----"fi_domain", "fi_functors", and "fi_predicates" are used to record the
%----domain, interpretation of functors, and interpretation of predicates, for
%----a finite interpretation.
%----"type" defines the type globally for one symbol; treat as $true.
%----"unknown"s have unknown role, and this is an error situation.
%------------------------------------------------------------------------------
%----THF formulae. All formulae must be closed.
::= | ::= | ::= | |
%----Only some binary connectives can be written without ()s.
%----There's no precedence among binary connectives
::= ::= | =
%----Associative connectives & and | are in .
::= | |
::= |
::= & |
& ::= @ |
@ ::= | @
%---- are in ()s or do not have a
%----at the top level. Essentially, a is any
%----lambda expression that "has enough parentheses" to be used inside
%----a larger lambda expression. However, lambda notation might not be used.
::= | |
| | () |
| ()
::= [] :
::= ! | ?
%----@ (denoting apply) is left-associative and lambda is right-associative.
%----$lambda [X] : $lambda [Y] : f @ g (where f is a
%----and g is a ) should be parsed as:
%----($lambda [X] : ($lambda [Y] : f)) @ g.
%----That is, g is not in the scope of either $lambda.
::= [] :
::= $lambda | ^
::= | , ::= | ::= :
%----Unary connectives bind more tightly than binary
::= ::=
%----THF atoms
::= | ::= : ::= | () | ::= :== |
%----If the entire formula is a , it should be treated as an
%----assertion that the atom is in this type, globally. If a thf_typed_atom>
%----appears inside a larger expression, it is presently unspecified what the
%----scope of this type declaration is. Users producing such formulas should
%----be sure to clarify their intent; ad-hoc polymorphism and subtyping are
%----two of several possibilities.
%----thf_tuple is really the "pair" function of lambda calculus, so it
%----should be right-associative. It is also "cons" in Lisp.
%----So "(U, V)" is "syntactic sugar" for "lambda [X]: (X @ U @ V)".
%----Some useful functions to work with tuples might be:
%----"first := $lambda [E]: (E @ $lambda [F, R]: F)" and
%----"rest := $lambda [E]: (E @ $lambda [F, R]: R)".
%----Then "(first @ (U, V)) = U" and "(rest @ (U, V)) = V" are valid.
%---- is not a because it would confuse Prolog
%----if it appeared at top level without parentheses.
::= , |
,
%----If "name := expr" is the entire formula, it has global scope, i.e., the
%----entire input. If "name := expr" is in the context of a $letrec, e.g.,
%----"$letrec [name1 := expr1, name2 := expr2, ...] : formula" (where the
%----symbols "name1", "name2", ... normally appear in "formula", and might
%----appear in "expr1", "expr2", ...), each occurrence of namei" should be
%----replaced by "expri" within "formula", but not elsewhere, i.e., "formula"
%----is the scope of the definition. For "cascading" definitions use
%----"$letrec [a := b]: $letrec [c := d]: e". As a formula a thf_definition>
%----evaluates to true.
::= [] : ::= |
, ::= := |
()
::= $letrec | :=
%---- appears after ":", where a type is being specified
%----for a constant or variable (or other expression, in the future), or
%----within a larger . However, this is just for readability,
%----and expands simply to thf_unitary_formula>, so the
%----syntax allows just about any lambda expression with "enough" parentheses
%----to serve as a type. The expected use of this flexibility is parametric
%----polymorphism in types, expressed with lambda abstraction:
%---- list := ^ [T]: ((T * (list @ T)) + (emptylist @ T))
%---- ! [L : (list @ int)]: $let [sum := ^ [L1]: ...] : .
%----If a that looks like a type appears in the function
%----position of an apply formula, it is considered to be a function into bool
%----that is true exactly when its parameter is of the type denoted by the
%----, e.g., ((nat -> nat) @ fibonacci) might evaluate to
%----$true.
%---- is right-associative: o->o->o means o->(o->o).
%---- is left-associative: o * o * o means (o * o) * o.
%---- is left-associative: o + o + o means (o + o) + o.
::= ::= | |
::= |
::= |
::= |
::= -> | >
%------------------------------------------------------------------------------
%----TFF formulae. All formulae must be closed.
%----TFF is like FOF except that predicate and function symbols must be typed
%----exactly once at top level (with formula role "type"), and variables must
%----be typed when they are bound in quantifier lists. atomic_formula>s are
%----just like FOF. See the porposal linked from the TPTP web page for details
%----of the semantics.
::= | ::= | ::= | ::= ::= | ::= *
::= ::= & *
::= & ::= | |
| ()
::= [] :
::= | , ::= : ::=
%---- can appear only at top level, unlike in THF.
::= : |
()
::= |
%----The types of the