TPTP v9.0.0

[Geoff Sutcliffe]

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

                   The TPTP Problem Library, Release v9.0.0
                   ----------------------------------------

                                Geoff Sutcliffe
                                ge...@tptp.org

The TPTP  (Thousands  of Problems  for Theorem  Provers)  Problem Library  is a
library  of  test problems for  automated theorem proving  (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  the
capabilities of the ATP system being considered.

TPTP v9.0.0 is now available at:
    http://tptp.org/TPTP
The TPTP-v9.0.0.tgz file  contains the  library,  including utilities and basic
documentation. Full documentation is online at:
    http://tptp.org/TPTP/TR/TPTPTR.shtml

========================== What's New in TPTP v8.2.0 ==========================
Release v9.0.0, Sat Jun 1 11:42:52 EDT 2024

This is the first release with non-classical logic (NXF and NHF) problems.

Changes from v8.2.0 to v9.0.0 for THF problems
 40 new abstract problems, in the domains GRA SYO.
 50 new problems, in the domains GRA PHI SYO.
2578 ratings changed

Changes from v8.2.0 to v9.0.0 for TFF problems
134 new abstract problems, in the domains GRA LCL PLA PRO SWC SYO.
247 new problems, in the domains GRA LCL PLA PRO SWC SYO.
  4 bugfixes done, in the domains LCL SYN.
842 ratings changed

Changes from v8.2.0 to v9.0.0 for FOF problems
5786 ratings changed

Changes from v8.2.0 to v9.0.0 for CNF problems
  1 bugfixes done, in the domains LCL.
3144 ratings changed

In SyntaxBNF:
-  Added required ()s around <thf_defined_infix>, <thf_infix_unary>,
   <tff_defined_infix>, and <tff_infix_unary>. For TFF the ()s are really needed
   for only TXF, but TXF uses the same grammar rules.
- Added details of logic specifications.
================================================================================