| WARNING: For historical reasons TPTP2X omits the quotes around some constants and function symbols that should be 'Quoted', e.g., as found in PUZ001+2. I'm really sorry about this - it's an artifact of a very generic printing framework that became overloaded when THF formulae came into the TPTP. Changing it would be a HUGE task, and now there's TPTP4X that is better in most respects. |
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<Level> 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:
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.
Examples
~/TPTP/TPTP2X> tptp2X -tfr,random -f prover9 PUZ001+1This applies two separate transformations to the problem ALG001-1. The transformations are formula order reversal and formula order randomizing. The transformed problems are output in prover9 format, in a directory prover9/PUZ below the current directory. The file names are PUZ001+1+fr.in and PUZ001+1+ran.in.
~/TPTP/TPTP2X> tptp2X -q2 -s3..5 -fotter -d~tptp/tmp SYN001-1.gThis 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.
~/TPTP/TPTP2X> tptp2X -tmagic+shorten - < ~tptp/TPTP/Problems/GRP/GRP001-1.pThis 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).
?-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.
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 the TPTP developers.
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 the TPTP developers.
The TPTP4X usage is Usage: tptp4X <options> <files>.
The options are (defaults in ()s):
The TPTP2T script is written in perl.
tptp2T [-f FileName] [-q1 or -q2 or -q3] [-pp or -ps or -pps] {[-]Constraint {[and/or] [-]Constraint}}
A problem Constraint is selected from:
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 TPTP4X Utility
The TPTP4X utility is a multi-functional utility for reformatting,
transforming, and generating TPTP problem files.
It is the successor to the TPTP2X utility, and offers some of the same
functionality, and some extra functionality.
TPTP4X is written in C, and is thus faster than TPTP2X.
The TPTP2T Script
The TPTP2T script selects lines from either the
ProblemAndSolutionStatistics
file, by problem and solution characteristics.
Installation
Installation of the TPTP2T utility requires simple changes in the
tptp2T script.
These changes can be made by running tptp2T_install, which will prompt
for required information.
Using TPTP2T
The use of this script is:
The Constraints specify required problem and solution
characteristics that must be satisfied for the statistics file
line(s) to be selected.
There are two sets of constraints, problem constraints and solution
constraints, which apply to problem lines and solution lines separately.
For a solution line to be printed, the problem line it accompanies must
pass all problem constraints, if any are provided.
Different sets of solution constraints can be applied to different systems
individually.
A solution <Constraint> is selected from:
Only the listed problem domains.
One of THF, TXF, TFF, FOF,
CNF, ANY. Default is ANY.
One of Theorem, CounterSatisfiable,
Unsatisfiable, Satisfiable,
Unknown, Open.
In the range 0.00 (easiest) to 1.00 (hardest)
The number of formulae in the problem.
The number of unit formulae
The number of type formulae
The number of atoms.
The number of equality atoms.
Only problems that use equality.
Only problems that use only equality.
Only problems with only unit-equality clauses/formulae.
Only problems with FOOL logic atoms/terms
Only problems that use arithmetic.
The number of types used
The number of distinct symbols
The number of predicates
The minimal predicate arity
The maximal predicate arity in TFF/FOF/CNF problems.
Only propositional (only preducates of arity 0) problems
The number of functions
The minimal function arity
The maximal function arity
Only problems with variables.
Only problems with PI variables.
ATP system which found a solution (ANY for any system).
Solutions with this result, or a result lower in the SZS ontology.
Solutions found in this time range.
Solutions with this output, or an output lower in the SZS ontology.
The number of formulae in the solution.
The number of leaves in the solution (for DAGs).
The depth of the solution (for DAGs, from an axiom to a root).
The number of atoms in the soltuion.
Only solutions that use equality.
Only solutions that use arithmetic.
The ratio of solution leaves to problem formulae.
The ratio of solution leaves to solution depth.