The University of New South Wales

The TPTP typed first-order form and arithmetic

Authors

Geoff Sutcliffe, Stephan Schulz, Koen Claessen and Peter Baumgartner

University of Miami

Technische Universitaet Muenchen
Germany

Chalmers University of Technology

NICTA

Australian National University

Abstract

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

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

Download