Utilities

The tptp2X Utility

The tptp2X utility is a multi-functional utility for reformatting, transforming, and generating TPTP problem files. In particular, it

Converts from the TPTP format to formats used by existing ATP systems.
Applies various transformations to TPTP problems.
Controls the generation of TPTP problem files from TPTP generator files.

tptp2X is written in Prolog, and should run on most Prolog systems. It is known to run on current versions of Eclipse, SICStus, SWI, and YAP Prolog. Before using tptp2X, it is necessary to install the code for the dialect of Prolog that is to be used. This and other installation issues are described next.

Installation

The tptp2X utility consists of the following files:

tptp2X - A shell script for running the tptp2X utility.
tptp2X_install - A csh script for installing the tptp2X utility.
tptp2X.config - The configuration file with site specific information.
tptp2X.main - The main source code file of the tptp2X utility.
tptp2X.read - Procedures for reading TPTP problem files.
tptp2X.generate - Procedures for using TPTP generator files.
tptp2X.syntax - Procedures for extracting syntactic measures from files.
tptp2X.format - Procedures used by format modules.
transform.<TRAN> - Procedures for doing <TRAN> transformations on TPTP problems.
format.<ATP> - Procedures for outputing formulae in <ATP> format.

Installation of the tptp2X utility requires simple changes in the tptp2X script and the files tptp2X.config and tptp2X.main. These changes can be made by running tptp2X_install, which will prompt for required information. Otherwise, to install tptp2X by hand, the following must be attended to:

In the tptp2X script file:
- TPTPDirectory must be set to the absolute path name of the TPTP directory.
- PrologInterpreter must be set to the absolute path name of the Prolog interpreter.
- PrologArguments must be set to any command line arguments for the Prolog interpreter.
- The Gawk variable must be set to the absolute path name of gawk or awk.
In the tptp2X.config file:
- The appropriate facts for the desired Prolog dialect must be uncommented.
- The absolute path name of the TPTP directory must be set in the tptp_directory/1 fact.
In the tptp2X.main file:
- If your Prolog interpreter does not support compile/1 for loading source code, the compile/1 directives must be changed to something appropriate, e.g., [ ].
- The compile directives for unwanted output format modules can be commented out.

Using tptp2X

The most convenient way of using the tptp2X utility is through the tptp2X script. The use of this script is:

tptp2X [-h][-q<Level>][-i][-s<Size>][-t<Transform>][-f<Format>] [-d<Directory>] -l<NamesFile>|<TPTPFiles>

The -h flag specifies that usage information should be output. The -q flag specifies the level of quietness at which the script should operate. There are three quietness levels; 0 is verbose mode, 1 suppresses informational output from the Prolog interpreter, and 2 suppresses all informational output except lines showing what files are produced. The default quietness level is 1. The -i flag specifies that the script should enter interactive mode after processing all other command line parameters. Interactive mode is described below. The other command line parameter values are:

-s<Size> : This specifies the required sizes when generating problems. <Size> is either an integer, a <Low>..<High> integer size range, or a : separated list of <Sizes>.

An integer directly specifies the required problem size.
Each integer in a size range is used to generate a separate set of formulae.
A : separated string of <Sizes> is used for generators that require multiple parameters, one <Size> for each size parameter required. For example, -s3..5:2 means the three sizes 3:2, 4:2, and 5:2.

-s<Size> is ignored for problem (.p) files.

-t<Transform> : Specifies transformations to be applied to the formulae. <Transform> is either a single transformation, a + separated string of transformations, or a comma separated list of <Transform>s.
- A single transformation is applied directly to the formulae.
- The transformations in a + separated string are applied to the formulae serially.
- Each <Transform> in a comma separated list of <Transform>s is used to create a separate set of transformed formulae.
The transformations are:
- clausify:<Algorithm>, to transform FOF problems to CNF problems. The <Algorithm> is one of:
  
  bundy, to use the algorithm presented in [Bun83],
  otter, to use the algorithm used in Otter [McC98],
  quaife, to use Art Quaife's algorithm [Qua90],
  tptp, to use an algorithm combining features of the otter and quaife algorithms.
  Details of these algorithms can found in [SM96]. Note that these transformations do not simplify the resultant clause set; see the next two transformations for this.
- simplify, to simplify a set of clauses. Details of the simplifications performed can be found in [SM96].
- cnf:<Algorithm>, to do clausify:<Algorithm> followed by simplify. Details of the performance of these transformations can be found in [SM96]. Generally cnf:otter and cnf:bundy produce clause sets with lower symbol counts than the other two.
- propify, to convert a set of 1st order clauses to a set of propositional clauses, preserving satisfiability. The transformation is very naive.
- lr, to reverse the literal ordering in the clauses of CNF problems.
- cr, to reverse the clause ordering in CNF problems.
- clr, to do both clausal reversals.
- fr, to reverse the formula ordering in FOF problems.
- random, to randomly reorder the clauses and literals in CNF problems, or to randomly reorder the formulae in FOF problems. The rearrangement of formulae, clauses, and literals in a problem facilitates testing the sensitivity of an ATP system to the order of presentation.
- er, to reverse the arguments of unit equality clauses in CNF problems.
- ran_er, to reverse the arguments of randomly selected unit equality clauses in CNF problems.
- rm_equality:<Remove>, to remove equality axioms. <Remove> is a string that indicates which equality axioms to remove. The characters that can be in the string are:
  - r, to remove reflexivity,
  - s, to remove symmetry,
  - t, to remove transitivity,
  - f, to remove function substitution,
  - p, to remove predicate substitution.
  For example, -t rm_equality:stfp would remove symmetry, transitivity, function substitution, and predicate substitution. This transformation works only if the equality axiomatization is complete (i.e., including the axioms of reflexivity, symmetry, transitivity, function substitution for all functors, and predicate substitution for all predicate symbols), using equal/2 as the equality predicate. (All TPTP problems containing the equal/2 predicate contain a complete equality axiomatization; see Section Equality Axiomatization.)
- add_equality, to add missing equality axioms. If the problem contains the equal/2 predicate, then a check is made to see if the equality axiomatization is complete. If not, the missing equality axioms are added to the problem.
- to_equality, to convert CNF problems to a pure equality representation. Every non-equality literal is converted to an equality literal (using the equal/2 predicate) with the same sign. The arguments of the new equality literal are the atom of the non-equality literal and the constant true.
- magic, to apply Mark Stickel's magic set transformation [Sti94] to CNF problems.
- shorten, to replace all the 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. Note that equal/2 is not shortened.
- none, to do nothing (same as omitting the -t parameter, but required for advanced use; see Section Running tptp2X from within Prolog).
The default <Transform> is none.
-f<Format> : Specifies the format in which the output is to be written. The available output formats are:
- bliksem, to convert CNF problems to the Bliksem format [DeN98]
- carine, to convert CNF problems to the CARINE format
- clin_s, to convert CNF problems to the CLIN-S format [CP94, Chu94]
- code to convert CNF condensed detachment problems to the CoDe format [FF97]
- dedam to convert CNF unit equality problems to the Dedam format [NRV97]
- dfg, to convert CNF problems to the DFG format [HKW96]
- dimacs, to convert propositional CNF problems to the DIMACS format [DIM]
- eqp to convert CNF unit equality problems to the EQP format [McC00]
- finder, to convert CNF problems to the FINDER format [Sla92]
- glides, to convert CNF problems to the GLiDeS format [BS00]
- ilf, to convert CNF problems to the ILF format [DG+95]
- kif, to convert CNF problems to the KIF format [GF92]
- leantap, to convert CNF problems to the leanTAP format [BP95]
- tap, to convert CNF problems to the 3TAP format [HBG94]
- mace4, to convert CNF problems to the Mace4 format [McC03]
- math, to convert propositional CNF problems to the Mathematica format
- meteor, to convert CNF problems to the METEOR format [Ast94]
- mgtp, to convert CNF problems to the MGTP format [FH+92]
- omdoc, to convert problems to the OmDoc format [Koh]
- oscar, to convert FOF problems to the OSCAR format [Pol90]
- otter:<SoS>:'<Otter options>', to convert FOF and CNF problems to the Otter .in format [McC94]. <SoS> specifies the Set-of-Support to use. It can be one of:
  - conjecture, to use the formulae whose type is conjecture
  - not_conjecture, to use the formulae whose type is not conjecture
  - hypothesis, to use the formulae whose type is hypothesis or conjecture
  - axioms, to use the formulae whose type is axiom
  - positive, to use the positive clauses
  - negative, to use the negative clauses
  - unit, to use the unit clauses
  - all, to use all formulae
  - none, to use no formulae (needed fo Otter's auto mode)
  '<Otter options>' is a quoted (to avoid UNIX shell errors), comma separated list of Otter options, which will be output before the formula lists. See the Otter Reference Manual and Guide [McC94] for details of the available options. For example, -f otter:none:'set(auto),assign(max_seconds,5)' would configure Otter to use its auto mode with a time limit of 5 seconds. As the auto mode is commonly used with Otter, the tptp2X script allows the abbreviation -f otter to specify -f otter:none:'set(auto),set(tptp_eq),clear(print_given)'. If no -t parameter is specified then -f otter also sets -t equality:stfp.
- protein, to convert CNF problems to the PROTEIN format [BF94]
- pttp, to convert CNF problems to the PTTP format [Sti84]
- satchmo, to convert CNF problems to the SATCHMO format [GPS97]
- scott, to convert CNF problems to the SCOTT format [HS00]
- sem:<WhatToModel>:<Cardinality>, to convert CNF problems to the SEM format [ZZ96]. <WhatToModel> specifies which clauses to use. It can be one of:
  - conjecture, to use the formulae whose type is conjecture
  - not_conjecture, to use the formulae whose type is not conjecture
  - hypothesis, to use the formulae whose type is hypothesis or conjecture
  - axioms, to use the formulae whose type is axiom
  - positive, to use the positive clauses
  - negative, to use the negative clauses
  - unit, to use the unit clauses
  - all, to use all formulae
  - none, to use no formulae (needed fo Otter's auto mode)
  <Cardinality> is the required cardinailty of the model.
- setheo:<Style>, to convert CNF problems to the SETHEO .lop format [STK90].
  <Style> specifies the style of SETHEO clauses to write. It can be one of:
  - sign, to write the atoms of the negative and positive literals of each clause in the antecendent and consequent of an implication, respectively;
  - type In the type style, if there are no negative axiom or hypothesis clauses, then the sign style is used. Otherwise in all negative axiom and hypothesis clauses the first literal is negated to form the consequent of an implication, with the remaining literals' atoms being written as the antecedent. Further, in all conjecture clauses all positive literals are negated so that all literals are written in the antecedent of an implication.
  The default style is sign, i.e., the abbreviation -f setheo means -f setheo:sign.
- sprfn, to convert CNF problems to the SPRFN format [Pla88]
- thinker, to convert FOF problems to the THINKER format [Pel82, Pel87]
- tptp, to convert FOF and CNF problems to the TPTP format, substituting include instructions with the actual formulae
- tstp, to convert FOF and CNF problems to the TPTP format [SZS03]
- waldmeister, to convert CNF unit equality problems to the Waldmeister format [HBF96]
The default <Format> is tptp.
-d<Directory> : Specifies the top level directory below which the output files are to be placed. If the <Directory> value is -, then all output files are written to standard output, and all informational output is suppressed (even quieter than -q2). If the input file has a TPTP domain name as its first three characters, the output files for that input file are placed in a subdirectory below the <Directory>, named according to the domain. Otherwise the output files are written in the <Directory>. The default <Directory> is a subdirectory below the TPTP Problems directory, named according to the <Format>.
-l<NamesFile> : Specifies a file containing the names of the input files which are to be processed, one per line. This can be used instead of an explicit list of files, described next.
<TPTPFiles> : Lists the input files which are to be processed. As a shortcut, the three letter domain names can be given, which processes all problems in those domains. If no files are specified, the entire TPTP is processed. If any file names are not absolute, then tptp2X looks in the current working directory, the Generators directory, the Problems directory, and the domain directories, for the file. If the file name - is specified then input is taken from standard input and all output is written to standard output (overriding any <Directory> specification). The default <TPTPFiles> is all TPTP problem files.
Hint: If your command shell complains about too many arguments as a result of expanding the <TPTPFiles> argument to a too large number of files, e.g., ~/TPTP/Problems/S*/*.p, place the <TPTPFiles> argument in 'single quotes', and tptp2X will do the expansion internally.

A common first use of tptp2X is to convert TPTP problems to another format. To convert all TPTP problems to another format, the use is tptp2X -f<Format>, e.g., tptp2X -f otter. To limit the conversion to one or more domains, the domain names are specified after the <Format>, e.g., tptp2X -f leantap ALG GRP LDA. If you are a new TPTP user, these are probably the uses that you want to start with.

The tptp2X Output Files

The output files produced by tptp2X are named according to the input file name and the options used. The TPTP problem name (the input file name without the .p or .g) forms the basis of the output file names. For files created from TPTP generators, the size parameters are appended to the base name, separated from the base name by a ".". Then, for each transformation applied a suffix is appended. The suffixes for the transformations are:

Transformation	Suffix

stdfof	`+stdfof`
clausify:<Algorithm>	`+cls_<Algorithm>`
simplify	`+simp`
cnf:<Algorithm>	`+cnf_<Algorithm>`
propify	`+prop`
lr	`+lr`
cr	`+cr`
clr	`+clr`
fr	`+fr`
random	`+ran`
er	`+er`
ran_er	`+ran_er`
rm_equality:<Remove>	`+rm_eq_<Remove>`
add_equality	`+eq`
to_equality	`+2eq`
magic	`+nhms`
shorten	`+short`
none

Finally an extension to indicate the output format is appended to the file name. The suffixes for the output formats are:

Format	Extension	Format	Extension

bliksem	`.blk`	carine	`.car`
clin-s	`.clin_s`	code	`.code`
dedam	`.dedam`	dfg	`.dfg`
dimacs	`.dimacs`	eqp	`.eqp`
finder	`.fin`	glides	`.glides`
ilf	`.ilf`	kif	`.kif`
leanTAP	`.leantap`	tap	`.3tap`
meteor	`.me`	mgtp	`.mgtp`
oscar	`.oscar`	otter	`.in`
protein	`.tme`	pttp	`.pttp`
satchmo	`.sat`	scott	`.sin`
sem	`.sem`	setheo	`.lop`
sprfn	`.sprfn`	thinker	`.thinker`
tptp	`.tptp`	waldmeister	`.pr`

To record how a tptp2X output file has been formed, the tptp2X parameters are given in a % Comments field entry of the output file.

Example

~/TPTP/TPTP2X> tptp2X -tlr,cr,clr -fpttp ../Problems/ALG/ALG001-1.p
---------------------------------------------------------------------
TPTP2X directory      = /home/2/tptp/TPTP/TPTP2X
TPTP directory        = /home/2/tptp/TPTP
Prolog interpreter    = /usr/local/bin/sicstus
Files to convert      = ../Problems/ALG/ALG001-1.p
Size                  =
Transformation        = lr,cr,clr
Format to convert to  = pttp
Output directory      = /home/tptp/TPTP/Problems/pttp
---------------------------------------------------------------------
Made the directory /home/tptp/TPTP/Problems/pttp/ALG
ALG001-1 -> /home/tptp/TPTP/Problems/pttp/ALG/ALG001-1+lr.pttp
ALG001-1 -> /home/tptp/TPTP/Problems/pttp/ALG/ALG001-1+cr.pttp
ALG001-1 -> /home/tptp/TPTP/Problems/pttp/ALG/ALG001-1+clr.pttp
~/TPTP/TPTP2X>

This run applies three separate transformations to the problem ALG001-1. The transformations are literal order reversal, clause order reversal, and reversal of both literal and clause order. The transformed problems are output in pttp format, in the directory pttp/ALG below the TPTP Problems directory. The file names are ALG001-1+lr.pttp, ALG001-1+cr.pttp, and ALG001-1+clr.pttp.

Example

~/TPTP/TPTP2X> tptp2X -q2 -s3..5 -fotter -d~tptp/tmp SYN001-1.g
SYN001-1 -> /home/tptp/tmp/SYN/SYN001-1.003+rm_eq_stfp.in
SYN001-1 -> /home/tptp/tmp/SYN/SYN001-1.004+rm_eq_stfp.in
SYN001-1 -> /home/tptp/tmp/SYN/SYN001-1.005+rm_eq_stfp.in
~/TPTP/TPTP2X>

This run generates three sizes of the generic problem SYN001-1. The sizes are 3, 4, and 5. The output files are formatted for Otter, to use its auto mode. The files are placed in \verb/~/tptp/tmp/SYN, and are named SYN001-1.003.lop, SYN001-1.004.lop, and SYN001-1.005.lop. The quietness level is set to 2, thus suppressing all informational output except the lines showing what files are produced. Note that the file SYN001-1.g is automatically found in the generators directory.

Example

~/TPTP/TPTP2X> tptp2X -tmagic+shorten - < ~tptp/TPTP/Problems/GRP/GRP001-1.p
---------------------------------------------------------------------
TPTP2X directory      = /home/tptp/TPTP/TPTP2X
TPTP directory        = /home/tptp/TPTP
Prolog interpreter    = /usr/local/bin/sicstus
Files to convert      = -
Size                  =
Transformation        = magic+shorten
Format to convert to  = tptp
Output directory      = -
---------------------------------------------------------------------
%--------------------------------------------------------------------------
% File     : Shortened file, so there is no header
%--------------------------------------------------------------------------
input_clause(clause_1,axiom,
    [++equal(X1,X1)]).

... Lots of output omitted here for brevity

input_clause(clause_41,theorem,
    [--p2(c8,c7,c9)]).
%--------------------------------------------------------------------------
~/TPTP/TPTP2X>

This run uses the tptp2X script as a filter, to apply the non-Horn magic set transformation and then the symbol shortening transformation to GRP001-1.p. GRP001-1.p is fed in from standard input, and the output is written to standard output (thus all informational output is suppressed).

The tptp2X Interactive Mode

If the -i flag is set, the tptp2X script enters interactive mode after processing all other command line parameters. In interactive mode the user can change the value of any of the command line parameters. The user is prompted for the <TPTPFiles>, the <Size>, the <Transform>, the <Format>, and the <Directory>. In each prompt the current value is given. The user may respond by specifying a new value or by entering <cr> to accept the current value. The prompt-respond loop continues for each parameter until the user accepts the value for the parameter. Example

~/TPTP/TPTP2X> tptp2X -q0 -d~tptp/tmp -i
---- Interactive mode -----------------------------------------------
Files to convert      [Problems/*/*.p] : ../Problems/GRP/GRP001-1.p
Files to convert      [../Problems/GRP/GRP001-1.p] :
Size                  [] :
Transformation        [none] : lr+rm_equality:stfp
Transformation        [lr+rm_equality:stfp] :
Format to convert to  [tptp] : setheo
Format to convert to  [setheo] :
Output directory      [/home/tptp/tmp] :
---- End of Interactive mode ----------------------------------------
---------------------------------------------------------------------
TPTP2X directory      = /home/2/tptp/TPTP/TPTP2X
TPTP directory        = /home/2/tptp/TPTP
Prolog interpreter    = /usr/local/bin/sicstus
Files to convert      = ../Problems/GRP/GRP001-1.p
Size                  =
Transformation        = lr+rm_equality:stfp
Format to convert to  = setheo:sign
Output directory      = /home/tptp/tmp
---------------------------------------------------------------------
Made the directory /home/tptp/tmp/GRP
SICStus 3  #6: Mon Nov 3 18:32:08 MET 1997

... Lots of informational output omitted here for brevity

{/home/2/tptp/TPTP/TPTP2X/tptp2X.main compiled, 12080 msec 785600 bytes}

yes

yes
GRP001-1 -> /home/tptp/tmp/GRP/GRP001-1+lr+rm_eq_stfp.lop
~/TPTP/TPTP2X>

This run converts the problem GRP001-1 to a SETHEO format file. The literals are reversed and all equality clauses except reflexivity are removed. The top level output directory is specified as \verb/~/tptp/tmp, below which the subdirectory GRP is made. The output file is named GRP001-1+lr+eq_stfp.lop. Verbose mode is used, so all informational output is given.

The following subsections are only of interest to real Prolog users. If you do not want to use Prolog directly, skip to the next section.

Running tptp2X from within Prolog

The tptp2X utility may also be run from within a Prolog interpreter. The tptp2X.main file has to be loaded, and the entry point is then tptp2X/5, in the form:

?-tptp2X(<TPTPFile>,<Size>,<Transform>,<Format>,<Directory>).

The parameters are similar to the tptp2X script command line parameters. A summary, highlighting differences with "(!)", is given here. See Section Using tptp2X for parameter options.

<TPTPFile> is the name of a single TPTP file. If the file name is not absolute, then it is considered to be relative to the directory specified in the tptp_directory/1 fact in the tptp2X.config file (!). If the file name is user (!), then input is taken from standard input.
<Size> is either an integer, a : separated string of <Size>s, a <Low>..<High> integer size range, or a Prolog list of <Size>s (!). Each <Size> in a Prolog list of <Size>s is used to generate separate sets of formulae.
<Transform> is either a single transformation specifier, a + separated string of <Transform>s, or a Prolog list (!) of <Transform>s.
<Format> is an output format or a Prolog list (!) of output formats. An output file is written for each output format specified. For the otter format, the syntax is otter:<SoS>:[<Otter options>] (!), i.e., the Otter options form a Prolog list.
<Directory> specifies the directory in which the output files are to be placed. If the <Directory> is user (!) then output is sent to standard output.

Example

~/TPTP/TPTP2X> sicstus
SICStus 3  #6: Mon Nov 3 18:32:08 MET 1997
| ?- ['tptp2X.main'].
{consulting /home/2/tptp/TPTP/TPTP2X/tptp2X.main...}

... Lots of informational output omitted here for brevity

{/home/tptp/TPTP/TPTP2X/tptp2X.main consulted, 10750 msec 773088 bytes}

yes
| ?- tptp2X('Generators/SYN010-1.g',3:[2,4],[lr,cr]+magic,kif,'.').
{compiling /home/tptp/TPTP/Generators/SYN010-1.g...}
{/home/tptp/TPTP/Generators/SYN010-1.g compiled, 90 msec 4288 bytes}
SYN010-1 -> ./SYN010-1.003:002+lr+nhms.kif
SYN010-1 -> ./SYN010-1.003:002+cr+nhms.kif
SYN010-1 -> ./SYN010-1.003:004+lr+nhms.kif
SYN010-1 -> ./SYN010-1.003:004+cr+nhms.kif

yes
| ?- ^D
~/TPTP/TPTP2X>

This run generates two sizes of the generic problem SYN010-1, and does two transformation sequences on each of the two sets of clauses, to produce four output files. The sizes are 3:2 and 3:4. The first transformation sequence is literal order reversal followed by the non-Horn magic set transformation, and the second transformation sequence is clause order reversal followed by the non-Horn magic set transformation. The files are output in KIF format in the current directory. The file names are
SYN010-1.003:002+lr+nhms.kif, SYN010-1.003:002+cr+nhms.kif,
SYN010-1.003:004+lr+nhms.kif, and SYN010-1.003:004+cr+nhms.kif.

Note that the TPTP file name is quoted in the query, to form a Prolog atom.

Writing your own Transformations and Output Formats

The transformations and output formatting are implemented in Prolog, in the files transform.<TRAN> and format.<ATP>, respectively. It is simple to add new transformations and output formats to the tptp2X utility, by creating new transformation and format files. New files should follow the structure of the existing files. Typically, a new file can be created by modifying a copy of one of the existing files.

The entry point in a transformation file is <Transform>/6. The first three arguments are inputs: a list of the problem's formulae, the variable dictionary (a bit complicated), and the transformation specification. The next three arguments are outputs: the transformed formulae, the transformed variable dictionary (typically the same as the input dictionary), and the transformation suffix. As well as the <Transform>/6 entry point, a <Transform>_file_information/2 fact must be provided. The two arguments of the <Transform>_file_information/2 fact are the atom transform and a description of the possible transformation specifications (as used in the third argument of <Transform>/6). See the existing transform.<TRAN> files for examples.

The entry point in a format file is <Format>/3. The three arguments are inputs: the format specification, a list of the problem's formulae, and the file header information. (It is not necessary to output a file header here; this information is available only for producing supplementary documentation.) As well as the <Format>/3 entry point, a <Format>_format_information/2 fact and a <Format>_file_information/2 fact must be provided. The two arguments of the <Format>_format_information/2 fact are a character that can be used to start a comment in the output file and the format extension, both as Prolog atoms. The two arguments of the <Format>_file_information/2 fact are the atom format and a description of the possible format specifications. See the existing format.<ATP> files for examples.

New transformation and format files must be compiled in with the other tptp2X files. This is done by adding a compile query in the tptp2X.main file, alongside the queries that compile in the existing files.

If you need help, please contact Geoff Sutcliffe.

Writing your own Problem Generators

The TPTP generators are implemented in Prolog. It is simple to write new generators. New files should follow the structure of the existing files.

The entry point in a generator file is <Problem name>/3, where <Problem name> is the file name without the .g suffix. The first argument is an input: the size parameter for generation. The second and third arguments are outputs: the formulae generated and the % Status of the formulae. The formulae must be a Prolog list of formulae in TPTP format. A <Problem name>_file_information/3 fact must also be provided. The three arguments of the fact are the atom generator, a description of the possible size parameters, and the TPTP size for this problem (this is hard to determine!). See the existing generator files for examples.

If you need help, please contact Geoff Sutcliffe.

The `tptp1T` Script

The tptp1T script selects lines from either the FOFProblemStatistics file or the CNFProblemStatistics file, by problem characteristics.

The tptp1T script is written in perl.

Installation

Installation of the tptp1T utility requires simple changes in the tptp1T script. These changes can be made by running tptp1T_install, which will prompt for required information. Otherwise, to install tptp1T by hand, in the tptp1T script file $TPTPDirectory must be set to the absolute path name of the TPTP directory.

Using tptp1T

The use of this script is:

tptp1T CNF|FOF [-f <ProblemFile>] {[-]<Constraint>}

The CNF or FOF argument indicates which statistics file to select lines from. The optional -f <ProblemFile> argument specifies the name of a file containing TPTP problem names. tptp1T will select statistics file lines for only those problems whose names appear in the <ProblemFile>. The problem names (without the .p extension) must appear one per line in the <ProblemFile>, and lines that start with # are ignored. The <Constraint>s specify required problem characteristics, all of which must be satisfied for the statistics file line to be selected. A - may be prepended to negate the meaning of any <Constraint>. The possible <Constraint>s are:

Domain {<TPTP domain name>} to select problems from these TPTP domains.
Standard, Incomplete, Augmented, Especial, Biased to select problems with this % Version status (see Section The Header Section).
Rating <Minimum> <Maximum> to select problems whose \% Rating is in the specified range.
Theorem, Satisfiable, Unsatisfiable, Unknown, Open to select FOF problems with this % Status. In addition, NonTheorem may be used to select both Satisfiable and Unsatisfiable problems.
Unsatisfiable, Satisfiable, Tautology, Unknown, Open to select CNF problems with this % Status. In addition, NonTheorem may be used to select Satisfiable problems.
Predicates <Minimum> <Maximum> to select problems with a number of predicate symbols in the specified range.
Propositional to select propositional problems.
Variables to select problems with variables.
MinimalPredicateArity <Minimum> <Maximum> to select problems whose minimal predicate arity is in the specified range, and MaximalPredicateArity <Minimum> <Maximum> to select problems whose maximal predicate arity is in the specified range.
Equality or PureEquality to select problems with equality, or problems with purely equality literals.
Functions <Minimum> <Maximum> to select problems with a number of function symbols in the specified range (constants are considered to be functions of arity 0).
MinimalFunctionArity <Minimum> <Maximum> to select problems whose minimal function arity is in the specified range, and MaximalFunctionArity <Minimum> <Maximum> to select problems whose maximal function arity is in the specified range.
Horn or NonHorn to select CNF problems which are Horn or non-Horn.
RangeRestricted to select CNF problems that are range restricted.
AverageLiterals <Minimum> <Maximum> to select CNF problems in which the average number of literals per clause is in the specified range.
UnitEquality to select CNF problems that have only unit equality clauses.

Utilities

The tptp2X Utility

Installation

Using tptp2X

The tptp2X Output Files

The tptp2X Interactive Mode

Running tptp2X from within Prolog

Writing your own Transformations and Output Formats

Writing your own Problem Generators

The tptp1T Script

Installation

Using tptp1T

The `tptp1T` Script