{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,15]],"date-time":"2025-06-15T13:20:49Z","timestamp":1749993649077},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>The TPTP World is a well established infrastructure that supports research,<\/jats:p><jats:p>development, and deployment of Automated Theorem Proving (ATP) systems for<\/jats:p><jats:p>classical logics.<\/jats:p><jats:p>The TPTP world includes the TPTP problem library, the TSTP solution library,<\/jats:p><jats:p>standards for writing ATP problems and reporting ATP solutions, and it<\/jats:p><jats:p>provides tools and services for processing ATP problems and solutions.<\/jats:p><jats:p>This work describes a new component of the TPTP world - the Thousands of<\/jats:p><jats:p>Models for Theorem Provers (TMTP) Model Library.<\/jats:p><jats:p>This is a library of models for identified axiomatizations built from<\/jats:p><jats:p>axiom sets in the TPTP problem library, along with functions for efficiently<\/jats:p><jats:p>evaluating formulae wrt models, and tools for examining and processing<\/jats:p><jats:p>the models.<\/jats:p><jats:p>The TMTP supports the development of semantically guided theorem proving<\/jats:p><jats:p>ATP systems, provide examples for developers of model finding ATP systems,<\/jats:p><jats:p>and provides insights into the semantics of axiomatizations.<\/jats:p>","DOI":"10.29007\/7dg5","type":"proceedings-article","created":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T18:04:19Z","timestamp":1516730659000},"page":"106-89","source":"Crossref","is-referenced-by-count":2,"title":["The Thousands of Models for Theorem Provers (TMTP) Model Library - First Steps"],"prefix":"10.29007","volume":"40","author":[{"given":"Geoff","family":"Sutcliffe","sequence":"first","affiliation":[]},{"given":"Stephan","family":"Schulz","sequence":"additional","affiliation":[]}],"member":"11545","event":{"name":"IWIL-2015. 11th International Workshop on the Implementation of Logics"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T18:04:21Z","timestamp":1516730661000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/V3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/7dg5","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}