TPTP v8.1.0
1 view
Skip to first unread message
Geoff Sutcliffe
Aug 9, 2022, 4:45:18 AM8/9/22
to TPTP World
================================================================================
The TPTP Problem Library, Release v8.1.0
----------------------------------------
Geoff Sutcliffe
Dep't of Computer Science, University of Miami, USA
*** 9th August 2022: The 11th IJCAR ATP System Competition (CASC-J11) 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.
+ Arbitrary 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 the
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.
Release v8.1.0, Sat Jul 30 18:16:58 EDT 2022
Changes from v8.0.0 to v8.1.0 for THF problems
64 new abstract problems, in the domains DAT LCL NLP PLA PUZ SYO.
298 new problems, in the domains DAT ITP LCL NLP PLA PRO PUZ SET SWB SWW SYO.
Changes from v8.0.0 to v8.1.0 for TFA problems
0 new abstract problems.
0 new problems.
Changes from v8.0.0 to v8.1.0 for TFF problems
66 new abstract problems, in the domains ITP.
86 new problems, in the domains ITP.
Changes from v8.0.0 to v8.1.0 for FOF problems
0 new abstract problems.
0 new problems.
Changes from v8.0.0 to v8.1.0 for CNF problems
24 new abstract problems, in the domains LAT MVA NUN TOP.
88 new problems, in the domains ALG ANA GRP LAT LCL MVA NUN TOP.
+ SZS ontology extended to include non-logical data output.
+ In SyntaxBNF
- Renamed "tnc" to "ntf"
- Added @ in <tfx_ntf_atom> ::= <ntf_connective> @ (<tff_arguments>)
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.
+ Arbitrary 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 the
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.
TPTP v8.1.0 is now available at:
The TPTP-v8.1.0.tgz file contains the library, including utilities and basic
documentation. Full documentation is online at:
========================== What's New in TPTP v8.1.0 ==========================
Release v8.1.0, Sat Jul 30 18:16:58 EDT 2022
Changes from v8.0.0 to v8.1.0 for THF problems
64 new abstract problems, in the domains DAT LCL NLP PLA PUZ SYO.
298 new problems, in the domains DAT ITP LCL NLP PLA PRO PUZ SET SWB SWW SYO.
Changes from v8.0.0 to v8.1.0 for TFA problems
0 new abstract problems.
0 new problems.
Changes from v8.0.0 to v8.1.0 for TFF problems
66 new abstract problems, in the domains ITP.
86 new problems, in the domains ITP.
Changes from v8.0.0 to v8.1.0 for FOF problems
0 new abstract problems.
0 new problems.
Changes from v8.0.0 to v8.1.0 for CNF problems
24 new abstract problems, in the domains LAT MVA NUN TOP.
88 new problems, in the domains ALG ANA GRP LAT LCL MVA NUN TOP.
+ SZS ontology extended to include non-logical data output.
+ In SyntaxBNF
- Renamed "tnc" to "ntf"
- Added @ in <tfx_ntf_atom> ::= <ntf_connective> @ (<tff_arguments>)
================================================================================
Reply all
Reply to author
Forward
0 new messages