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:

Online access to:
• TPTP Solutions Individual solutions to TPTP problems.
• The SZS Ontology Problem statuses, as may be established by an ATP system
• New Names Convention for new symbol names introduced in proofs
• 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