TPTP v7.5.0

3 views
Skip to first unread message

Geoff Sutcliffe

unread,
Jul 13, 2021, 1:49:25 PMJul 13
to TPTP World
================================================================================

                   The TPTP Problem Library, Release v7.5.0
                   ----------------------------------------

                                Geoff Sutcliffe
             Dep't of Computer Science, University of Miami, USA
                              ge...@cs.miami.edu

*** 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