The TSTP Solution Library

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 = "112", Publisher = "SpringerVerlag" } @InProceedings{Sut07CSR, 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 = "723", Publisher = "SpringerVerlag" } 
 
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 websupported mathematics. It provides you with a software system that connects a widerange 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 