TH1: The TPTP Typed Higher-Order Form
with Rank-1 Polymorphism
Abstract
The TPTP world is a well established infrastructure that supports
research, development, and deployment of Automated Theorem Proving (ATP)
systems for classical logics.
The TPTP language is one of the keys to the success of the TPTP world.
Originally the TPTP world supported only first-order clause normal form (CNF).
Over the years support for full first-order form (FOF),
monomorphic typed first-order form (TF0), rank-1 polymorphic
typed first-order form (TF1), and monomorphic typed
higher-order form (TH0) have been added.
The TF0, TF1, and TH0 languages also include constructs for arithmetic.
This paper introduces the TH1 form, an extension of TH0 with TF1-style rank-1
polymorphism.
TH1 is designed to be easy to process by existing reasoning tools
that support ML-style polymorphism.
The hope is that TH1 will be implemented in many popular ATP systems for
typed higher-order logic.