The TMTP Model Library for Automated Theorem Proving by Geoff Sutcliffe geoff@cs.miami.edu

The TMTP (Thousands of Models for Theorem Provers) is a library of models of axiomatizations for automated theorem proving (ATP) systems. The TMTP supplies the ATP community with:

• A library of models for ATP axiomatizations, expressed in a standard syntax. In particular, the TMTP contains models for axiomatizations from the TPTP Problem Library. These models are accumulated from the TSTP Solution Library.
• Tools for evaluating terms and formulae wrt the models.
• Tools for examining and manipulating the models.
• Standards for input and output for ATP systems.

Online access to:
TPTP Models	Individual models for TPTP axiomatizations.
SZS Ontology	Problem statuses, as may be established by an ATP system
TMTP subprojects:
System on TMTP	Services for processing solutions.
TMTP Citations	If you would like to cite the TMTP, please use: @InProceedings{SS15-IWIL, Author = "Sutcliffe, G. and Schulz, S.", Year = "2015", Title = "{The Thousands of Models for Theorem Provers (TMTP) Model Library - First Steps}", Editor = "Konev, B. and Schulz, S. and Simon, L.", BookTitle = "{Proceedings of the 11th International Workshop on the Implementation of Logics}", Place = "Suva, Fiji", Series = "EasyChair Proceedings in Computing", Number = "", Pages = "To appear", Comment = "" }