TPTP Format for Interpreted Arithmetic

Introduction

Arithmetic must be done in the context of TFF logic, which supports the predefined types $int, $rat, and $real. Using TFF enforces types and semantics that separate $int from $rat from $real from $i from $o. If arithmetic is not done in the context of TFF, then the domain of every interpretation is the integers/rationals/reals. Here are some strange cases that show what can happen if you don't use a type system:

• ! [X] : X = a is unsatisfiable if X in an integer, but satisfiable otherwise.
• ! [X] : X < X+1 will not hold automatically.
• The conjecture ? [X] : X != a ...
  • Is CounterSatisfiable if there are no types and no integers in the problem.
  • Is a Theorem if there are no types and there are some integers in the problem.
  • Is a Theorem if there are types and X and a are both integers.
  • Is CounterSatisfiable if there are types and X and a are not integers.
  The first two cases show why it might be considered insane to do arithmetic without types - the status can be changed by adding an axiom that has an integer in it. If a is not intended to be an integer, then there's unsoundness wrt proving.

The numbers are unbounded and the reals of of infinite precision (rather than some specific implementation such as 32 bit 2's complement integer, or IEEE floating point). Systems that implement some limited arithmetic, e.g., 32 bit, must halt in an SZS error state if they hit overflow.

The following interpreted predicates and interpreted functions are proposed for the TPTP syntax. Each symbol is suffixed to indicate the type of numbers in the arguments and produced by functions. A _int suffix on indicates integers, a _rat suffix on indicates rationals, and a _real suffix indicates reals. Thus, for example $plus_int/2 takes two integer arguments and returns an integer, while $minus_real/2 takes two real arguments and returns a real. In the table below a * is used in place of specific suffixes. Comparators, e.g., $less_rat/2, return a $o. There are coercion functions to convert integers to rationals and reals, and rationals to reals. There are functions to convert reals and rationals to integers.

At this stage all the functions are written in prefix form. The general issue of flexible specification of infix operators in the TPTP syntax is an orthogonal issue, which must be addressed separately.

Symbol	Operation	Number types	Comments, examples                                        -
$int	The type of integers		123, -123 <integer> ::- (<signed_integer>|<unsigned_integer>) <signed_integer> ::- <sign><unsigned_integer> <unsigned_integer> ::- <decimal_natural> <decimal_natural> ::: ([0]|<non_zero_numeric><numeric>*) <sign> ::: [+-]
$rat	The type of rationals		123/456, -123/456, 123/-456, -123/-456 <rational> ::- <integer>[/]<integer> If the denominator is 0, that's a syntax error. If the denominator evaluates to 0, that's a runtime error.
$real	The type of reals		123.456, -123.456, 123.456E789, 123.456e789, -123.456E789, 123.456E-789, -123.456E-789 <real> ::- (<decimal_fraction>|<decimal_exponent>) <decimal_exponent> ::: (<decimal>|<decimal_fraction>)<exponent><decimal> <decimal_fraction> ::: <decimal><dot_decimal> <decimal> ::: (<signed_decimal>|<decimal_natural>) <signed_decimal> ::: <sign><decimal_natural> <dot_decimal> ::: [.]<numeric><numeric>* <exponent> ::: [Ee]
= (infix)	Comparison of two numbers.	= is adhoc polymorphic	See the type system.
$less_*/2	Comparison of two numbers.	* = {int,rat,real}
$lesseq_*/2	Comparison of two numbers.	* = {int,rat,real}
$greater_*/2	Comparison of two numbers.	* = {int,rat,real}
$greatereq_*/2	Comparison of two numbers.	* = {int,rat,real}	$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.
$uminus_*/1	Unary minus of a number.	* = {int,rat,real}
$plus_*/2	Addition of two numbers.	* = {int,rat,real}
$minus_*/2	Subtraction of two numbers.	* = {int,rat,real}	$uminus_*, $plus_*, and $minus_* are related by   ! [X,Y] : $minus_*(X,Y) = $plus_*(X,$uminus_*(Y)) i.e, only $uminus_* and $plus_* need to be implemented to get all three additive operators.
$times_*/2	Multiplication of two numbers.	* = {int,rat,real}
$eval_*/2	Evaluates the first argument and unifies the answer with the second	* = {int,rat,real}	Example: $eval_int($plus_int(4,5),X) succeeds with X set to 9. This allows a relational form of mathematics, and is also necessary for "forcing" evaluation. For example, the conjecture ... fof(do,conjecture, ? [X] : $plus_int(2,3) = X). ... could be proved without setting X to 5. By using the $eval_*/2 predicate ... fof(do,conjecture, ? [X] : $eval_int($plus_int(2,3),X)). ... the ATP system is forced to do the evaluation.
Everything above here can be done for purely integer arithmetic
$is_int_*/1	True when the argument coincides with an integer	* = {rat,real}
$is_rat_*/1	True when the argument coincides with a rational	* = {real}
$to_rat_*/1	Coerce a number to rational	* = {int}
$to_real_*/1	Coerce a number to real	* = {int,rat}

The extent to which ATP systems are able to work with the interpreted predicates and functions may vary, from a simple ability to evaluate ground terms, e.g., $plus_int(2,3) may be evaluated to 5, through an ability to instantiate variables in equations involving such functions, e.g., $times_int(2,$uminus_int(X)) = $uminus_int($plus_int(X,2)) may instantiate X to 2, to extensive algebraic manipulation capability.

Axioms

    ! [X:$int] : $greater_int($succ_int(X),X)

IntegerArithmetic.p

Axioms for other Operators

IntegerArithmetic.ax