================================================================================
The TPTP Problem Library, Release v7.3.0
----------------------------------------
Geoff Sutcliffe
Dep't of Computer Science, University of Miami, USA
ge...@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>.
================================================================================
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
