The Thousands of Models for Theorem Provers (TMTP) Model Library - First Steps
Geoff Sutcliffe, Stephan Schulz · EPiC series in computing · 2018
The TPTP World is a well established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems for classical logics. The TPTP world includes the TPTP problem library, the TSTP solution library, standards for writing ATP problems and reporting ATP solutions, and it provides tools and services for processing ATP problems and solutions. This work describes a new component of the TPTP world - the Thousands of Models for Theorem Provers (TMTP) Model Library. This is a library of models for identified axiomatizations built from axiom sets in the TPTP problem library, along with functions for efficiently evaluating formulae wrt models, and tools for examining and processing the models. The TMTP supports the development of semantically guided theorem proving ATP systems, provide examples for developers of model finding ATP systems, and provides insights into the semantics of axiomatizations.