In a separate development, Evgeny Kotelnikov introduced the FOOL logic, which extends TFF to allow boolean terms. This logic can be automatically translated to first-order logic. It has is also useful in software verification applications.

This document describes a new TPTP language form - Typed First-order form eXtended (TFX), and changes to the THF language that correspond to decisions made for TFX.

**Boolean Terms**

Formulae are permitted as terms.
For example ...

tfx(p_type,type,p: ($i * $o * $int) > $o ). tfx(q_type,type,q: ($int * $i) > $o ). tfx(me_type,type,me: $i ). tfx(fool_1,axiom,! [X: $int] : p(me,! [Y: $i] : q(X,Y),27) ).... and ...

tfx(p_type,type,p: $i > $o ). tfx(q_type,type,p: $o > $o ). tfx(me_type,type,me: $i ). tfx(fool_2,axiom,q((~p(me)) != q(me))).Note that the

**Tuples**

Tuples in TFF are written in `[]` brackets, and can contain only
non-boolean terms; tuples of formulae have been removed from TFF.
Tuples in TFX are also written in `[]` brackets, and can contain
any type of term.
Tuples are of type `$i`.
For example ...

tfx(p_type,type,p: ($i * $o * $int) > $o ). tfx(f_type,type,q: ($int * $i) > $o ). tfx(me_type,type,me: $i ). tfx(tuples_1,axiom,! [X: $int] : p([33,me,$true],! [Y: $i] : q(X,Y),27) ).Signatures can contain tuple types. For example ...

tfx(t1_type,type,t1: $tType ). tfx(p_type,type,p: [t1,$i] > $o ). tfx(d_type,type,d: [$i,t1,$int] ). tfx(f_type,type,f: ($o * $i) > [t1,$i] ). tfx(tuples_2,axiom,p(f($true,d)) ).... and ...

tfx(a_b_type,type,[a,b]: [$int,$int] ). tfx(c_d_type,type,[c,d]: [$int,$int] ). tfx(tuples_3,axiom,[a,b] = [c,d] ).

**Conditional Expressions**

Conditional expressions are adhoc polymorphic, taking a formula as the first
argument, then two terms (of any one type) or two formulae as the second and
third arguments as the return values, i.e., the return type is the same as
that of the second and third arguments.
For example ...

tfx(p_type,type,p: $int > $o). tfx(q_type,type,q: $int > $o). tfx(ite_1,axiom,! [X:$int,Y:$int] : $ite($greater(X,Y),p(X),p(Y)) ). tfx(ite_2,axiom,! [X:$int,Y:$int] : q($ite($greater(X,Y),X,Y)) ).Tuples can be used in conditional expressions. For example ...

tfx(p_type,type,p: [$int,$int] > $o). tfx(d_type,type,d: [$int,$int]). tfx(ite_3,axiom,! [X:$int,Y:$int] : p($ite($greater(X,Y),[X,Y],[Y,X])) ). tfx(ite_4,axiom,! [X:$int,Y:$int] : (d = $ite($greater(X,Y),[X,Y],[Y,X])) ).

**Let Expressions**

Let expression provide the type of the defined symbols, definitions for
the symbols, and a formula/term (of any type) in which the let expression
applies.
For example ...

tfx(p_type,type,p: $int > $o ). tfx(let_1,axiom,$let(c: $int,c:= 27,p(c))).... would be equivalent to ...

tfx(let_1,axiom,p(27) ).The defined symbols and have scope over the formula/term in which the let expression applies, shadowing any definition outside the let expression. The RHS of a definition can have symbols with the same name as the defined symbol, but refer to symbols defined outside the let expression.

If variables are used in the definition, their values are supplied in the the defined symbol's use. Such variables do not need to be declared, but must be top-level arguments of the defined symbol, and be pairwise distinct. For example ...

tfx(i_type,type,i: $int). tfx(j_type,type,j: $int). tfx(f_type,type,f: ($int * $int * $int * $int) > $int). tfx(p_type,type,p: $int > $o ). tfx(let_2,axiom,$let(ff: ($int * $int) > $rat, ff(X,Y):= f(X,X,Y,Y), p(ff(i,j))) ).... would be equivalent to ...

tfx(let_2,axiom,p(f(i,i,j,j)) ).Tuples can be used to define multiple symbols in let expressions. For example ...

tfx(i_type,type,i: $int). tfx(f_type,type,f: ($int * $int * $int * $int) > $int). tfx(p_type,type,p: $int > $o ). tfx(let_tuple_1,axiom, $let([ff: ($int * $int) > $rat, gg: $int > $int], [ff(X,Y):= f(X,X,Y,Y), gg(Z):= f(Z,Z,Z,Z)], p(ff(i,gg(i)))) ).... would be equivalent to ...

tfx(let_tuple_1,axiom,p(f(i,i,f(i,i,i,i),f(i,i,i,i))) ).

Tuples can be used directly in let expressions. For example ...

tfx(p_type,type,p: ($int * $int) > $o ). tfx(q_type,type,q: [$int,$int] > $o ). tfx(let_tuple_2,axiom,$let([a:$int,b:$int], [a,b]:= [27,28], p(a,b)) ). tfx(let_tuple_3,axiom,$let(d: [$int,$int], d:= [27,28],q(d)) ).... would be equivalent to ...

tfx(let_tuple_2,axiom,p(27,28)) ). tfx(let_tuple_3,axiom,q([27,28])) ).An alternative equivalent version of

tfx(let_tuple_2,axiom,$let([a,b]: [$int,$int], [a,b]:= [27,28], p(a,b)) ).

Tuples, conditional expressions, and let expressions can be mixed in useful ways. For example ...

tfx(let_ite_1,axiom, $let([aa: $int,bb: $$int], [aa,bb]:= $ite($greater(aa,bb),[aa,bb],[bb,aa]), p(aa,bb))).

**Tuples**

Tuples in THF are written in `[]` brackets, and can contain any
type of expression.
Tuples are of type `$i`.
For example ...

thf(p_type,type,p: $int > $o ). thf(q_type,type,q: [$int,$int] > $i > $o ). thf(me_type,type,me: $i ). thf(tuples_1,axiom,p = ^ [Z: $int] : ( q @ [Z,Z] @ me ) ).Signatures can contain tuple types. For example ...

thf(t1_type,type,t1: $tType ). thf(p_type,type,p: [t1,$i] > $o ). thf(f_type,type,f: $o > $i > [t1,$i] ). thf(me_type,type,me: $i ). thf(tuples_2,axiom,p @ (f @ $true @ me ) ).

**Conditional Expressions**

**Let Expressions**