[Prev][Next][Index][Thread]

TPTP-v1.2.0 release




*Email us if you want to register as a TPTP user or be removed from this alias.

                   The TPTP Problem Library, Release v1.2.0
                   ----------------------------------------

                                Geoff Sutcliffe
          Dep't of Computer Science, James Cook University, Australia.
                              geoff@cs.jcu.edu.au

                               Christian Suttner
                 Institut fuer Informatik, TU Muenchen, Germany
                       suttner@informatik.tu-muenchen.de

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:
+ 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.
+ New  generalized variants  of problems  whose original  presentation is hand-
  tailored towards a particular automated proof.
+ Arbitary size instances of generic problems (e.g., the pigeon-holes problem).
+ 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.
+ General guidelines outlining the requirements for ATP system evaluation.

The principal motivation for this project is to move the testing and evaluation
of ATP  systems from the previously  ad hoc situation onto a firm footing. This
became necessary,  as results currently being published often do not accurately
reflect the 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.

Release v1.2.0 of the TPTP is now available. TPTP v1.2.0 contains 2758 problems
in 25 domains. Here's what's new in v1.2.0 (after v1.1.3) :
+ 267 new problems, in the domains BOO COL GRP MSC PUZ ROB SYN.
+ 49 bugfixes done, in the domains COL LCL PUZ ROB SYN.
+ Generic problems (e.g., the N-queens problem) are now handled by problem
  generators, which allow the automatic generation of any desired problem size.
+ The % Syntax field has been reordered in all files.
+ The tptp2X utility has been extended and improved in various ways :
  - Installation and use of tptp2X have been simplified.
  - tptp2X now updates the % Syntax field after transformations.
  - There are three new output formats: 3TAP, KIF, and leanTAP.
  - Problem generation has been integrated into tptp2X.
  - The syntax for specifying equality axiom removal has changed.
  - The syntax for specifying OTTER format output has changed.
  - A new syntax conversion option for the SETHEO system has been added.
+ The TPTP technical report has been substantially revised.

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 one of us. Our addresses are:
    Geoff Sutcliffe   - geoff@cs.jcu.edu.au                (FAX: +61-77-814029)
or  Christian Suttner - suttner@informatik.tu-muenchen.de  (FAX: +49-89-526502)

The  TPTP can  be obtained  by  anonymous  ftp from  either the  Department  of
Computer  Science,  James Cook  University,  Australia,  or the  Institut  fuer
Informatik,  TU Muenchen, Germany.  Instructions for fetching and unpacking the
TPTP are  given below  in the  Quick Guide.  There are  three files in the TPTP
distribution:  ReadMe-v1.2.0, TPTP-v1.2.0.tar.gz, and TR-v1.2.0.ps.gz.  General
information  about the  library is  in the ReadMe-v1.2.0 file,  the library  is
packaged in TPTP-v1.2.0.tar.gz,  and a technical report describing the TPTP (in
postscript form)  is in  TR-v1.2.0.ps.gz.  Please read  the ReadMe file,  as it
contains up-to-date information about the TPTP.  The technical report serves as
a manual explaining the structure and use of the TPTP. It also explains much of
the reasoning behind the development of the TPTP.

                         TPTP Quick Installation Guide
                         -----------------------------

This explains how to obtain, install, and syntax-convert the TPTP problems. For
more details, explanations, and further options, see the TPTP technical report.

1. Obtaining the TPTP by FTP

   prompt> cd <the directory where you want the TPTP to reside>
   prompt> ftp -i ftp.cs.jcu.edu.au               # or: ftp -i 137.219.53.16
           # or use
           ftp -i flop.informatik.tu-muenchen.de  # or: ftp -i 131.159.8.35
   Name (ftp.cs.jcu.edu.au:<your login-name>): ftp
   331 Guest login ok, send your complete e-mail address as password.
   Password:<your full login-name>
   ftp> cd pub/research/tptp-library        # on ftp.cs.jcu.edu.au
        cd pub/tptp-library                 # on flop.informatik.tu-muenchen.de
   ftp> binary
   ftp> mget *.gz
   ftp> quit

   Or use the World Wide Web (WWW) with either of the following URLs :
      http://www.cs.jcu.edu.au/ftp/users/GSutcliffe/TPTP.HTML
      http://wwwjessen.informatik.tu-muenchen.de/~suttner/tptp.html


2. Installing the TPTP

   prompt> gunzip -c TPTP-v1.2.0.tar.gz | tar xvf -
   prompt> TPTP-v1.2.0/TPTP2X/tptp2X_install
           <... the script will then ask for required information>

   If you don't have any Prolog installed, you need to get one first. BinProlog
   is freely available by anonymous ftp from clement.info.umoncton.ca:BinProlog


3. Converting all the TPTP problems to the syntax of other ATP systems

   prompt> TPTP-v1.2.0/TPTP2X/tptp2X -f<Syntax>

   where  <Syntax> is one of  kif,  leantap, tap,  meteor, mgtp,  otter,  pttp,
   setheo, sprfn, or tptp.

   The tptp  option simply expands  include directives,  producing files in the 
   TPTP Prolog-style syntax.  tptp2X offers  MUCH more than this.  See the TPTP 
   technical  report  for a  detailed description  of  the  utility,  including 
   information on how to produce output in your own syntax.