Skip to main content


The TPTP typed first-order form and arithmetic


Geoff Sutcliffe, Stephan Schulz, Koen Claessen and Peter Baumgartner

University of Miami

Technische Universitaet Muenchen

Chalmers University of Technology


Australian National University


The TPTP World is a well established infrastructure supporting research, development, and deployment of Automated Theorem Proving systems. Recently, the TPTP World has been extended to include a typed first-order logic, which in turn has enabled the integration of arithmetic. This paper describes these developments.

BibTeX Entry

    publisher        = {Springer},
    doi              = {10.1007/978-3-642-28717-6_32},
    author           = {Sutcliffe, Geoff and Schulz, Stephan and Claessen, Koen and Baumgartner, Peter},
    month            = mar,
    editor           = {{Nikolaj Bjoerner and Andrei Voronkov}},
    year             = {2012},
    keywords         = {theorem proving, tptp},
    title            = {The {TPTP} Typed First-order Form and Arithmetic},
    booktitle        = {Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence
                        and Reasoning},
    pages            = {406--419},
    address          = {Merida, Venezuela}


Served by Apache on Linux on seL4.