[T7] ================================================ AMAST Links 02 07

               The TPTP Problem Library, Release v1.2.0

   The _full version_ of this announcement is available at URL:
   http://www.cs.utwente.nl/data/amast/links/v02/i07/full/AC0207T7.txt

  The TPTP (Thousands of Problems for Theorem Provers) Problem Library
is a library of test problems for automated theorem proving (ATP)
systems, using the clause normal form of 1st order logic.  The TPTP
supplies the ATP community with: 
 o  A comprehensive library of the ATP test problems that are 
    available today, in order to provide an overview and a simple, 
    unambiguous reference mechanism.
 o  A comprehensive list of references and other interesting 
    information for each problem.
 o  New generalized variants of problems whose original presentation is
    hand-tailored towards a particular automated proof.
 o  Arbitary size instances of generic problems (e.g., the pigeon-holes
    problem).  
 o  A utility to convert the problems to existing ATP formats.
    Currently the KIF, leanTAP, 3TAP, METEOR, MGTP, OTTER, PTTP,
    SETHEO, and SPRFN formats are supported, and the utility can
    easily be extended to produce any format required.
 o  General guidelines outlining the requirements for ATP system
    evaluation.
  The tools are available on the WWW or by anonymous ftp, with either
of the following URLs:
WWW : http://www.cs.jcu.edu.au/ftp/users/GSutcliffe/TPTP.HTML
FTP : ftp://ftp.cs.jcu.edu.au/pub/research/tptp-library
WWW : http://wwwjessen.informatik.tu-muenchen.de/~suttner/tptp.html
FTP : ftp://flop.informatik.tu-muenchen.de/pub/tptp-library

  If you would like to register as a TPTP user, and be kept informed
of such developments, please email one of us. Our addresses are:

  Geoff Sutcliffe   : geoff@cs.jcu.edu.au (FAX: +61-77-814029)
  Christian Suttner : suttner@informatik.tu-muenchen.de
    (FAX: +49-89-526502)