[Om-announce] TPTP v7.3.0 released

[geoff at cs.miami.edu]

================================================================================

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

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

*** NOTICE: The CADE-27 ATP System Competition (CASC-27) will run on Wednesday.
*** See the action online at ...
***    http://www.tptp.org/CASC/27/

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.3.0 is now available at:
    http://www.tptp.org
The TPTP-v7.3.0.tgz file contains the library, including utilities and basic
documentation. Full documentation is online at:
    http://www.tptp.org/TPTP/TR/TPTPTR.shtml

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.3.0 ==========================

Release v7.3.0, Fri Aug 2 16:17:10 EDT 2019

Changes from v7.2.0 to v7.3.0 for THF problems
  8 bugfixes done, in the domains LCL.

Changes from v7.2.0 to v7.3.0 for TFA problems
  6 new abstract problems, in the domains PLA.
  7 new problems, in the domains PLA.

Changes from v7.2.0 to v7.3.0 for FOF problems
286 new abstract problems, in the domains CSR NUN SEV SWW.
458 new problems, in the domains CSR NUM NUN SEV SWW.
247 bugfixes done, in the domains CSR NUN SET.

Changes from v7.2.0 to v7.3.0 for CNF problems
 45 new abstract problems, in the domains SYO.
196 new problems, in the domains AGT ALG ANA BOO CAT COL CSR GRP HEN KLE LAT LCL MSC NLP NUM PLA PUZ REL RNG ROB SEU SWB SWV SYN SYO.
 16 bugfixes done, in the domains SET.

+ In SyntaxBNF
  - Added semantic rules for <thf_unitary_type>.
  - Split <tff_top_level_type> into <tff_atomic_type> and
    <tff_non_atomic_type>, and added (<tff_atomic_type>) to <tff_atomic_type>.

================================================================================