The TPTP Language

Table of Contents

• Annotated Formulae
• The Type System
• The Arithmetic System
• The Non-classical Logics
• Hyperlinked BNF

TLA	Logic	Symbol	Variants
PRP	PRoPositional	fof
CNF	Clause Normal Form	cnf
FOF	First-Order Form	fof
TFF	Typed First-order Form	tff	TF0 - monomorphic; TF1 - polymorphic
TXF	Typed eXtended first-order Form	tff	TX0 - monomorphic; TX1 - polymorphic
THF	Typed Higher-order Form	thf	TH0 - monomorphic; TH1 - polymorphic
DHF	Dependently typed Higher-order Form	thf	DH0 - monomorphic; DH1 - polymorphic
NXF	Non-classical typed eXtended first-order Form	tff	TX0 - monomorphic; TX1 - polymorphic
NHF	Non-classical typed Higher-order Form	thf	NH0 - monomorphic; NH1 - polymorphic
NTF	Non-classical Typed Form	-	NXF and NHF

• The axiom-like formulae are those with the roles axiom, hypothesis, definition, assumption, lemma, theorem, and corollary. They are accepted, without proof, as a basis for proving conjectures in THF, TFF, and FOF problems. In CNF problems the axiom-like formulae are accepted as part of the set whose satisfiability has to be established. There is no guarantee that the axiom-like formulae of a problem are consistent.
• hypothesiss are assumed to be true for a particular problem.
• definitions are used to define symbols.
• assumptions must be discharged before a derivation is complete.
• lemmas and theorems have been proven from the other axiom-like formulae, and are thus redundant wrt those axiom-like formulae. theorem is used also as the role of proven conjectures, in output. A problem containing a lemma or theorem that is not redundant wrt the other axiom-like formulae is ill-formed. theorems are more important than lemmas from the user perspective.
• corollarys have been proven from the axioms and a theorem, and are thus redundant wrt the other axiom-like and theorem formulae. A problem containing a corollary that is not redundant wrt the other axiom-like formulae and theorem formulae is ill-formed.
• conjectures occur in DHF, THF, TFF, and FOF problems, and are to all be proven from the axiom-like formulae. A problem is solved only when all conjectures are proven. (TPTP problems never contain more than one conjecture, and the creation of problems with more than one conjecture is currently deprecated, because contemporary ATP systems commonly treat them as a disjunction, and will prove only one of them.)
• negated_conjectures are formed from negation of a conjecture, typically in FOF to CNF conversion.
• plain formulae have no special user semantics, and are typically used in derivation output.
• type formulae define the types of symbols globally.
• interpretation formulae are used for writing interpretations, typically models of satisfiable sets of formulae, in particular the axioms and negated_conjecture of a non-theorem.
• logic formulae are used for defining the logic in non-classical logics.
• unknowns have unknown role, and this is an error situation.

The useful_info field of an annotated formula is optional, and if it is not used then the source field becomes optional. The source field is used to record where the annotated formula came from, and is most commonly a file record or an inference record. A file record stores the name of the file from which the annotated formula was read, and optionally the name of the annotated formula as it occurs in that file - this might be different from the name of the annotated formula itself, e.g., if an ATP systems reads an annotated formula, renames it, and then prints it out. An inference record stores information about an inferred formula. The useful_info field of an annotated formula is a list of arbitrary useful information formatted as Prolog terms, as required for user applications.

Logical Formulae
In a formula, terms and atoms follow Prolog conventions - functions and predicates start with a lowercase letter or are 'single quoted', and variables start with an uppercase letter. Symbols may be overloaded with different arity signatures, and are treated as different symbols. The language also supports interpreted symbols that are either defined symbols that start with a $, or are composed of non-alphabetic characters. Defined symbols come in two varieties: TPTP defined predicates and functors, whose interpretation is specified by the TPTP language, and system defined predicates and functors, whose interpretation is ATP system specific. The defined predicates and functors recognized so far are listed below.

The logical connectives in the classical TPTP languages are !>, ?*, @+, @-, ^, !, ?, @, ~, |, &, =>, <=, <=>, and <~>, for Pi, Sigma, choice (indefinite description), definite description, lambda abstraction, universal quantification, existential quantification, function application, negation, disjunction, conjunction, implication, reverse implication, equivalence, and non-equivalence (XOR). Equality and inequality are expressed as the infix predicates = and !=. Quantified formulae are written in the form
    Quantifier [Variables] :  Formula
In all except the CNF language, every variable in a Formula must be bound by a preceding quantification with adequate scope. Negation has higher precedence than quantification, which in turn has higher precedence than the binary connectives. No precedence is specified between the binary connectives; brackets are used to ensure the correct association. See the section on non-classical logics for information about the non-classical connectives.

Types
The typed languages (TFF, TXF, THF, DHF, NXF, NHF) support types and type declarations (all the details are in the section on types and type declarations). Symbols are declared before their use, with type signatures that specify the types of their arguments and result. Two TPTP defined types are available, $i for individuals, and $o for booleans. User defined types can be introduced as being of the "type" $tType. In the first-order languages, a signature of the form (t₁ * ... * t_n) > r is the type of an n-ary symbol, where the i-th argument is of type t_i and the result type is r. If r is $o then the symbol is a predicate. Variables are given their type by a :type suffix. Equality is ad hoc polymorphic over all types. A useful feature of TFF is default typing for symbols that are not explicitly declared: predicates default to ($i,...,$i) > $o, and functions default to ($i,...,$i) > $i. This allows TFF to effectively degenerate to untyped FOF. The typed extended first-order form (TXF) augments TFF with FOOL constructs: formulae of type $o as terms; variables of type $o as formulae; tuples; conditional (if-then-else) expressions; and let (let-defn-in) expressions. The typed higher-order form (THF) includes type declarations in curried form, lambda-terms with a binder symbol ^ for lambda, explicit application with @, and quantification over variables of any type. A curried type signature has the form t₁ > ... > t_n > r. THF does not admit default typing - all symbol types must be declared before use. The polymorphic languages use a !> to quantify over types, producing types signatures of the form !> [T:$tType] : (t₁ * ... * t_n) > r and !> [T:$tType] : t₁ > ... > t_n > r. where any t_i or r can be the type T. When using polymorphic symbols the concrete type(s) must be provided as the first arguments in the use.

Defined Symbols
The defined symbols are:

• The truth constants $true and $false.
• Integer/rational/real numbers such as 27, 43/92, -99.66.
• $distinct, whose arguments are hence known to be unequal from each other (but not necessarily unequal to any other constants). $distinct maybe overloaded with different arities. In the typed languages $distinct is ad hoc polymorphic with all arguments having the same type.
• "distinct object"s, written in double quotes. All "distinct object"s are unequal to all "different distinct object"s (but not necessarily unequal to any other constants), e.g., "Apple" != "Microsoft". One way of implementing this is to interpret "distinct object" as the domain element in the double quotes. In typed contexts "distinct object"s are of type $i (and as a result, are unequal to all numbers because their interpretation domains are disjoint in the TPTP type systems).
• Numbers (numeric constants). These are used in only the typed languages (numbers require a type system in order to make sense). Numbers are interpreted as themselves (as domain elements). All different numbers are unequal, e.g., 1 != 2 (but not necessarily unequal to any other constants of the same type). All numbers are also unequal to terms of type $i (because their interpretation domains are disjoint in the TPTP type systems).

Conditional and Let Expressions
The THF and TXF languages have conditional and let expressions.

• Conditional expressions have $ite as the functor. The expressions are parametric polymorphic, taking a boolean expression as the first argument, then two expressions of any one type as the second and third arguments, as the true and false return values respectively, i.e., the return type is the same as that of the second and third arguments.
• Let expressions have $let as the functor. The expressions provide the types of defined symbols, definitions for the symbols, and a formula/term in which the definitions are applied. Each type declaration is the same as a type declaration in an annotated formula with the type role, and multiple type declarations are given in []ed tuples of declarations. Each definition defines the expansion of one of the declared symbols, and multiple definitions are given in []ed tuples of definitions. If variables are used in the lefthand side of a definition, their values are supplied in the defined symbol's use. Such variables do not need to be declared (they are implicitly declared to be of the type defined by the symbol declaration), but must be top-level arguments of the defined symbol and be pairwise distinct. In the polymorphic case, type declarations may include type variables introduced in an enclosing scope, such as

  %----The constant function using A from 'outside' and B from 'inside'. B 
  %----is required in the use of const, but not A.
  tff(let_polymorphic_both_types, axiom,
      !>[A: $tType] : 
        $let(
          const : !>[B: $tType] : (A * B) > A,
          const(B, X, Y) := X),
          ... ).  

  No extra type arguments are needed when using such $let-defined symbols.

Examples
An example CNF problem is PUZ003-1. An example FOF problem is PUZ001+1. An example TFF problem is PUZ031_1. An example TXF problem is PUZ081_8. An example THF problem is PUZ081^1. An example DHF problem is DAT346^1. An example NXF problem is PUZ001_10. An example NHF problem is PHI003^8.

Subtypes
None of the type systems offer subtypes, despite the subtype symbol << being part of the THF and TFF languages. I tried to convince the ATP system developers it would be useful, but they cried crocodile tears. Here's an example of what was planned:

    tff(food_type,type, food: $tType).

    tff(fruit_type,type, fruit: $tType).

    tff(vegetable_type,type, vegetable: $tType).

    tff(fruit_is_food,type, 
        fruit << food ).

    tff(vegetable_is_food,type, 
        vegetable << food ). 

    tff(apple_decl,type, apple: fruit).

    tff(potatoe_decl,type, potatoe: vegetable).  

The Typed First-order Monomorphic Type System (TF0 and TX0)

Defined atomic types
The atomic types $i (individuals), $o (Booleans), and $tType are defined. ($tType is the "type" of atomic types - it is not really a type, and in other places this is known as the "kind" of atomic types. See below for motivation for its existence and usage.) Other defined atomic types are associated with specific theories. In particular, $int, $rat, and $real are types for arithmetic. The type $i of individuals is predefined but has no peculiar semantics, whereas the arithmetic types $int, $rat, and $real are modeled by ℤ, ℚ, and ℝ, respectively.

User atomic type declarations:
User atomic types are declared in advance of use, to be of "type" $tType. Example:

    tff(food_type,type, 
        food: $tType ).

    tff(fruit_type,type, 
        fruit: $tType ).

    tff(list_type,type, 
        list: $tType ).  

Defined functions and predicates
Defined functions and predicates have preassigned types.

• $true is of type $o
• $false is of type $o
• Distinct objects in "double quotes" are of type $i
• = and != are ad hoc polymorphic over atomic types other than $o, with result type $o.
• $distinct is ad hoc polymorphic over all atomic types other than $o, with result type $o.
• The (atomic) types of numbers are defined in the arithmetic section.
• The types of the arithmetic predicates and functions are defined in the arithmetic section.

Function and predicate type declarations
Every function and predicate symbol has maximally one declared type. Example:

    tff(cons_type,type, 
        cons: (fruit * list) > list   ).

    tff(is_empty_type,type, 
        isEmpty: list > $o   ).

Every variable is given an atomic type at quantification time. Example:

    tff(list_not_empty,axiom, 
        ! [X: fruit,Xs: list] : ~isEmpty(cons(X,Xs))   ).

Implicit typing for functions and predicates
If a symbol is used and its type has not been declared, then default types are assumed.

• All untyped predicates get type ($i * ... * $i) > $o.
• All untyped functions get type ($i * ... * $i) > $i.
• All untyped variables get type $i.

The Typed First-order Polymorphic Type System (TF1 and TX1)

The TF1 polymorphic type system extends the monomorphic type system with rank-1 polymorphism. Syntactically, the types, terms, and formulas of TF1 are analogous to those of TF0, except that function and predicate symbols can be declared to be polymorphic, types can contain type variables, and n-ary type constructors are allowed. Type variables in type signatures and formulas are explicitly bound. Instances of polymorphic symbols are specified by explicit type arguments, rather than inferred.

Types and type signatures
The types of TF1 are built from type variables and type constructors of fixed arities. A type is polymorphic if it contains type variables (otherwise, it is monomorphic). Polymorphic type signatures are of the form: !>[α1 : $tType, ..., αn : $tType]: ς for n > 0, where α1, ..., αn are distinct type variables and ς is a monomorphic type. The binder !> denotes universal quantification.

Type declarations
Type constructors can be declared, e.g., the following declarations introduce a type constant bird, a unary type constructor list, and a binary type constructor map:

    tff(bird_t, type, bird: $tType).
    tff(list_t, type, list: $tType > $tType).
    tff(map_t, type, map: ($tType * $tType) > $tType).  

    tff(is_empty_t, type, is_empty : !>[A : $tType]: (list(A) > $o)).
    tff(cons_t, type, cons : !>[A : $tType]: ((A * list(A)) > list(A))).
    tff(lookup_t, type, lookup : !>[A : $tType, B : $tType]: ((map(A, B) * A) > B)).

Using symbols with a polymorphic type
Every use of a polymorphic symbol must explicitly specify the type instance. A function or predicate symbol with a type signature !>[α₁$: $tType, ..., α_m : $tType]: ((τ₁ * ... * τ_n) > υ) must be applied to m type arguments and n term arguments. Given the above signatures, the term lookup($int, list(A), M, 2) and the atom is_empty($i, cons($i, X, nil($i))) are well-formed and contain free occurrences of the type variable A and the term variable X, respectively. As TF1 is restricted to rank-1 polymorphism, type variables can be instantiated with only concrete types. In particular, $o, $tType, and !>-binders cannot occur in type arguments of polymorphic symbols.

Every variable in a TF1 formula must be bound. In particular, every type variable in a TF1 formula must be bound with the pseudotype $tType:

    tff(bird_list_not_empty, axiom,
        ![B : bird, Bs : list(bird)]: ~ is_empty(bird, cons(bird, B, Bs))).

    tff(lookup_update_same, axiom,
        ! [A : $tType, B : $tType, M : map(A, B), K : A, V : B]:
          lookup(A, B, update(A, B, M, K, V), K) = V).  

Example
An example TF1 problem is PUZ139_1.

The Typed Higher-order Monomorphic Type System (TH0)

The TH0 monomorphic type system lifts the TF0 type system to simply typed λ-calculus, with Henkin semantics (i.e., including Boolean and functional extensionality) and choice. Type signatures are curried, and variables can have function types. Example:

    thf(mix_type,type,
        mix: beverage > syrup > beverage ).
    
    thf(mixed_coffee,conjecture,
        ? [Mixture: beverage > syrup > beverage] :
        ! [S: syrup] :
          ( ( Mixture @ coffee @ S ) = coffee ) ). 

An example TH0 problem is PUZ140^1.

The Typed Higher-order Polymorphic Type System (TH1)

The TH1 polymorphic type system combines the polymorphic features of TF1/TX1 with the higher-order features of TH0.
Example:

    thf(list,type, list: $tType > $tType ).
    
    thf(nil,type, nil: !>[A: $tType] : ( list @ A ) ).
    
    thf(append,type, append: !>[A: $tType] : ( ( list @ A ) > ( list @ A ) > ( list @ A ) ) ).
    
    thf(append_nil,axiom,
        ! [A: $tType,L: list @ A] :
          ( ( append @ A @ ( nil @ A ) @ L ) = L ) ). 

TH1 has five additional polymorphic constants: !! for Π (universal quantification), ?? for Σ (existential quantification), @@+ for ε (indefinite description, aka choice), @@- for ι (definite description), and @= (equality). The type of the first four is !>[A: $tType] : (A > $o) > $o, and the type of @= is !>[A: $tType]: (A > A) > $o. When used they must be instantiated by applying them to a type argument. Example:

    thf(eps,type, eps: ( $i > $o ) > $i ).
    
    thf(choiceax,axiom,
        ! [P: $i > $o] :
          ( ? [X: $i] : ( P @ X )
         => ( P @ ( eps @ P ) ) ) ).
    
    thf(conj,conjecture,
        ( ( ^ [P: $i > $o] : ( P @ ( eps @ P ) ) )
        = ( ^ [P: $i > $o] : ( ?? @ $i @ P ) ) ) ).
    
    thf(bird_type,type, bird: $tType).

    thf(tweety_decl,type, tweety: bird).

    thf(some_tweety,axiom,
        ? [B: bird] : ( (@= @ bird) @ tweety @ B ) ). 

An example TH1 problem is DAT434^1.

The Dependently Typed Higher-order Type System (DH0 and DH1)

The DH0 and DH1 type systems add dependent types, i.e., types that take term arguments, to TH0 and TH1. As such they are classical and extensional type theories. The !> binder used for TF1 and TH1 polymorphism is reused to specify the term typess on which a type depends. Example:

    thf(elem_type,type, elem: $tType ).

    thf(nat_type,type, nat: $tType ).

    thf(zero_type,type, zero: nat ).

    thf(suc_type,type, suc: nat > nat ).

    thf(plus_type,type, plus: nat > nat > nat ).

    thf(list_type,type, list: nat > $tType ).

    thf(nil_type,type, nil: list @ zero ).

    thf(cons_type,type, cons:
        !>[N: nat] : (elem > (list @ N) > (list @ (suc @ N))) ).

    thf(app_type,type, app:
        !>[N: nat,M: nat] : ((list @ N) > (list @ M) > (list @ (plus @ N @ M))) ). 

    thf(ax1,axiom,
        ! [N: nat] : ((plus @ zero @ N) = N) ).

    thf(ax2,axiom,
        ! [N: nat,X: list @ N] : ((app @ zero @ N @ nil @ X) = X) ).

    thf(list_app_assoc_base,conjecture,
        ! [M2: nat,L2: list @ M2,M3: nat,L3: list @ M3] :
          ( ( app @ zero @ ( plus @ M2 @ M3 ) @ nil @ ( app @ M2 @ M3 @ L2 @ L3 ) )
          = ( app @ ( plus @ zero @ M2 ) @ M3 @ ( app @ zero @ M2 @ nil @ L2 ) @ L3 ) ) ). 

The following interpreted predicates and interpreted functions are defined. The symbols are overloaded (i.e., ad-hoc polymorphic) for the provided type signatures.

Symbol	Types	Operation	Comments, examples                                        -
$int	$tType	The type of integers	123, -123 <integer> ::- (<signed_integer>|<unsigned_integer>) <signed_integer> ::- <sign><unsigned_integer> <unsigned_integer> ::- <decimal> <decimal> ::- (<zero_numeric>|<positive_decimal>) <positive_decimal> ::- <non_zero_numeric><numeric>* <sign> ::: [+-] <zero_numeric> ::: [0] <non_zero_numeric> ::: [1-9] <numeric> ::: [0-9]
$rat	$tType	The type of rationals	123/456, -123/456, +123/456 <rational> ::- (<signed_rational>|<unsigned_rational>) <signed_rational> ::- <sign><unsigned_rational> <unsigned_rational> ::- <decimal><slash><positive_decimal> <slash> ::: [/]
$real	$tType	The type of reals	123.456, -123.456, 123.456E789, 123.456e789, -123.456E789, 123.456E-789, -123.456E-789 <real> ::- (<signed_real>|<unsigned_real>) <signed_real> ::- <sign><unsigned_real> <unsigned_real> ::- (<decimal_fraction>|<decimal_exponent>) <decimal_exponent> ::- (<decimal>|<decimal_fraction>)<exponent><decimal> <decimal_fraction> ::- <decimal><dot_decimal> <dot_decimal> ::- <dot><numeric><numeric>* <dot> ::: [.] <exponent> ::: [Ee]
= (infix)	($int * $int) > $o ($rat * $rat) > $o ($real * $real) > $o	Comparison of two numbers.	The numbers must be the same atomic type (see the type system).
$less/2	($int * $int) > $o ($rat * $rat) > $o ($real * $real) > $o	Less-than comparison of two numbers.	$less, $lesseq, $greater, and $greatereq are related by   ! [X,Y] : ( $lesseq(X,Y) <=> ( $less(X,Y) | X = Y ) )   ! [X,Y] : ( $greater(X,Y) <=> $less(Y,X) )   ! [X,Y] : ( $greatereq(X,Y) <=> $lesseq(Y,X) ) i.e, only $less and equality need to be implemented to get all four relational operators.
$lesseq/2	($int * $int) > $o ($rat * $rat) > $o ($real * $real) > $o	Less-than-or-equal-to comparison of two numbers.
$greater/2	($int * $int) > $o ($rat * $rat) > $o ($real * $real) > $o	Greater-than comparison of two numbers.
$greatereq/2	($int * $int) > $o ($rat * $rat) > $o ($real * $real) > $o	Greater-than-or-equal-to comparison of two numbers.
$uminus/1	$int > $int $rat > $rat $real > $real	Unary minus of a number.	$uminus, $sum, and $difference are related by   ! [X,Y] : $difference(X,Y) = $sum(X,$uminus(Y)) i.e, only $uminus and $sum need to be implemented to get all three additive operators.
$sum/2	($int * $int) > $int ($rat * $rat) > $rat ($real * $real) > $real	Sum of two numbers.
$difference/2	($int * $int) > $int ($rat * $rat) > $rat ($real * $real) > $real	Difference between two numbers.
$product/2	($int * $int) > $int ($rat * $rat) > $rat ($real * $real) > $real	Product of two numbers.
$quotient/2	($int * $int) > $rat ($rat * $rat) > $rat ($real * $real) > $real	Exact quotient of two numbers of the same type.	For non-zero divisors, the result can be computed. For zero divisors the result is not specified. In practice, if an ATP system does not "know" that the divisor is non-zero, it should simply not evaluate the $quotient. Users should always guard their use of $quotient using inequality, e.g.,   ! [X: $real] : ( X != 0.0 => p($quotient(5.0,X)) ) For $rat or $real operands the result is the same type. For $int operands the result is $rat; the result might be simplied.
$quotient_e/2, $quotient_t/2, $quotient_f/2	($int * $int) > $int ($rat * $rat) > $rat ($real * $real) > $real	Integral quotient of two numbers.	The three variants use different rounding to an integral result: $quotient_e(N,D) - the Euclidean quotient, which has a non-negative remainder. If D is positive then $quotient_e(N,D) is the floor (in the type of N and D) of the real division N/D, and if D is negative then $quotient_e(N,D) is the ceiling of N/D. $quotient_t(N,D) - the truncation of the real division N/D. $quotient_f(N,D) - the floor of the real division N/D. For zero divisors the result is not specified.
$remainder_e/2, $remainder_t/2, $remainder_f/2	($int * $int) > $int ($rat * $rat) > $rat ($real * $real) > $real	Remainder after integral division of two numbers.	For τ ∈ {$int,$rat, $real}, ρ ∈ {e, t,f}, $quotient_ρ and $remainder_ρ are related by   ! [N:τ,D:τ] : $sum($product($quotient_ρ(N,D),D),$remainder_ρ(N,D)) = N For zero divisors the result is not specified.
$floor/1	$int > $int $rat > $rat $real > $real	Floor of a number.	The largest integral value (in the type of the argument) not greater than the argument (i.e., ! [X] : ($is_int($floor(X)))).
$ceiling/1	$int > $int $rat > $rat $real > $real	Ceiling of a number.	The smallest integral value (in the type of the argument) not less than the argument (i.e., ! [X] : ($is_int($ceiling(X)))).
$truncate/1	$int > $int $rat > $rat $real > $real	Truncation of a number.	The nearest integral value (in the type of the argument) with magnitude not greater than the absolute value of the argument (i.e., ! [X] : ($is_int($truncate(X)))).
$round/1	$int > $int $rat > $rat $real > $real	Rounding of a number.	The nearest integral value (in the type of the argument) to the argument (i.e., ! [X] : ($is_int($rount(X)))). If the argument is halfway between two integral values, the nearest even integral value to the argument.
$abs/1	$int > $int $rat > $rat $real > $real	Absolute value of a number.	$abs is related to other operators by ! [X] : ( ( $greatereq(X,0) => $abs(X) = X ) & ( $less(X,0) => $abs(X) = $uminus(X) ) )
$is_int/1	$int > $o $rat > $o $real > $o	Test for coincidence with an $int value.
$is_rat/1	$int > $o $rat > $o $real > $o	Test for coincidence with a $rat value.
$to_int/1	$int > $int $rat > $int $real > $int	Coercion of a number to $int.	The largest $int not greater than the argument; the argument effectively gets truncated before conversion: ! [X] : ($to_int($truncate(X)) = $to_int(X)). If applied to an argument of type $int, this is the identity function.
$to_rat/1	$int > $rat $rat > $rat $real > $rat	Coercion of a number to $rat.	This function is not fully specified. If applied to an argument of type $int, the result is the argument over 1. If applied to an argument of type $rat, this is the identity function. If applied to an argument of type $real that is (known to be) rational, the result is the $rat value. For other reals the result is not specified. In practice, if an ATP system does not "know" that the argument is rational, it should simply not evaluate the $to_rat. Users should always guard their use of $to_rat using $is_rat, e.g.,   ! [X: $real] : ( $is_rat(X) => p($to_rat(X)) )
$to_real/1	$int > $real $rat > $real $real > $real	Coercion of a number to $real.	If applied to an argument of type $real, this is the identity function.

The extent to which ATP systems are able to work with the arithmetic predicates and functions can vary, from a simple ability to evaluate ground terms, e.g., $sum(2,3) can be evaluated to 5, through an ability to instantiate variables in equations involving such functions, e.g., $product(2,$uminus(X)) = $uminus($sum(X,2)) can instantiate X to 2, to extensive algebraic manipulation capability. The syntax does not axiomatize arithmetic theory, but may be used to write axioms of the theory.

Full specification of the connectives and their use in formulae is in the BNF starting at <nxf_atom> and <thf_defined_atomic>.

Semantics Specification
An annotated formula with the role logic is used to specify the semantics of formulae. The semantic specification typically comes first in a file. A semantic specification consists of the defined name of the logic followed by == and a list of properties value assignments. Each specification is the property name, followed by == and either a value or a tuple of specification details. If the first element of a list of details is a value, that is the default value for all cases that are not specified in the rest of the list. Each detail after the optional default value is the name of a relevant part of the vocabulary of the problem, followed by == and a value for that named part. The BNF grammar is here. The grammar is not very restrictive on purpose, to enable working with other logics as well. It is possible to create a lot of nonsense specifications, and to say the same thing in different meaningful ways. A tool to check the sanity of a specification is available.

A semantic specification changes the meaning of things such as the boolean type $o, universal quantification with !, etc - their existing meaning in classical logic should not be confused with the meaning in the declared logic.

For plain $modal and all the *_modal logics the properties that may be specified are $domains, $designation, $terms, and $modalities.

• $domains
  • $constant - Constant domain semantics has all world's domains fixed the same.
  • $varying - Varying domain semantics has (potentially) different domains for each world.
  • $cumulative - Cumulative domain semantics and varying, and the domain of each world is a superset of the domains of the worlds from which it can be reached.
  • $decreasing - Decreasing domain semantics and varying, and the domain of each world is a subset of the domains of the worlds from which it can be reached.
• $designation
  • $rigid - Rigid designation independent of worlds.
  • $flexible - Flexible designation dependent on worlds.
• $terms
  • $local - Terms are interpreted in the local world
  • $global - Terms are interpreted globally in all the worlds
• $modalities
  • A known system name in the form $modal_system_Sys
    Sys ∈ { K,KB,K4,K5,K45,KB5,D,DB,D4,D5,D45,M,B,S4,S5,S5U }
  • A tuple of known axiom names in the form [ $modal_axiom_Ax₁, $modal_axiom_Ax₂, ... ]
    Ax_i ∈ { K,M,B,D,4,5,CD,BoxM,C4,C }

For $temporal_instant the properties are the $domains, $designation, and $terms of the modal logic, $modalities with different possible values, and another property $time.

• $modalities
  • A tuple of known axiom names in the form [ $modal_axiom_AxTm₁, $modal_axiom_AxTm₂, ... ]
    Ax_i ∈ { K,M,B,D,4,5 }, Tm_i ∈ { +,- },
• $time
  • A tuple of known time properties in the form [ P₁,P₂, ... ]
    P_i ∈ { $reflexivity, $irreflexivity, $transitivity, $asymmetry, $anti_symmetry, $linearity, $forward_linearity, $backward_linearity, $beginning, $end, $no_beginning, $no_end, $density, $forward_discreteness, $backward_discreteness }

The formulae of a problem can be either local (true in the current world) or global (true in all worlds). By default, formulae with the roles hypothesis and conjecture are local, and all others are global. These defaults can be overridden by adding a subrole, e.g., axiom-$local, conjecture-$global.

The TPTP Language BNF