TPTP v8.0.0
6 views
Skip to first unread message
Geoff Sutcliffe
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.
================================================================================
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