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:

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

Online access to:
Individual models for TPTP axiomatizations.
Problem statuses, as may be established by an ATP system

TMTP subprojects:
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      = ""
}