TPTP v7.5.0
7 views
Skip to first unread message
Geoff Sutcliffe
Jul 13, 2021, 1:49:25 PM7/13/21
to TPTP World
================================================================================
The TPTP Problem Library, Release v7.5.0
----------------------------------------
Geoff Sutcliffe
Dep't of Computer Science, University of Miami, USA
*** 13th July 2021: The CADE-28 ATP System Competition (CASC-28) is running.
*** See the action online at ...
The TPTP (Thousands of Problems for Theorem Provers) Problem Library is a
library of test problems for automated theorem proving (ATP) systems. The TPTP
supplies the ATP community with:
+ A comprehensive library of the ATP test problems that are available today, in
order to provide an overview and a simple, unambiguous reference mechanism.
+ A comprehensive list of references and other interesting information for each
problem.
+ Arbitary size instances of generic problems (e.g., the N-queens problem).
+ A utility to convert the problems to existing ATP systems' formats.
+ General guidelines outlining the requirements for ATP system evaluation.
+ Standards for input and output for ATP systems.
The principal motivation for the TPTP is to support the testing and evaluation
of ATP systems, to help ensure that performance results accurately reflect
capabilities of the ATP system being considered. A common library of problems
is necessary for meaningful system evaluations, meaningful system comparisons,
repeatability of testing, and the production of statistically significant
results. The TPTP is such a library.
This is the first release with polymorphic THF (TH1) problems. There are 644
polymorphic TH1 problems in 14 domains.
TPTP v7.5.0 is now available at:
The TPTP-v7.5.0.tgz file contains the library, including utilities and basic
documentation. Full documentation is online at:
The TPTP is regularly updated with new problems, additional information, and
enhanced utilities. If you would like to register as a TPTP user, and be kept
informed of such developments, please email Geoff Sutcliffe.
========================== What's New in TPTP v7.5.0 ==========================
Release v7.5.0, Tue Jul 13 12:56:51 EDT 2021
Changes from v7.4.0 to v7.5.0 for THF problems
319 new abstract problems, in the domains COL GRP ITP LCL NUN SEV SYO.
512 new problems, in the domains COL GRP ITP LCL NUN PHI SEV SYO.
152 bugfixes done, in the domains ITP SYO.
Changes from v7.4.0 to v7.5.0 for TFA problems
60 bugfixes done, in the domains SWW.
Changes from v7.4.0 to v7.5.0 for TFF problems
1 new problems, in the domains PHI.
150 bugfixes done, in the domains ITP.
Changes from v7.4.0 to v7.5.0 for FOF problems
152 new abstract problems, in the domains COL GEO GRP SYO.
156 new problems, in the domains COL GEO GRP SYO.
108 bugfixes done, in the domains ITP SYO.
Changes from v7.4.0 to v7.5.0 for CNF problems
139 new problems, in the domains ANA BOO CAT COL CSR GRP KLE LAT LCL MGT MSC NLP PLA PUZ REL RNG ROB SWB SWV SYN SYO.
+ In SyntaxBNF
- Extended <general_data> to include bindings for type variables.
- Added <infix_inequality> to <thf_conn_term>
- Changed !! and friends to be constants:
<thf_prefix_unary> uses only <unary_connective>
<thf_defined_atomic> uses <th1_defined_term>, which in turn
uses <th1_defined_term>, which is !! and friends.
================================================================================
Reply all
Reply to author
Forward
0 new messages