Arithmetic

Geoff Sutcliffe
University of Miami
geoff[@]cs.miami.edu

Some of these ideas come from emails with Stephan Schulz.

Introduction

A fair while ago Stephan Schulz and I wrote a proposal for integer arithmetic in the TPTP. There has been only one development towards adding such capabilities to an ATP system, that being Uwe Waldmann's SPASS+T system. Independently, the SMT-LIB has specified a theory of integers. The SMT theory closely corresonds to, but is a subset of, the existing TPTP proposal. SPASS+T relies on an SMT procedure for arithmetic and free function symbols.

Can we hope for Arithmetic in the TPTP?

If arithmetic will become part of the TPTP, I would like to keep it aligned with SMT-LIB, so that their specification of the semantics can be adopted (generally, I hope to leverage the SMT-LIB for all their theories).

Regarding the necessary extensions to the TPTP syntax, Stephan has suggested a system of "syntax levels", e.g.,

  1. Base
  2. Base+Integer Artithmetic
  3. Base+Full Arithmetic
  4. etc
This would allow people to restrict themselves to whatever level they want. My idea for specifying the syntax level is to have theory directives just like include directives, e.g., 
   include_theory('Theories/Integers.th').
Such a directive would have to appear at the start of a problem file, to indicate that the syntax and semantics of the theory are active for the problem. A concern is that a directive in a file might be too late - do systems need to know about any syntax extension in advance? Or should the matching of syntax to system be done by a harness?

A final and major concern is that if arithmetic is added to the TPTP, there will be no ATP systems that can deal with the problems. I do need to play with SPASS+T and find out its capabilities.