The TPTP world is a well established infrastructure that supports research, development, and deployment of Automated Theorem Proving systems for classical logics. The TPTP language is one of the keys to the success of the TPTP world. Originally the TPTP world supported only first-order clause normal form (CNF). Over the years support for full first-order form (FOF), monomorphic typed first-order form (TF0), rank-1 polymorphic typed first-order form (TF1), monomorphic typed higher-order form (TH0), and rank-1 polymorphic typed higherorder form (TH1), have been added. TF0 and TF1 together form the TFF language family; TH0 and TH1 together form the THF language family. This paper introduces the eXtended Typed First-order form (TFX), which extends TFF to include boolean terms, tuples, conditional expressions, and let expressions.
The TPTP world [
The TPTP language is one of the keys to the success of the TPTP world. The
language is used for writing both TPTP problems and TSTP solutions, which
enables convenient communication between different systems and researchers.
Originally the TPTP world supported only first-order clause normal form (CNF)
[
Since the inception of TFF there have been some features that have received
little use, and hence little attention. In particular, tuples, conditional expressions
(if-then-else), and let expressions (let-defn-in) were neglected, and the latter two
were horribly formulated with variants to distinguish between their use as
formulae and terms. Recently, conditional expressions and let expressions have
become more important because of their use in software verification applications.
In an independent development, Evgenii Kotelnikov et al. introduced FOOL [
The TPTP’s new eXtended Typed First-order form (TFX) language remedies the old weaknesses of TFF, and incorporates the features of FOOL. This has been achieved by conflating (with some exceptions) formulae and terms, removing tuples from plain TFF, including fully expressive tuples in TFX, removing the old conditional expressions and let expressions from TFF, and including new elegant forms of conditional expressions and let expressions as part of TFX. (These more elegant forms have been mirrored in THF, but that is not a topic of this paper.) TFX is a superset of the revised TFF language. This paper describes the extensions to the TFF language form that define the TFX language. The remainder of this paper is organized as follows: Section 2 reviews the TFF language, and describes FOOL. Section 3 provides technical and syntax details of the new features of TFX. Section 4 describes the evolving software support for TFX, and provides some examples that illustrate its use. Section 5 concludes. 2
The TPTP language is a human-readable, easily machine-parsable, flexible and extensible language, suitable for writing both ATP problems and solutions. The top level building blocks of the TPTP language are annotated formulae. An annotated formula has the form language(name, role, formula, source, useful_info). The languages supported are clause normal form (cnf), first-order form (fof), typed first-order form (tff), and typed higher-order form (thf). The role, e.g., axiom, lemma, conjecture, defines the use of the formula in an ATP system. In the formula, terms and atoms follow Prolog conventions, i.e., functions and predicates start with a lowercase letter or are ’single quoted’, variables start with an uppercase letter, and all contain only alphanumeric characters and underscore. The TPTP language also supports interpreted symbols, which either start with a $, or are composed of non-alphanumeric characters, e.g., the truth constants $true and $false, and integer/rational/real numbers such as 27, 43=92, 99:66. The logical connectives are !, ?, ~, |, &, =>, <=, <=>, and <~>, for 8, 9, :, _, ^, ), (, ,, and respectively. Equality and inequality are expressed as the infix operators = and !=. The following is an example of an annotated first-order formula, supplied from a file. fof(union,axiom, ! [X,A,B] :
( member(X,union(A,B)) <=> ( member(X,A)
| member(X,B) ) ), file(’SET006+0.ax’,union), [description(’Definition of union’),relevance(0.9)]). 2.1
TFF extends the FOF language with types and type declarations. The TF0 variant is monomorphic, and the TF1 variant is rank-1 polymorphic. Every function and predicate symbol is declared before its use with a type signature that specifies the types of the symbol’s arguments and result. Each TF0 type is one of – the predefined types $i for (individuals) and $o for o (booleans); – the predefined arithmetic types $int (integers), $rat (rationals), and $real (reals); or – user-defined types (constants).
User defined types are declared before their use to be of the kind $tType, in annotated formulae with the type role - see Figure 1 for examples. Each TF0 type signature declares either – an individual type ; or – a function type ( 1 * * n) > ~ for n > 0, where i are the argument types, and ~ is the result type.
The type signatures of uninterpreted symbols are declared like types, in
annotated formulae with the type role - see Figure 1 for examples. The type of =
and != is ad hoc polymorphic over all types except $o (this restriction is lifted
in TFX), with both arguments having the same type and the result type being
$o. The types of arithmetic predicates and functions are ad hoc polymorphic
over the arithmetic types; see [
The polymorphic TF1 extends TF0 with (user-defined) type constructors, type variables, polymorphic symbols, and a new binder. Each TF1 type is one of – the predefined types $i and $o; – the predefined arithmetic types $int, $rat, and $real; – user-defined n-ary type constructors applied to n type arguments; or – type variables, which must be quantified by !> - see the type signature forms below.
Type constructors are declared in annotated formulae with a type role before their use, to be of the kind ($tType * * $tType) > $tType. Each TF1 type signature declares either – an individual type ; – a function type ( 1 * * n) > ~ for n > 0, where i are the argument types and ~ is the result type; or – a polymorphic type !>[ 1: $tType, : : : , n: $tType]: & for n > 0, where 1; : : : ; n are distinct type variables and & is a TF0 type signature.
The !> binder in the last form denotes universal quantification in the style
of calculi. It is used only at the top level in polymorphic type signatures. All
type variables must be of type $tType; more complex type variables are beyond
rank-1 polymorphism. An example of TF1 formulae can be found in [
FOOL [
FOOL contains an interpreted two-element boolean type bool , allows quantification over variables of type bool , and considers formulae to be terms of type bool . This allows boolean variables to be used as formulae, and all formulae to be used as boolean terms. For example, Formula 1 is a syntactically correct tautology in FOOL.
(8x : bool )(x _ :x) Logical implication can be defined as a binary function imply of the type bool bool ! bool using the axiom
(8x : bool )(8y : bool )(imply (x; y) , :x _ y): A graph P of a (partial) function of the type !
can be expressed as (8x : )(8y : )(8z : )imply (P (x; y) ^ P (x; z); y = z) (1) (2) (3) Formula 2 can be equivalently written with = instead of ,.
FOOL extended with the theory of tuples contains a type ( 1; : : : ; n) of the nary tuple for all types 1; : : : ; n, n > 0. Each type ( 1; : : : ; n) is first class, that is, it can be used in the type of a function or predicate symbol, and in a quantifier. An expression (t1; : : : ; tn), where t1; : : : ; tn are terms of types 1; : : : ; n, respectively, is a tuple term of type ( 1; : : : ; n). Each tuple term is first class and can be used as an argument to a function symbol, a predicate symbol, or equality.
Tuples are ubiquitous in mathematics and programming languages. For example, one can use the tuple type (R; R) as the type of complex numbers. Thus the term (2; 3) represents the complex number 2+3i. A function symbol plus that represents addition of complex numbers has the type (R; R) (R; R) ! (R; R).
FOOL contains conditional expressions of the form if then s else t, where is a formula, and s and t are terms of the same type. The semantics of such expressions mirrors the semantics of conditional expressions in programming languages, and they are therefore convenient for expressing formulae coming from program analysis. For example, consider the max function of the type Z Z ! Z that returns the maximum of its arguments. Its definition can be expressed in FOOL as (8x : Z)(8y : Z)(max (x; y) = if x y then x else y): (4)
FOOL allows conditional expressions to occur as formulae, as in the following valid property of max .
(8x : Z)(8y : Z)(if max (x; y) = x then x y else y x) (5)
FOOL contains let expressions of the form let D1; : : : ; Dk in t, where k > 0, t is either a term or a formula, and D1; : : : ; Dk are simultaneous non-recursive definitions. FOOL allows definitions of function symbols, predicate symbols, and tuples.
The definition of a function symbol f : 1 : : : n ! has the form f (x1 : 1; : : : ; xn : n) = s, where n 0, x1; : : : ; xn are distinct variables, and s is a term of the type . For example, the following denotes the maximum of three integer constants a, b, and c, using a local definition of the function symbol max .
let max (x : Z; y : Z) = if x
y then x else y in max (max (a; b); c)
The definition of a predicate symbol p : 1 : : : n ! bool has the form p(x1 : 1; : : : ; xn : n) = ', where n 0, x1; : : : ; xn are distinct variables, and ' is a formula. For example, the following denotes equivalence of two boolean constants A and B, using a local definition of the predicate symbol imply . let imply (x : bool ; y : bool ) = :x _ y
in imply (A; B) ^ imply (B; A)
The definition of a tuple has the form (c1; : : : ; cn) = s, where n > 1, c1; : : : ; cn are distinct constant symbols of the types 1; : : : ; n, respectively, and s is a term of the type ( 1; : : : ; n). For example, the following defines addition for complex numbers using two simultaneous local definition of tuples.
(8x : (R; R))(8y : (R; R))
(plus(x; y) = let (a; b) = x; (c; d) = y in (a + c; b + d))
The semantics of let expressions in FOOL mirrors the semantics of simultaneous non-recursive local definitions in programming languages. That is, none (6) (7) (8) of the definitions D1; : : : ; Dn uses function or predicate symbols created by any other definition. In the following example, constants a and b are swapped by a let expression, and the formula is equivalent to P (b; a).
let a = b ; b = a in P (a; b) let (a; b) = (b; a) in P (a; b)
Formula 9 can be equivalently expressed by the following let expression with a definition of a tuple. (9) (10)
Let expressions with tuple definitions are convenient for expressing problems
coming from program analysis, namely modelling of assignments [
if (x > y) { t := x; x := y; y := t; } assert x <= y; let (x; y; t) = if x > y then let t = x in let x = y in let y = t in
(x; y; t) else (x; y; t) in x
y The TPTP TFX syntax extends the TFF syntax to provide the features of FOOL, and at the same time some of the previous weaknesses of plain TFF have been remedied. Formulae and terms have been conflated (with some exceptions). Tuples have been removed from TFF, and fully expressive tuples included in TFX. The old conditional expressions and let expressions have been removed from TFF, and new elegant forms have been included as part of TFX. The grammar of TFX is captured in version v7.1.0.2 of the TPTP syntax, available online at http://www.tptp.org/TPTP/SyntaxBNF.html. In the subsections below, the relevant excerpts of the BNF are provided, with examples and commentary. 3.1
Variables of type $o can be used as formulae, and formulae can be used as terms. The following is the relevant BNF excerpt. Formulae and terms are conflated by including logic/atomic formulae as options for terms/unitary terms. The distinction between formulae and terms is maintained for plain TFF. tff(tautology,conjecture, ! [X: $o]: (X | ~X) ).
The imply predicate in Formula 2 can be written in TFX as tff(imply_type,type,imply: ($o * $o) > $o ). tff(imply_defn,axiom,
! [X: $o,Y: $o]: (imply(X,Y) <=> (~X | Y)) ).
The definition of a graph of a function in Formula 3 can be written in TFX as tff(s,type,s: $tType). tff(t,type,t: $tType). tff(p,type,p: (s * t) > $o ). tff(graph,axiom,
! [X: s,Y: t,Z: s] : imply(p(X,Y) & p(X,Z),Y = Z) ).
A consequence of allowing formulae as terms is that the default typing of functions and predicates supported in plain TFF (functions default to ($i * ...* $i) > $i and predicates default to ($i * ...* $i) > $o) is not supported in TFX.
Note that not all terms can be used as formulae. Tuples, numbers, and “distinct objects” cannot be used as formulae. 3.2
Tuples in TFX are written in [] brackets, and can contain any type of term, including formulae and variables of type $o. Signatures can contain tuple types. The following is the relevant BNF excerpt. <tfx_tuple_type> <tff_type_list> <tfx_tuple> <tff_arguments> ::= [<tff_type_list>] ::= <tff_top_level_type> |
<tff_top_level_type>,<tff_type_list> ::= [] | [<tff_arguments>] ::= <tff_term> | <tff_term>,<tff_arguments>
The tuple type (R; R) can be written in the TFX syntax as [$real,$real]
and the type of addition for complex numbers (R; R) (R; R) ! (R; R) can be
written as ([$real,$real] * [$real,$real]) > [$real,$real]. The tuple
term (2; 3) can be written as [
! [X: $int] : p([33,me,$true],! [Y: $i] : q(X,Y),27) ).
While product types and tuple types are semantically equivalent, the two separate syntaxes make it easy to distinguish between the following cases. tff(n_type,type,n: [$int,$int]). tff(f_type,type,f: [$int,$int] > $int). tff(g_type,type,g: ($int * $int) > $int). tff(h_type,type,h: ([$int,$int] * $int) > $int).
The first case defines n to be a tuple of two integers. The second case defines f to be a function from a tuple of two integers to an integer. The third case defines g to be a function from two integers to an integer. The last case defines h to be a function from a tuple of two integers and an integer, to an integer.
The tuple syntax cannot be used to simultaneously declare types of multiple constants in an annotated formula with the type role. For example, the following expression is not valid. tff(ab_type,type,[a,b]: [$int,$int]).
Instead, one must declare the type of each constant separately. tff(a_type,type,a: $int). tff(b_type,type,b: $int). 3.3
Conditional expressions are polymorphic, taking a formula as the first argument, then two formulae or terms of the same type as the second and third arguments. The type of the conditional expression is the type of its second and third arguments. The following is the relevant BNF excerpt. <tfx_conditional>
::= $ite(<tff_logic_formula>,<tff_term>,<tff_term>)
The keyword $ite is used for conditional expressions occurring both as terms and formulae, which is different from the old TFF syntax of if-then-else that contained two separate keywords $ite_t and $ite_f.
The definition and a property of the max function in Formulae 4 and 5 can be expressed in TFX as tff(max_type,type,max: ($int * $int) > $int). tff(max_defn,axiom,
! [X: $int,Y: $int]: max(X,Y) = $ite($greatereq(X,Y),X,Y) ). tff(max_property,conjecture, ! [X: $int,Y: $int]:
$ite(max(X,Y) = X,$greatereq(X,Y),$greatereq(Y,X)) ). 3.4
Let expressions in TFX contain (i) the type signatures of locally defined symbols; (ii) the definitions of the symbols; and (iii) the term or formula in which the definitions are used. The syntax of type signatures in let expressions is the same as for top-level type declrations. The definitions specify how the locally defined symbols are expanded in the term or formulae where they are used. The type signature must include the types for all the local defined symbols. The following is the relevant BNF excerpt. <tfx_let> ::= $let(<tfx_let_types>,<tfx_let_defns>,<tff_term>) <tfx_let_types> ::= <tff_atom_typing> | [<tff_atom_typing_list>] <tff_atom_typing_list> ::= <tff_atom_typing> |
<tff_atom_typing>,<tff_atom_typing_list> <tfx_let_defns> ::= <tfx_let_defn> | [<tfx_let_defn_list>] <tfx_let_defn> ::= <tfx_let_LHS> <assignment> <tff_term> <tfx_let_LHS> ::= <tff_plain_atomic> | <tfx_tuple> <tfx_let_defn_list> ::= <tfx_let_defn> | <tfx_let_defn>,<tfx_let_defn_list>
The keyword $let is used for let expressions defining both function and predicate symbols, regardless of whether the let expression occurs as a term or a formula. This is different from the old TFF syntax of let expressions that contained four separate keywords $let_tt, $let_tf, $let_ft, and $let_ff.
In the following example an integer constant c is defined in a let expression. tff(p_type,type,p: ($int * $int) > $o ). tff(let_1,axiom,$let(c: $int,c:= $sum(2,3),p(c,c)) ).
The left hand side of a definition may contain pairwise distinct variables as top-level arguments of the defined symbol, and the variables can (typically do) also appear in the right hand side of the definition. Such variables are implicitly universally quantified, and are of the type defined by the symbol’s type signature. The variables’ values are supplied by unification in the defined symbol’s use. For example, the let expression for the maximum of three integers in Formula 4 can be expressed in TFX as tff(a_type,type,a: $int). tff(b_type,type,b: $int). tff(c_type,type,c: $int). tff(p_type,type,p: $int > $o ). tff(max_max,axiom, $let(max: ($int * $int) > $int, max(X,Y):= $ite($greatereq(X,Y),X,Y), p(max(max(a,b),c)) ) ). and the let expression for the equivalence of two boolean constants in Formula 7 can be expressed in TFX as tff(p,type,p: $o). tff(q,type,q: $o). tff(p_eq_q,axiom, $let(imply: ($o * $o) > $o, imply(X,Y):= ~X | Y, imply(p,q) & imply(q,p)) ).
Let expressions can use definitions of tuples. Formula 8 can be written in TFX as follows. Notice that the let expression’s type declarations contain the elements of both tuples in the simultaneous definition. tff(plus,type,
plus: ([$real,$real] * [$real,$real]) > [$real,$real]). tff(plus_def,axiom, ! [X: [$real,$real],Y: [$real$,$real]] : ( plus(X,Y) = $let([a: $real,b: $real,c: $real,d: $real], [[a,b]:= X, [c,d]:= Y], [$sum(a,c),$sum(b,d)]) ).
Sequential let expressions (let*) can be implemented by nesting let expressions. In the following example ff and gg are defined in sequence, and the let expression is equivalent to p(f(i,i,i,i)). tff(i_type,type,i: $int). tff(f_type,type,f: ($int * $int * $int * $int) > $int). tff(p_type,type,p: $int > $o ). tff(let_tuple_3,axiom, $let(ff: ($int * $int) > $int, ff(X,Y):= f(X,X,Y,Y), $let(gg: $int > $int, gg(Z):= ff(Z,Z), p(gg(i)) ) ) ).
Let expressions can have simultaneous local definitions with the type declarations and the definitions given in []s (they look like tuples of declarations and definitions, but are specified independently of tuples in the syntax). The symbols must have distinct signatures. For example, the let expression to swap two constants in Formula 9 can be expressed in TFX as tff(a,type,a: $i). tff(b,type,b: $i). tff(p,type,p: ($i * $i) > $o). tff(pba,axiom, $let([a: $i,b: $i], [a:= b, b:= a], p(a,b))). and the equivalent let expression using a tuple in Formula 10 can be expressed in TFX as tff(a,type,a: $i). tff(b,type,b: $i). tff(p,type,p: ($i * $i) > $o). tff(pba,axiom, $let([a: $i,b: $i], [a,b]:= [b,a], p(a,b))).
In the following example two function symbols are defined simultaneously, and the let expression is equivalent to p(f(i,i,f(i,i,i,i),f(i,i,i,i))). tff(i_type,type,i: $int). tff(f_type,type,f: ($int * $int * $int * $int) > $int). tff(p_type,type,p: $int > $o ). tff(let_tuple_2,axiom, $let([ff: ($int * $int) > $int, gg: $int > $int], [ff(X,Y):= f(X,X,Y,Y), gg(Z):= f(Z,Z,Z,Z)], p(ff(i,gg(i)))) ).
The defined symbols of a let expression have scope over the formula or term in which the definitions are applied, shadowing any definition outside the let expression. The right hand side of a definition can have symbols with the same name as the defined symbol, but refer to symbols defined outside the let expression. In the following example the local definition of the array function symbol shadows the global declaration. tff(array_type,type,array: $int > $real). tff(p_type,type,p: $real > $o). tff(let_3,axiom, $let(array: $int > $real, array(I):= $ite(I = 3,5.2,array(I)), p($sum(array(2),array(3))) ) ).
The BNF that defines TFX (and all the TPTP languages) provides the basis for the BNFParser family of automatically generated lex/yacc parsers for TPTP files. The parsers are available through the SystemB4TPTP online interface at http://www.tptp.org/cgi-bin/SystemB4TPTP. At the time of writing this paper, the TPTP4X utility is being upgraded to support TFX.
The Vampire theorem prover [
TFX has been used by the program verification tools BLT [
This paper has introduced the eXtended Typed First-order form (TFX) of the TPTP’s TFF language. TFX includes boolean variables as formulae, formulae as terms, tuple types and terms, conditional expressions, and let expressions. 3 https://github.com/vprover/vampire %----------------------------------------------------------------------tff(x,type,x:$int). tff(y,type,y:$int). tff(t,type,t:$int). tff(x_leq_y,conjecture, $let([x: $int,y: $int,t: $int], [x,y,t] := $ite($greater(x,y), $let(t: $int, t := x, $let(x: $int, x := y, $let(y:$int, y := t, [x,y,t]))), %----------------------------------------------------------------------tff(a_type,type, a: $i ). tff(b_type,type, b: $i ). tff(c_type,type, c: $i ). tff(exactly_one_truthteller_type,type, exactly_one_truthteller: $o ). tff(says,type, says: ( $i * $o ) > $o ). %----Each person is either a truthteller or a liar tff(island,axiom, ! [P: $i] : ( says(P,$true) <~> says(P,$false) ) ). tff(exactly_one_truthteller,axiom,
( exactly_one_truthteller <=> ( ? [P: $i] : says(P,$true) & ! [P1: $i,P2: $i] : ( ( says(P1,$true) & says(P2,$true) ) => P1 = P2 ) ) )). %----B said that A said that there is exactly one truthteller tff(b_says,hypothesis, says(b,says(a,exactly_one_truthteller)) ). %----C said that what B said is false tff(c_says,hypothesis, says(c,says(b,$false)) ). %----------------------------------------------------------------------TFX is useful for (at least) concisely expressing problems coming from program analysis, and translated from more expressive logics.
Now that the syntax is settled, ATP system developers will be able to implement the new language features. It is already apparent from the SMT community that these are useful features, and systems that can already parse and reason using the SMT version 2 language need only new parsers to implement the features of TFX. In parallel, version v8.0.0 of the TPTP will include problems that use TFX, and the automated reasoning community is invited to submit problems for inclusion in the TPTP.
Acknowledgements. Thanks to our friends in the TPTP World who have provided feedback on TFX features, starting from the TPTP Tea Party at CADE-22 in 2009. The second author was partially supported by the Wallenberg Academy Fellowship 2014 and the Swedish VR grant D0497701.