Arithmetic must be done in the context of the THF or TFF types logics, which support the predefined atomic numeric types $int, $rat, and $real. Using THF or TFF enforces semantics that separate $int from $rat from $real from $i from $o. The numbers are unbounded, and the reals of infinite precision (rather than some specific implementation such as 32 bit 2's complement integer, or IEEE floating point). Systems that implement limited arithmetic must halt in an SZS error state if they hit overflow.
The following interpreted predicates and interpreted functions are defined. The symbols are overloaded (i.e., ad-hoc polymorphic) for the provided type signatures. 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.
Arithmetic datatypes
$int
The type of integers
$tType
123, -123
$rat
The type of rationals
$tType
123/456, -123/456, +123/456
$real
The type of reals
$tType
123.456, -123.456,
123.456E789, 123.456e789, -123.456E789,
123.456E-789, -123.456E-789
Comparison and additive functions
= (infix), != (infix), $less/2, $lesseq/2, $greater/2, $greatereq/2
Comparison of two numbers.
($int * $int) > $o
($rat * $rat) > $o
($real * $real) > $o
The two numbers must be the same atomic arithmetic type.
=, $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 = and $less are needed to get all four relational operators.
$uminus/1
Unary minus of a number.
$int > $int
$rat > $rat
$real > $real
$sum/2, $difference/2
Sum and difference of two numbers.
($int * $int) > $int
($rat * $rat) > $rat
($real * $real) > $real
$uminus, $sum, and $difference are related by
! [X,Y] : $difference(X,Y) = $sum(X,$uminus(Y))
i.e, only $uminus and $sum are needed to get all three additive operators.
Multiplicative functions
$product/2
Product of two numbers.
($int * $int) > $int
($rat * $rat) > $rat
($real * $real) > $real
$quotient/2
Exact quotient of two numbers of the same type.
($int * $int) > $rat
($rat * $rat) > $rat
($real * $real) > $real
For non-zero divisors, the result can be computed. For zero divisors the $quotient is not defined. In practice, if an ATP system does not "know" that the divisor is non-zero, it should simply not evaluate $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
Integral quotient of two numbers.
($int * $int) > $int
($rat * $rat) > $rat
($real * $real) > $real
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
Remainder after integral division of two numbers.
($int * $int) > $int
($rat * $rat) > $rat
($real * $real) > $real
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.
Type conversion functions
$floor/1
Floor of a number.
$int > $int
$rat > $rat
$real > $real
The largest integral value (in the type of the argument) not greater than the argument, i.e., ! [X] : ($is_int($floor(X))).
$ceiling/1
Ceiling of a number.
$int > $int
$rat > $rat
$real > $real
The smallest integral value (in the type of the argument) not less than the argument, i.e., ! [X] : ($is_int($ceiling(X))).
$truncate/1
Truncation of a number.
$int > $int
$rat > $rat
$real > $real
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
Rounding of a number.
$int > $int
$rat > $rat
$real > $real
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
Absolute value of a number.
$int > $int
$rat > $rat
$real > $real
$abs is related to other operators by
! [X] :
( ( $greatereq(X,0)
=> $abs(X) = X )
& ( $less(X,0)
=> $abs(X) = $uminus(X) ) )
Recognition and coersion functions
$is_int/1
Test for coincidence with an $int value.
$int > $o
$rat > $o
$real > $o
$is_rat/1
Test for coincidence with a $rat value.
$int > $o
$rat > $o
$real > $o
$to_int/1
Coercion of a number to $int.
$int > $int
$rat > $int
$real > $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
Coercion of a number to $rat.
$int > $rat
$rat > $rat
$real > $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
Coercion of a number to $real.
$int > $real
$rat > $real
$real > $real
If applied to an argument of type $real, this is the identity function.