Some Opinions on TPTP

Hans de Nivelle
Instytut Informatyki, Wroclaw
Poland

Positive

TPTP has now become the common language of all serious first-order theorem provers. This is a very big step forward. It makes ATP more accessible to non-experts. For a developer, it is much easier to see how strong other theorem provers are on certain problems.

Although developers are usually creative at interpreting TPTP-results, TPTP still allows to obtain a reasonably objective standard for comparing the relative strenghts of theorem provers.

Negative

The problem with TPTP/CASC is there is too much symbiosis between the regular CASC winners and the CASC organization. Winners have invested very much in their system, and they naturally resist changes that would invalidate these investments. This has impact on the CASC organization, on the categories, and on possible extensions of TPTP format. Making changes in CASC is much harder than extending TPTP.

Some Statements

Treat CASC from TPTP separately. One can extend TPTP syntax and library without changing CASC. CASC is less important than the TPTP-interface.
The present extension to Higher-Order Logic is a missed opportunity. It should have been based on polymorphic lambda calculus with Curry-Howard isomorphism instead of Church's type theory. This would have solved all questions of proof representation, type system, and simplicity of representation (this is also my answer to point 5).
I think that the problem with adding of integers and reals is: Which integers and which reals? Unbounded precision?, 32/16-bit?, signed or unsigned? How to deal with overflows? One cannot add data types without adding a type system to TPTP, and this is already subject of long discussions.