TPTP Format for Interpreted Integer Arithmetic

Introduction

The (new) TPTP syntax has features that were designed to facilitate the addition of interpreted functions and predicates for arithmetic. Specifically, (i) numbers have their own name space, and are assumed to be distinct, and (ii) interpreted functions and predicates have their own name space. This proposal is is to extend the TPTP syntax with interpreted functions and predicates for integer arithmetic. The proposed functions and predicates may be used for "doing" arithmetic - evaluation of ground expressions, and also for reasoning "about" arithmetic - manipulation of arithmetic expressions.

Arithmetic should be done in the context of TFF logic, which supports the predefined type $int. Using TFF enforces types and semantics that separate $int from $i from $o. If arithmetic is not done in the context of TFF, then the domain of every interpretation is the integers.

The integers are unbounded (rather than some specific implementation such as 16 bit 2's complement). Systems that implement some limited arithmetic, e.g., 32 bit, must halt in an SZS error state if they hit overflow.

Interpreted predicates and interpreted functions are proposed for the TPTP syntax:

$less_int/2 - Comparison of two integers.
$lesseq_int/2 - Comparison of two integers.
$greater_int/2 - Comparison of two integers.
$greatereq_int/2 - Comparison of two integers. $less_int, $lesseq_int, $greater_int, and $greatereq_int are related by
```
    ! [X,Y] : ( $lesseq_int(X,Y) <=> ( $less_int(X,Y) | X = Y ) )
    ! [X,Y] : ( $greater_int(X,Y) <=> $less_int(Y,X) )
    ! [X,Y] : ( $greatereq_int(X,Y) <=> $lesseq_int(Y,X) )
```
i.e, only $less_int and equality need to be implemented to get all four relational operators.
$uminus_int/1 - Unary minus of one integer.
$plus_int/2 - Addition of two integers.
$minus_int/2 - Subtraction of two integers. $uminus_int, $plus_int, and $minus_int are related by
```
    ! [X,Y] : $minus_int(X,Y) = $plus_int(X,$uminus_int(Y))
```
i.e, only $uminus_int and $plus_int need to be implemented to get all three additive operators.
$times_int/2 - Multiplication of two integers.
$divide_int/2 - Division of two integers. This is a partial function, being undefined for zero divisors.

$remainder_int/2 - Remainder after division. This is a partial function, being undefined for zero divisors. $divide_int and $remainder_int are related by

    ! [N,D] : $plus_int($times_int($divide_int(N,D),D),$remainder_int(N,D)) = N

$remainder_int has the properties that

    ! [N,D] :
      ( $greater_int(D,0)
     => ( $greater_int(D,$remainder_int(N,D)) 
        & $greatereq_int($remainder_int(N,D),0) ) )

    ! [N,D] : 
      ( $less_int(D,0) 
     => ( $less_int(D,$remainder_int(N,D)) 
        & $lesseq_int($remainder_int(N,D),0) ) )

i.e., the remainder lies between 0 and the divisor. Examples:

    $divide_int(13,5) = 2      $remainder(13,5) = 3
    $divide_int(-13,5) = -3    $remainder(-13,5) = 2
    $divide_int(13,-5) = -3    $remainder(13,-5) = -2
    $divide_int(-13,-5) = 3    $remainder(-13,-5) = -2

$power_int/2 - Exponentionation of two integers.

$abs_int/1 - Absolute value of one integer. $abs_int is related to other operators by

    ! [X] :
      ( ( $less_int(0,X)
       => $abs_int(X) = X )
      & ( X = 0
       => $abs_int(X) = 0 )
      & ( $less_int(X,0)
       => $abs_int(X) = $uminus_int(X) ) )

i.e, $abs_int can be implemented in terms of other operators.

$min_int/2 - Smallest (towards negative infinity) of two integers.
$max_int/2 - Largest (towards positive infinity) of two integers. $min_int and $max_int are related to other operators by
i.e, $min_int and $max_int can be implemented in terms of other operators.

The _int suffix on each indicates that they operate on integers. This enables differentiation in the future from analogous functions for, e.g., reals. The following will be added in the syntax:

<defined atom>       ::= $true | $false |
                         <term> = <term> | <term> != <term> | 
                         $equal(<term>,<term>) | 
                         <int_atom>
<int atom>           ::= $less_int(<term>,<term>) | $lesseq_int(<term>,<term>)

<term>               ::= <function term> | <variable>
<function term>      ::= <plain term> | <defined term> | <system term>
<plain term>         ::= <constant> | <functions>(<arguments>)
<defined term>       ::= <number> | <double quoted> | <int_term>
<int term>           ::= $plus_int(<term>,<term>) | $minus_int(<term>,<term>) |
                         $times_int(<term>,<term>) | $divide_int(<term>,<term>) |
                         $remainder_int(<term>,<term>) | $uminus_int(<term>)
<variable>           ::= <upper word>

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.

This proposal is minimal, in an effort to keep the entry barrier low. The choices made allow for conservative extensions in the future:

At this stage all the functions will be 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.

Sample Conjectures

These are sample conjectures, designed first to exercise basic arithmetic machinery, and then to provide increasingly hard challenges that require more complete treatment of arithmetic. If you design further examples to test particular notions, please email them to Geoff Sutcliffe, to be added to this list.

IntegerArithmetic.p

Axioms for other Operators

Other commonly used arithmetic operators can be defined in terms of the interpreted ones.

IntegerArithmetic.ax

This proposal was developed by Stephan Schulz and Geoff Sutcliffe, and has benefited from input at the 2005 TPTP Tea Party.