The TSTP Solution Library
for Automated Theorem Proving

by Geoff Sutcliffe

The TSTP (Thousands of Solutions from Theorem Provers) is a library of solutions to test problems for automated theorem proving (ATP) systems. The TSTP supplies the ATP community with:

If you're new to all this, you might want to start at the TPTP and TSTP Quick Guide.

Online access to:
Individual solutions to TPTP problems.
Problem statuses, as may be established by an ATP system
Convention for new symbol names

TSTP subprojects:
Services for processing solutions.
  • TSTP Citations
If you would like to cite the TSTP, please use:
    Author       = "Sutcliffe, G.",
    Year         = "2010",
    Title        = "{The TPTP World - Infrastructure for Automated Reasoning}",
    Editor       = "Clarke, E. and Voronkov, A.",
    BookTitle    = "{Proceedings of the 16th International Conference on Logic
                    for Programming Artificial Intelligence and Reasoning}",
    Place        = "Dakar, Senegal",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "6355",
    Pages        = "1-12",
    Publisher    = "Springer-Verlag"

    Author       = "Sutcliffe, G.",
    Year         = "2007",
    Title        = "{TPTP, TSTP, CASC, etc.}",
    Editor       = "Diekert, V. and Volkov, M. and Voronkov, A.",
    BookTitle    = "{Proceedings of the 2nd International Computer Science
                    Symposium in Russia}",
    Place        = "Ekaterinburg, Russia", 
    Series       = "Lecture Notes in Computer Science",
    Number       = "4649",
    Pages        = "7-23",
    Publisher    = "Springer-Verlag"

Other people are doing similar things:
Metamath is a tiny language that can express theorems in abstract mathematics, accompanied by proofs that can be verified by a computer program. This site has a collection of web pages generated from those proofs and lets you see mathematics developed in complete detail from first principles, with absolute rigor.
The most important activity in the Mizar project is the development of a data base for mathematics. The data base contains definitions of mathematical concepts and thousands of theorems.
The aim of the QED project is to build a single, distributed, computerized repository that rigorously represents all important, established mathematical knowledge.
The HELM project is meant to integrate the current tools for the automation of formal reasoning and the mechanization of mathematics (proof assistants and logical frameworks) with the most recent technologies for the development of web applications and electronic publishing. The final aim is the development of a suitable technology for the creation and maintenance of a virtual, distributed, hypertextual library of formal mathematical knowledge.
MathWeb supplies an infrastructure for web-supported mathematics. It provides you with a software system that connects a wide-range of mathematical services by a common, mathematical software bus, a set of mathematical services that support all aspects of doing mathematics on the web, an inter lingua for mathematical communication (OMDoc), and a portal for potential users and a discusssion forum for developers