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:

• A library of solutions to ATP problems, expressed in a standard syntax. In particular, the TSTP contains solutions to problems from the TPTP Problem Library.

• A utility to convert the output from existing ATP systems to the standard syntax.

• Tools for examining and manipulating the solutions.

• Standards for input and output for ATP systems.

Online access to:

• TPTP Solutions
  Individual solutions to TPTP problems.

• The SZS Ontology
  Problem statuses, as may be established by an ATP system

• Derivations
  Quick guide to writing derivations in TSTP format

• Interpretations
  Quick guide to writing interpretations in TSTP format

• SystemOnTSTP
  Online access to SystemOnTSTP solution examination.

• TPTP2T online
  Online access to TPTP2T problem and solution selection.

If you would like to cite the TSTP solution library, please use:

@InProceedings{Sut10,

    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"

}

@InProceedings{Sut07-CSR,

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

• Mizar
  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.

• HELM
  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
  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