TPTP v8.0.0

4 views
Skip to first unread message

Geoff Sutcliffe

unread,
Apr 25, 2022, 12:49:26 PM4/25/22
to TPTP World
================================================================================

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

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

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

This is the first release with  TXF problems.  There are  306 TXF problems in 8
domains.  217 of the problems are TX0,  i.e., use monomorphic types, and 89 are
TX1,  i.e.,  use polymorphic types.  In order to avoid revealing which problems
might be  eligible for CASC-J11,  this release  does not  have updated  problem
ratings.

========================== What's New in TPTP v8.0.0 ==========================

Changes from v7.5.0 to v8.0.0 for THF problems
 88 new abstract problems, in the domains ITP.
178 new problems, in the domains ITP.

Changes from v7.5.0 to v8.0.0 for TFF problems
122 new abstract problems, in the domains ITP.
516 new problems, in the domains CSR ITP NUM PUZ SEU SEV SYN SYO.

Changes from v7.5.0 to v8.0.0 for CNF problems
  0 new abstract problems.
  1 new problems, in the domains SYN.

+ One new domain has been added:
  - MVA (MV-algebras)

+ New SZS value USM (Unsemantic)

+ In SyntaxBNF
  - Added TXF capability - a lot of changes for that.
  - Moved <thf_sequent> and <tfx_sequent> inwards to allow use inside formulae
    (not only top level).
  - Added <thf_definition> and <tfx_definition>
  - Made defined and system words more flexible, so they can start with $ then
    any <alpha_numeric>
  - Changed format of <tnc_long_connective> to include <system_constant>s.
  - Changed the third part of a <thf_let> to a <thf_logic_formula>
  - Removed <thf_conditional> as it is written and read as <thf_apply_formula>.
    It can still be written in a first-order functional style, read as a
    <thf_fof_function>. Removed <tfx_conditional> as it is written and read as
    <tff_atomic_formula>.
  - <tnc_connective> allowed as a <tff_defined_atomic>, for logic
    specifications.

================================================================================
Reply all
Reply to author
Forward
0 new messages