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.

BibTeX

@inproceedings{ckgsfr-paar16,
 author    = {Cezary Kaliszyk and
              Geoff Sutcliffe and
              Florian Rabe},
 title     = {{TH1:} The {TPTP} Typed Higher-Order Form with Rank-1
Polymorphism},
 pages     = {41--55},
 booktitle = {Proc. 5th Workshop on Practical Aspects of Automated
Reasoning (PAAR 2016)},
 year      = {2016},
 editor    = {Pascal Fontaine and
              Stephan Schulz and
              Josef Urban},
 series    = {{CEUR}},
 volume    = {1635},
 publisher = {CEUR-WS.org},
}