Thousands of Models for Theorem Provers
The TMTP Model Library
Abstract
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, tools and
services for processing ATP problems and solutions, and it supports the
CADE ATP System Competition (CASC).
This work describes a new component of the TPTP World - the Thousands of
Models for Theorem Provers (TMTP) Model Library.
This is a corpus of models for identified sets of axioms in the TPTP,
along with functions for interpreting formulae wrt models, interfaces for
visualizing interpretations, tools for verifying models, etc.
The TMTP supports the development of semantically guided theorem proving
ATP systems, provides models that can be used to guide axioms selection in
large theories, and provides insights into the semantic structure of
axiomatizations.