The TSTP Solution Library
for Automated Theorem Proving

by	Geoff Sutcliffe geoff@cs.miami.edu

The TSTP (Thousands of Solutions from Theorem Provers) Solution Library 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 (coming online soon).
Tools for accessing and manipulating the solutions.
Standards for input and output for ATP systems.

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

Online access to:

TPTP Solutions
Individual solutions to TPTP problems.

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

TSTP subprojects:

System on TSTP
Services for processing solutions.

Other people are doing similar things:

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.

QED

The aim of the QED project is to build a single, distributed, computerized repository that rigorously represents all important, established mathematical knowledge.

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

Unique visitors to this page since 2 February 2004:

Online access to:
TPTP Solutions	Individual solutions to TPTP problems.
SZS Ontology	Problem statuses, as may be established by an ATP system

TSTP subprojects:
System on TSTP	Services for processing solutions.

Other people are doing similar things:
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.
QED	The aim of the QED project is to build a single, distributed, computerized repository that rigorously represents all important, established mathematical knowledge.
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

The TSTP Solution Library for Automated Theorem Proving

The TSTP Solution Library
for Automated Theorem Proving