Introduction
------------
The tptp2X  utility is used  to convert  TPTP problems from  the TPTP format to 
formats accepted  by existing ATP systems.  Additionally it allows to rearrange 
the clauses and  literals of  a TPTP problem.  The utility consists of  several 
files :
  tptp2X       - The main file of the tptp2X utility.
  tptpread     - Procedures for reading TPTP syntax files.
  tptpshort    - Procedures for shortening symbols in TPTP problems.
  format.<ATP> - Procedures for  outputing clauses in <ATP> format, where <ATP> 
                 is one of mgtp, otter, pttp, setheo, sprfn, tptp.
The tptp2X  code should run on most Prolog systems. The procedure realRead/2 in 
the  tptpread  file  has special  variants, for  SICStus 2.1,  SICStus 0.7  and 
Quintus,  which preserve  the variable  names in  the conversion  process.  The 
default version  of realRead/2 renames variables in the the conversion process. 
The distributed version  of tptp2X uses the default version of realRead/2.  The 
special variants can be used by changing the commenting in the tptpread file.


Using the tptp2X utility
------------------------
Before using  the tptp2X utility,  it is necessary to set  the name of the TPTP 
directory,  in the tptp_directory__/1 fact at the top of the tptpread file.  It 
is  currently set to ~/TPTP.  It must be  changed to the  absolute name of  the 
directory that contains the Problems and Axioms directories.

The main entry point to the tptp2X utility is tptp2X/5, in the form : 

?-tptp2X(<TPTP file>,<Format>,<Arrangements>,<Output dir.>,<Shorten flag>).

where:
  <TPTP file> is  the file name of  the TPTP problem file.  If the file name is 
    not relative, then it considered to be relative to the directory
    specified in the tptp_directory__/1 fact.
  <Format> is one of :
    setheo, to convert to TUM's SETHEO .lop format,
    otter(<SoS>,<Inference rules>), to convert to ANL's Otter .in format.
      <SoS> specifies the Set of Support to use. It can be one of :
        theorem,    to use the clauses whose status is theorem;
        hypothesis, to use the clauses whose status is hypothesis or theorem;
        positive,   to use the positive clauses;
        negative,   to use the negative clauses;
        unit,       to use the unit clauses.
      <Inference rules> is a (Prolog) list of Otter inference rules.
    mgtp,  to convert to ICOT's MGTP format;
    pttp,  to convert to Mark Stickel's PTTP format;
    sprfn, to convert to David Plaisted's SPRFN format,
    tptp,  to convert to the TPTP format.
  <Arrangements> is a (Prolog) list of arrangements. 
    The  rearrangment of  clauses  and/or  literals in  a  problem  facilitates 
    testing the  sensitivity of an ATP system to the order in which the clauses 
    and  literals  are presented.  For each  order specified  in  the  list,  a 
    separate output file is produced. The available orders are :
      none, for no reordering;
      lr,   to reverse the order of the literals in each clause;
      cr,   to reverse the order of the clauses in the problems;
      clr,  to reverse the order of the literals and the clauses.
  <Output directory> is where the output files are placed.
  <Shorten flag> is "shorten"  to replace  all symbols in the problem by short, 
    meaningless symbols.  This is  useful if  you are  only interested  in  the 
    syntax of the problem, and do not want to read through the long, meaningful 
    symbols that  are often  used in  TPTP problems.  To retain the  meaningful 
    symbols, use anything else, e.g. "_", as the <Shorten flag>.
 
There is  a secondary entry point  to the tptp2X utility, tptp2X/0.  This entry 
point interactively  prompts for the five arguments required for tptp2X/5,  and 
then calls the tptp2X/5 entry point.

An  alternative  to using  the tptp2X  entry  points directly,  is to  use  the 
tptp_convert script. This script provides a shell-level front end to the tptp2X 
utility. Use of the script is described in Scripts/ReadMe.


The tptp2X output files
-----------------------
The output files produced by the tptp2X utility are named according to the TPTP 
file  name and the  options used.  The name of the TPTP  problem (the file name 
without  the  .p)  forms  the  basis  of  the  output  file  names.   For  each 
rearrangement  specified,  the type  of rearrangement is  appended to the basic 
name,  except in the  case of "none"  rearrangement,  in which  case nothing is 
appended.  Finally, an extension to indicate the format is appended. The format 
extensions are .lop  for SETHEO  format, .in  for Otter  format, .mgtp for MGTP 
format,  .pttp for  PTTP format,  .sprfn for  SPRFN format,  and .tptp for TPTP 
format.


Example
-------
The following is a typical tptp2X/5 run.

coral:~/atp/TPTP2X> sicstus
SICStus 2.1 #7: Fri Feb 26 14:50:11 EST 1993
| ?- compile(tptp2X).

yes
| ?- tptp2X('Problems/PUZ/PUZ031-1.p',otter(hypothesis,[hyper_res]),[lr,cr],
     otter_directory,_).

yes
| ?- ^D

This  use of the tptp2X utility  converts the  problems PUZ031-1  to two  Otter 
format  files.  In one  file the literals  are reversed  and in  the other  the
clauses  are reversed.  In both  cases the  clauses with  status hypothesis  or
theorem are placed in the Set of Support list, and hyper-resolution is the only 
inference rule.  No symbol shortening is done.  Two output files are produced : 
otter_directory/PUZ031-1-lr.in  and  otter_directory/PUZ031-1-cr.in.  Note that 
the TPTP file name is quoted, to form a Prolog atom.


Specifying your own output format
---------------------------------
The output formats are specified in the format.<ATP> files. To make any changes 
to the formats provided, the corresponding format file has to be edited.  It is 
also simple  to add  new  formatting  capabilities to  the tptp2X  utility,  by 
creating  new fomat  files.  New format  files should  follow the  style of the 
existing format files. Typically, a new format file can be created by modifying 
a copy of one of the existing format files. The entry point in the format files 
is  via the  output_clauses_in_format__/2  procedure in  the tptp2X  file.  The 
arguments that are  passed to output_clauses_in_format__/2 are  the name of the 
format and a list of TPTP format input clauses.  To integrate a new format file 
into    the   tptp2X    utility,   it    is   necessary    to    add    a   new 
output_clauses_in_format__/2 clause in the tptp2X file,  following the standard 
set there.  The file extension  to be used  for output files  in the new format 
must be specified in a new format_extension__/2 fact,  and a character that can 
be    used   to    start   a   comment    must   be   specified    in   a   new 
format_comment_character__/2  fact.  Finally,  the  new  format  file  must  be 
compiled in with the tptp2X file. This is done by adding a compile query at the 
top of the  tptp2X file,  alongside the  queries that compile  in  the existing 
format files. 
