================================================================================
The TPTP Problem Library, Release v9.3.0
----------------------------------------
Geoff Sutcliffe
[email protected]
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.3.0 is now available at:
http://tptp.org/TPTP
The TPTP-v9.3.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 this Release ==========================
Release v9.3.0, Sat Jun 20 07:06:06 AM UTC 2026
Changes from v9.2.1 to v9.3.0 for THF problems
97 new problems, in the domains DAT GRA SEV SWX SYP.
3 bugfixes done, in the domains ITP SYN.
2959 ratings changed
Changes from v9.2.1 to v9.3.0 for TFF problems
321 new problems, in the domains COM DAT KRS MSC PLA PUZ SWX SYO SYP TIM.
151 bugfixes done, in the domains ITP SYN SYO.
1397 ratings changed
Changes from v9.2.1 to v9.3.0 for FOF problems
178 new problems, in the domains GEO GRA MGT SEV SWX.
3 bugfixes done, in the domains MGT SYN.
6860 ratings changed
Changes from v9.2.1 to v9.3.0 for CNF problems
131 new problems, in the domains ARI DAT GRA NUN PUZ RNG SWX.
2 bugfixes done, in the domains SYN.
5073 ratings changed
+ One new domain has been added:
- TIM (Time)
+ In SyntaxBNF:
- Fixed typo in <ntf_domain_type_list>
- Redefined <ntf_connective_name> ::= <ntf_defined_connective> |
<atomic_system_word>
<ntf_defined_connective> ::= <atomic_defined_word>
<ntf_connective_name> :== $box | $dia | {$necessary} | {$possible}
|
{$obligatory} | {$permissible} |
{$knows} |
{$canKnow} | {$believes} | {$canBelieve}
- Removed old fi_domain, fi_functors, fi_predicates
- Removed <thf_fof_function>, so all THF terms must be applied. That also
removed
<thf_arguments>
================================================================================
