Logic List Mailing Archive

Announcement: TPTP Problem Library v9.3.0

================================================================================

                   The TPTP Problem Library, Release v9.3.0
                   ----------------------------------------

                                Geoff Sutcliffe
                                geoff@tptp.org

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>
================================================================================
--
[LOGIC] mailing list, provided by DLMPST
More information (including information about subscription management) can
be found here: http://dlmpst.org/pages/logic-list.php