The TPTP World

The TPTP World is a well established infrastructure that supports research, development, and deployment of Automated Theorem Proving (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.

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

TPTP Problem Library

The TPTP (Thousands of Problems for Theorem Provers) problem library is a collection of test problems for Automated Theorem Proving (ATP) systems.

TSTP Solution Library

The TSTP (Thousands of Solutions from Theorem Provers) solution library is a collection of solutions to TPTP problems.

TPTP Language BNF

The TPTP language is one of the keys to the success of the TPTP World. It is used for writing both problems and solutions.

SZS Ontologies

The SZS ontologies provide values to specify the logical status of problems and solutions, and to describe logical data.

Online Tools and Services

SystemB4TPTP

SystemB4TPTP provides tools online, to prepare ATP problems.

SystemOnTPTP

SystemOnTPTP provides recent versions of ATP systems online, to solve ATP problems.

SystemOnTSTP

SystemOnTSTP provides tools online, to examine ATP solutions.

TPTP2T Selector

TPTP2T generates lists of problems and solutions from the TPTP and TSTP libraries, with required characteristics.

Events

TPTP Tea Party

The TPTP Tea Party brings together developers and users of the TPTP World. This approximately annual meeting elicits feedback to ensure that the TPTP World meets the needs of users and developers.

TPTP Talks

Slides from talks about the TPTP World (and some other aspects of automated reasoning) .

CASC

The CADE ATP System Competition (CASC) is the annual evaluation of fully automatic ATP systems - the world championship for such systems. 

TPTP World Tour

The TPTP World is coming to you in the first half of 2025. Book your lab's tour dates now!

User Documentation

Quick Guide

A quick guide to the TPTP problem library, TSTP solution library, and the TPTP language and standards. Some easy and hard test problems for ATP systems are listed.

TPTP Language

The TPTP language is one of the keys to the success of the TPTP World. Read lots about the language here.

TPTP Problem Library Manual

Eveything you need to know about downloading and using the TPTP problem library.

TPTP World Tutorial

A short hands-on tutorial about ATP and (practical use of) the TPTP World.

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.

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).