TPTP-v1.2.1 ReadMe
------------------ Wed Jun 12 08:52:59 MET DST 1996.

(Please read the TPTP technical report for full details about the TPTP.)

Description
-----------
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 N-queens problem).
+ A utility  to convert the  problems to  existing ATP formats.  Currently  the
  KIF,  leanTAP, 3TAP,  METEOR, MGTP,  OTTER, PTTP,  SETHEO, SPASS,  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  being published  seldom  provided  an  accurate
reflection of the intrinsic power 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.

The TPTP  is the work  of Geoff Sutcliffe  and Christian  Suttner.  The TPTP is
maintained and  distributed from the Department of Computer Science, James Cook
University,  Australia.  The TPTP  is also  supported and  distributed  by  the
Institut fuer Informatik, TU Muenchen, Germany.

The TPTP  is regularly updated.  If you would like to  become a registered TPTP
user  and  be kept  informed of  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)

Simple  instructions for  obtaining and installing  the TPTP  are given in  the
Quick Installation Guide at the end of this ReadMe file.

Files
-----
The  TPTP  files  are kept  in various  directories,  as described  below.  The
directory structure  should not  be changed,  as the TPTP  software is coded to
work in the structure as distributed.

ReadMe-v1.2.1 - This file.
TPTP-v1.2.1.tar.gz - The TPTP problem library, which expands to :
+ Problems   - The problem files directory with subdirectories for each domain.
               The  subdirectories  contain  problem  files  with  the  clauses 
               specific to each problem.
+ Axioms     - The directory containing axiom set files.  Axiom sets are merged 
               into the problem files.
+ Generators - The  directory containing  generator files.  Generator files are
               used  to generate  instances of generic problems,  according  to
               user supplied size parameters.
+ TPTP2X     - The directory containing the tptp2X utility. The tptp2X utility:
               * Converts from  the TPTP format to formats used by existing ATP 
                 systems.
               * Applies transformations to the clauses of TPTP problems.
               * Controls  the  generation  of  TPTP  problem  files  from TPTP
                 generator files.
+ Scripts    - A directory containing C shell scripts that may be used with the 
               TPTP. The scripts are described in Scripts/ReadMe.
+ Documents  - A  directory  containing  documents that  provide  comprehensive
               online  information  about  the TPTP.  The  files provide  quick
               access to data that is useful for using the TPTP, using standard 
               system tools (e.g., grep, awk).
TR-v1.2.1.ps.gz - A technical report  describing  the TPTP.  The report  may be
               updated in each release of the TPTP.
BuggedProblems-v1.2.1 - A list  of bugs in  the current TPTP  (bugs found after 
               release).

Conditions of use
-----------------
By providing  this library  of ATP problems,  and a specification  of how these
problems should  be presented to ATP systems,  it is our intention to place the
testing, evaluation,  and comparison of ATP systems on a firm footing.  To this
end, you should abide by the  following conditions when using TPTP problems and
presenting your results.
1. The specific version,  edition,  and patch  level of the TPTP,  used as  the
   problem source, must be stated.
2. Each problem must be referenced by its unambiguous syntactic name.
3. No clauses or literals may be changed,  added,  or removed without  explicit
   notice (this holds also for removing equality axioms  when built-in equality
   is provided by the prover).
4. The  clauses or literals may not  be reordered  without explicit  notice. If
   reordering  is  done  using  the  tptp2X  utility,  the  reordering must  be
   explicitly noted.
5. The header  information in  each problem  may not  be used by the ATP system
   without explicit notice.  Any information  that is given  to the ATP system,
   other than that in the "input_clause"s,  must be explicitly noted (including
   any system switches or default settings).

Please email one of us if :
---------------------------
1. You find any mistakes in the TPTP.
2. You are able to provide further information for a TPTP problem.
3. You  want  to  contribute  a  problem  to  the TPTP.  Please use the problem
   template that comes with the distribution, and fill in header information as
   far as possible. Any unambiguous representation will do for the clauses.
4. You have further suggestions for improving the TPTP library.

General Disclaimer
------------------
Every effort has been made to ensure that the TPTP problems have been correctly
presented, and that appropriate acknowledgments have been made.  However, we do
not guarantee that we have succeeded,  and accept  no  responsibility  for  any
errors or omissions.  We will gratefully receive comments and  corrections.

Copyright
---------
The TPTP  is  copyrighted (c)  1993, 1994, 1995, 1996,  by Geoff Sutcliffe  and 
Christian Suttner.  Use and verbatim redistribution of the TPTP  are permitted.
Distribution  of any modified  version or  modified part  of the TPTP  requires 
permission.

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

                         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 *
   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.1.tar.gz | tar xvf -
   prompt> TPTP-v1.2.1/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, spass, 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.

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