[Om-announce] TPTP v7.0.0 and CASC-26

[geoff at cs.miami.edu]

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

                   The TPTP Problem Library, Release v7.0.0
                   ----------------------------------------

                                Geoff Sutcliffe
             Dep't of Computer Science, University of Miami, USA
                              geoff at cs.miami.edu

*** NOTICE: The 26th CADE STP System Competition (CASC-26) is running today. 
*** See the action online at ...
***    http://www.tptp.org/CASC/26/
***    http://www.tptp.org/CASC/26/RealTimeResults.html

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.0.0 is now available at:
    http://www.tptp.org
The TPTP-v7.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

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.0.0 ==========================

Changes from v6.4.0 to v7.0.0 for THF problems
639 new abstract problems, in the domains ANA COM DAT GEO LIN MSC NUN PRO PUZ RAL SEV.
648 new problems, in the domains ANA COM DAT GEO LIN MSC NUN PRO PUZ RAL SEV.
  0 new generators.
  0 bugfixes done.

Changes from v6.4.0 to v7.0.0 for TFA problems
195 new abstract problems, in the domains ARI DAT SWW.
198 new problems, in the domains ARI DAT SWW.
  0 new generators.
  0 bugfixes done.

Changes from v6.4.0 to v7.0.0 for TFF problems
  0 new abstract problems.
  0 new problems.
  0 new generators.
  0 bugfixes done.

Changes from v6.4.0 to v7.0.0 for FOF problems
106 new abstract problems, in the domains GEO SEV SYO.
109 new problems, in the domains GEO SEV SYO.
  0 new generators.
  4 bugfixes done, in the domains BIO.

Changes from v6.4.0 to v7.0.0 for CNF problems
  0 new abstract problems.
  0 new problems.
  0 new generators.
  0 bugfixes done.

+ Two new domains have been added:
  - LIN (Linear Algebra)
  - RAL (Real Algebra)

+ Numbers no longer permitted in CNF and FOF. Use "distinct objects", e.g.,
  "27".

+ In SyntaxBNF
  - Noted that <number>s may not be used in CNF or FOF.
  - Added tcf
  - Moved ^ into <th0_quantifier>
  - Changed <thf_top_level_type> and <thf_unitary_type> to be more precise.
    <thf_binary_type> removed from <thf_binary_formula>.
  - Specified that the quantification in a $let must be universal.
  - Added ()s around the <thf_let_plain_defn> in a <thf_let_quantified_defn>
    (to avoid binding ambiguity).
  - Changed $ite to be an instance of a <thf_unitary_formula>, so it uses
    application rather than FOF style $ite(...).
  - Added := to the THF binary connectives, to accomodate logic specifications.
    This changed $let to use <thf_unitary_formula> for it's first arguments;
    the original rule hierarchy for $let has been changed to :== semantic
    rules. Semantic rules for logic specifications have been added.
  - Added := to the TFF binary connectives, to accomodate logic specifications.
  - Split off TFX language, for FOOL and modal logic.
  - Renamed things to separate THF from TFF from FOF from general
  - Added <tff_subtype> back
  - Added <tff_tuple_term>. Allow <thf_tuple>s to use either {}s or []s.
  - Added <thf_apply_type> to <thf_top_level_type>
  - Updated comment about number of languages, and comment saying all variables
    except CNF must be quantified.
================================================================================