The TPTP World

The TPTP World is the established infrastructure used by the Automated Theorem Proving (ATP) community for research, development, and deployment of ATP systems. The TPTP World has some key online components, accessible through the links in the logo images below.

If you're new to all this, you might want to start at the TPTP and TSTP Quick Guide. You could also work your way through the slides of the TPTP World Tutorial. There is quite comprehensive documentation in the TPTP Problem Library's technical manual that is also relevant to other parts of the TPTP World.

If you have any questions, suggestions, or contributions, please email Geoff Sutcliffe (the TPTP World is my baby :-). If you are not sure whether the TPTP World is for you, Get Inspired!

The TPTP World Needs Money If your work benefits from use of the TPTP and related projects, consider making an annual cash donation to support the TPTP. A donation can be made as an unrestricted gift (tax deductible) to the University of Miami, explicitly to support the TPTP and related projects. Read about benefits and process of making a donation. A premium support contract is also available.

Problems, Solutions, & Standards

Online Tools and Services

Events

User Documentation

If you would like to cite the TPTP World, please use:

@InProceedings{Sut24,

    Author       = "Sutcliffe, G.",

    Year         = "2024",

    Title        = "{Stepping Stones in the TPTP World}",

    Editor       = "Benzmüller, C. and Heule, M. and Schmidt, R.",

    BookTitle    = "{Proceedings of the 12th International Joint Conference on Automated

                    Reasoning}",

    Place        = "Nancy, France",

    Series       = "Lecture Notes in Artificial Intelligence",

    Number       = "14739",

    Pages        = "30-50"

}

See the TPTP problem library and TSTP solution library pages for their BibTeX entries.

TPTP Proposals

We are working on new features for the TPTP, as explained in the following proposals. Comments from potential users will be appreciated.

• Dependent Types

• Interpretation Representation and Model Verification

• Include File Namespace Hierarchy

• Answer Extraction

• The TPTP Process Instruction Language

• ATP System Building Conventions

TPTP Software

Many people have written software for processing TPTP format data. These links point to software I know of (please send your link if you have some software to add to the list).

• Geoff's Service Tools (clone --recurse-submodules to get the JJParse submodule). A bunch of tools for manipulating the TPTP, including the JJ parser for the TPTP language (named after the Spanish software developers, Justo Fernandez Reche and José Taboada Berenguer). The JJ parser will parse TPTP files and build a useful data structure, and there are lots of "useful" API functions for interrogating and manipulating the data structure. There is no documentation for any of this yet, but the sample drivers illustrate how to use the JJ parser API.

• João Paulo A. Almeida's TPTP Editor as an Eclipse Plugin.

• Alex Steen's Scala parser for the entire TPTP grammar.

• Tobias Gleißner's ANTLR4 grammar for the SyntaxBNF-v7.0.0.

• Matthias Fuchs' NPM package for the TPTP and SystemOnTPTP.

• Mark Lemay's Xtext based Java parser for the TPTP grammar.

• Michael Rawson's Rust parser for the TPTP's FOF and CNF grammars.