                           tptp_convert
                           ------------

This script is  a shell-level front  end  to  the tptp2X  utility.

Usage : tptp_convert

The user  is prompted for the required  information for the conversion,  and an
input file for the Prolog interpreter is built.  The Prolog interpreter is then
invoked, taking  input from this file.  It is necessary to configure tptp2X for
your Prolog  dialect  (see the  tptp2X ReadMe  file or  look in  tptp2X.config)
before using this script.  The problems to be converted are specified  relative
to the TPTP  Problems directory.  The output files are placed in subdirectories
below the  supplied output directory,  maintaining the  TPTP Problems directory
structure.

Usage : tptp_convert meteor|mgtp|otter|pttp|setheo|sprfn|tptp

The user is  prompted for system specific information,  then all TPTP files are
converted to  the specified  format  (for  Otter the  format specifies  Otter's
autonomous mode).  The output  files are  stored in  a directory  named as  the 
specified format.  No transformations  are applied.  This is the fastest way to 
convert all TPTP problems to another format.

Example
-------
The following is a typical tptp_convert run.

sunjessen19:~/TPTP> tptp_convert
Absolute name of TPTP2X directory      : ~/TPTP/TPTP2X
Name of your Prolog interpreter        : eclipse
Names of files to convert, relative to /home/geoff/TPTP/Problems
    (e.g., S??/*)                      : A??/*
Tranformations to apply
    (e.g., [clr,magic])                : none
Formats to convert to
    (e.g., setheo)                     : setheo
Absolute name of output directory
    (e.g., ~/ATP/TPTPProblems)         : ~/LOP
Make the directory /home/geoff/LOP/ALG
Make the directory /home/geoff/LOP/ANA
ECRC Common Logic Programming System [sepia opium megalog]
Version 3.4.4, Copyright ECRC GmbH, Fri Mar 25 14:08 1994
[eclipse 1]:
tptp2X     compiled traceable 14812 bytes in 2.10 seconds

yes.

sunjessen19:~/TPTP>

This use of tptp_convert converts all the  problems in the  ALG and ANA domains
to the SETHEO format. No transformations are done to the clauses.


                           tptp_naming
                           -----------
This  script  renames  TPTP  problem  files  with  either  their  syntactic  or
syntactic=semantic name,  using the  names given  in the  % File  field of  the
header.

Usage : tptp_naming syntactic|semantic <List of problem files>

Example
-------
The following is a typical tptp_naming run.

sunjessen4:~/TPTP> tptp_naming semantic Problems/GRP/GRP001*
Problems/GRP/GRP001-1.p renames to Problems/GRP/GRP001=SqrComm-1.p
Problems/GRP/GRP001-2.p renames to Problems/GRP/GRP001=SqrComm-2.p
Problems/GRP/GRP001-3.p renames to Problems/GRP/GRP001=SqrComm-3.p
Problems/GRP/GRP001-4.p renames to Problems/GRP/GRP001=SqrComm-4.p
Problems/GRP/GRP001-5.p renames to Problems/GRP/GRP001=SqrComm-5.p
sunjessen4:~/TPTP>

This use of tptp_naming adds the semantic name  to all versions of the abstract
problem GRP001.
