Input to a TPI system can contain both logical formulae and TPI command formulae. The two types of formulae are processed together, in the order they appear in the file. (This makes the order of the formulae relevant, which is counter to the TPTP principle that formulae can be reordered, cut-and-pasted, merged, etc. However, TPI command formulae are non-logical, so this deviation from the principle seems tolerable.) Logical formulae are processed and stored as usual, and command formulae are obeyed.
The logical formulae that have been processed and stored by a TPI system are initially in an active state. Logical formulae can be "deactivated", placing them into an inactive state, so that they do not appear to exist. Inactive formulae are not used in any processing. Inactive logical formulae can be "activated" so that they are again used in processing. In addition to being active or inactive, logical formulae also belong to one or more named groups. All logical formulae belong to the group tpi, all premises (axioms, hypothesiss, definitions, lemmas, etc.) belong to the group tpi_premises, all conjectures and negated_conjectures belong to the group tpi_conjectures, and all logical formulae can belong to multiple other user-defined groups. The TPI language provides commands for manipulating groups of logical formulae.
tpi(1,execute,'SZS_STATUS' = 'E---1.6/eprover --auto --cpu-limit=$getargv(0) --tstp-format $getgroups(tpi)').
Using non-terminals from the TPTP syntax, each Command is an <atomic_word>, and CommandDetails is either a <proposition>, a <defined_infix_formula> in the form of an equality, or a <fol_infix_unary>. in the form of an inequality. This use of existing TPTP syntax makes it easy to modify an existing parser for the TPTP language to read TPI commands. The Source and UsefulInfo are optional as usual.
In order for a command's CommandDetails to be parsed as a <proposition>, <defined_infix_formula>, or <fol_infix_unary>., it is often necessary to quote the whole CommandDetails or the operands of the (in)equality. For example, the lefthand side of the equality that forms the CommandDetails of the example TPI command above is an environment variable that starts with an uppercase letter. It has to be quoted so that a TPTP parser does not interpret it as a logic variable.
TPI command formulae can use three new TPTP interpreted functors:
An example of TPI command formulae interleaved with logical formulae is:
tpi(1,input,'Axioms/SET006+0.ax').
fof(thI14,conjecture,
( ! [A] : equal_set(union(A,A),A) )).
tpi(2,execute,
'SZS_STATUS' = 'E---1.6/eprover --auto --cpu-limit=$getargv(0) --tstp-format $getgroups(tpi)').
tpi(3,write,'Status: ' & $getenv('SZS_STATUS')).
tpi(4,exit,exit(27)).
With those formulae in an input file named Simple.p, a TPI system
would be invoked like this:
my_tpi_system Simple.p 300
The first line reads in a file of axioms, after which a conjecture is
provided.
The third line invokes the ATP system E, with a 300s CPU time
limit taken from the command line.
The SZS status is stored in the environment
variable SZS_STATUS.
The fourth line writes that status to stdout,
after which the last lines ends the processing.
Action: Inputs the named file. The logical formulae in the file are put in the named group if one is specified (it's the same as putting a start_group - end_group pair around the input command without a group name - see below). This has the same effect as a TPTP include directive.
Examples:
tpi(1,input,'/TPTP/Axioms/SET001-0.ax').
tpi(2,input,some_axioms = '/TPTP/Axioms/SET001-0.ax').
Action: The active logical formulae in the named group, or all logical formulae if no group is specified, are output to the named file. The file name can be stdout, with the obvious meaning.
Examples:
tpi(1,output,'OutputFile.txt').
tpi(2,output,'OutputFile.txt' = some_axioms).
tpi(3,output,stdout).
Action: The named logical formula is deactivated.
Examples:
tpi(1,deactivate,left_identity).
Action: The named logical formula is activated.
Examples:
tpi(1,activate,left_identity).
Action: Sets the role of the named logical formula to the atomic value, which must be a valid TPTP formula role, e.g., axiom, lemma, conjecture, etc.
Examples:
tpi(1,set_role,midpoint = lemma).
Action: The named logical formula is deleted.
Examples:
tpi(1,delete,left_identity).
Action: Adds all subsequent logical formulae to the named group, until a corresponding end_group command is encountered. Groups do not have to be contiguous in the input, i.e., there can be multiple start_group - end_group pairs with the same group name.
Examples:
tpi(1,start_group,some_axioms).
Action: Stops adding logical formulae to the named group.
Examples:
tpi(1,end_group,some_axioms).
Action: The logical formula in the named group are deactivated.
Examples:
tpi(1,deactivate_group,some_axioms).
Action: The logical formulae in the named group are activated.
Examples:
tpi(1,activate_group,some_axioms).
Action: The logical formulae in the named group are deleted.
Examples:
tpi(1,delete_group,some_axioms).
tpi(2,delete_group,tpi).
Action: Sets the environment variable to the atomic value. An expected use of environment variables is to pass values to ATP systems run through execute commands - see below.
Examples:
tpi(1,setenv,'TPTP' = '/home/geoff/tptp/TPTP').
tpi(2,setenv,'CPU_LIMIT' = 300).
Action: Waits for an environment variable to become set. The <environment_variables> can be a single environment variable, or a disjunction in which case the TPI system waits for any one of them to become set. A main use of waitenv is to coordinate with execute_async commands - see below.
Examples:
tpi(1,waitenv,'ASYNC_SZS_STATUS').
tpi(2,waitenv,'EP_SZS_STATUS' | 'VAMPIRE_SZS_STATUS').
Action: Unsets the environment variable.
Examples:
tpi(1,unsetenv,'TPTP').
Action: Creates a new temporary file and places the name of the file in the environment variable. All temporary files created this way are deleted when a clean command is executed.
Examples:
tpi(1,mktemp,'TEMP_FILENAME').
Action: Sets the logic/semantics within which the active logical formulae should be processed.
Examples:
tpi(1,set_logic,qmltp([ml(a,modal_s4),ml(b,modal_d)])).
Action: If the argument is self then the TPI system processes all the active logical formulae using its own reasoning process. Thus execute,self is meaningful only in the context of an ATP system, which runs its reasoning process on all the active logical formulae. If the argument is an <command> then any embedded $get* terms are replaced by the corresponding values, and the resulting <command> is executed. If the optional equation is provided, the SZS status from reasoning is placed into the environment variable. The TPI system waits for the execution to complete.
For backward compatibility, a %s in an <command> is equivalent to $getgroups(tpi). Note that execute can be used to run arbitrary commands, e.g., /bin/date to output the date and time.
When a TPI system is reading the top level file, i.e., not an included or input file, if it reaches the end of the file without finding an exit command then an implicit execute,self is performed. Thus a conventional ATP system that is given a file of logical formulae as its input, and runs its reasoning process on the logical formulae after reading the complete file, is a TPI system.
Examples:
tpi(1,execute,self).
tpi(2,execute,'E---1.6/eprover --auto --tstp-format $getgroups(tpi)').
tpi(3,execute,'SZS_STATUS' = 'E---1.6/eprover --auto --tstp-format --cpu-limit=$getenv(0) $getgroups(some_axioms,the_conjectures)').
tpi(4,execute,'MutzaBall---1.0/gomutza -a $getgroups(some_axioms,more_axioms) -c $getgroups(the_conjectures) -t 300').
tpi(5,execute,'/bin/date').
Action: Runs like execute, but processing of the current TPI file continues concurrently with the execution. All processes created this way are terminated when a clean command is executed.
Examples:
tpi(1,execute_async,'ASYNC_SZS_STATUS' = 'E---1.6/eprover --auto --tstp-format $getgroups(tpi)').
Action: Runs like execute, then deletes the groups specified by any $getgroups terms in the <command> (like delete_group), and uses the output from the execution as input. As such a filter is equivalent to a sequence such as:
tpi(1,mktemp,'TEMP_FILENAME').
tpi(2,execute,'the_filter_command_details $getgroups(foo,blah) > $TEMP_FILENAME').
tpi(3,delete_group,foo).
tpi(4,delete_group,blah).
tpi(5,input,$getenv('TEMP_FILENAME')).
Examples:
Action: Runs like execute, and uses the output from the execution as input. Logical formulae can be passed to the generator to provide context, using $getgroups terms.
Examples:
tpi(1,generate,'RandomProblemGenerator').
tpi(2,generate,'SZS_STATUS' = 'LemmaGenerator --context=$getgroups(tpi)').
Action: Checks the equality or inequality. The only <term>s allowed are <atomic_word>s, <integer>s, and $get* terms. If the assertion fails a write,'Assertion failed: ' & negated_assertion command, followed by an exit,exit(1) command are performed.
Examples:
tpi(1,assert,$getenv('SZS_STATUS') = 'Satisfiable').
Action: Outputs the <output_data> to stdout. The <output_data> can be atomic, or a conjunction in which case each of the conjuncts is output.
Examples:
tpi(1,write,'--------------------').
tpi(2,write,$getenv('SZS_STATUS')).
tpi(3,write,'Conjecture status: ' & $getenv('SZS_STATUS')).
Action: Any processes started with execute_async commands that are still running are stopped. Any files created with mktemp commands are deleted.
Examples:
tpi(1,clean,clean).
Action: A clean command is executed, then the TPI system
stops and exits.
If an
Examples:
tpi(1,exit,exit).
tpi(2,exit,exit(27)).
tpi(1,input,'Axioms/SYN001+1.ax').
fof(another,axiom,pp => qq).
fof(a,conjecture,qq).
The following example shows how some common core axioms (in SYN001+1.ax) can be loaded, then used in conjunction with different conjecture-specific axioms using explicit execute,selfs. Command 1 inputs a file of axioms, after which command 2 starts a group named try_these. Another axiom and a conjecture are put into the group, which is ended by command 3. Command 4 starts the TPI system's (necessarily an ATP system) reasoning process. After the execution is completed command 5 deletes the axiom and conjecture in the group, and yet another axiom and another conjecture are provided. The axioms that were input from the file also remain. Command 6 starts the TPI system's reasoning process again. When execution is completed command 7 stops the TPI system.
tpi(1,input,'Axioms/SYN001+1.ax').
tpi(2,start_group,try_these).
fof(another,axiom,q).
fof(a,conjecture,qq).
tpi(3,end_group,try_these).
tpi(4,execute,self).
tpi(5,delete_group,try_these).
fof(yet_another,axiom,r).
fof(and_another,conjecture,rr).
tpi(6,execute,self).
tpi(7,exit,exit).
The following example shows how different groups of axioms can be used with a conjecture. Commands 1 and 2 start two groups of axioms. Command 3 loads the axioms that are unique to the old group, after which command 4 starts the group of new axioms. Command 5 loads axioms that are common to the old and new groups, command 6 ends the old group, command 7 loads axioms that are unique to the new group, and commands 8 and 9 end the groups. Command 10 loads another set of axioms, which are part of only the {\tt tpi} group. Commands 11 and 12 put the conjecture into a group. The next eight pairs of commands try prove the conjecture from various combinations of the axioms, and report the results. Commands 13 and 14 use just the old axioms, commands 15 and 16 use just the new axioms, commands 17 and 18 use both the old and new axioms, and finally commands 19 and 20 use all the available axioms. When execution is completed command 21 stops the TPI system.
tpi(1,start_group,old_and_new_axioms).
tpi(2,start_group,old_axioms).
tpi(3,input,'Axioms/SYN001+1.ax').
tpi(4,start_group,new_axioms).
tpi(5,input,'Axioms/SYN001+2.ax').
tpi(6,end_group,old_axioms).
tpi(7,input,'Axioms/SYN002+1.ax').
tpi(8,end_group,new_axioms).
tpi(9,end_group,old_and_new_axioms).
tpi(10,input,'Axioms/SYN003+1.ax').
tpi(11,start_group,the_conjecture).
fof(a,conjecture,qq).
tpi(12,end_group,the_conjecture).
tpi(13,execute,
'SZS_STATUS' = '$TPTP_HOME/Systems/E---1.6/eprover -s --auto --cpu-limit=300 --tstp-format $getgroups(old_axioms,the_conjecture)').
tpi(14,write,'Conjecture status for old axioms:' & $getenv('SZS_STATUS')).
tpi(15,execute,
'SZS_STATUS' = '$TPTP_HOME/Systems/E---1.6/eprover -s --auto --cpu-limit=300 --tstp-format $getgroups(new_axioms,the_conjecture)').
tpi(16,write,'Conjecture status for replacement axioms:' & $getenv('SZS_STATUS')).
tpi(17,execute,
'SZS_STATUS' = '$TPTP_HOME/Systems/E---1.6/eprover -s --auto --cpu-limit=300 --tstp-format $getgroups(old_and_new_axioms,the_conjecture)').
tpi(18,write,'Conjecture status for old and new axioms:' & $getenv('SZS_STATUS')).
tpi(19,execute,
'SZS_STATUS' = '$TPTP_HOME/Systems/E---1.6/eprover -s --auto --cpu-limit=300 --tstp-format $getgroups(tpi)').
tpi(20,write,'Conjecture status for all axioms:' & $getenv('SZS_STATUS')).
tpi(21,exit,exit).
The following example shows how to check the axioms for satisfiability before making a proof attempt. Two axioms are provided, after which command 1 invokes the Paradox ATP system to establish that the axioms are satisfiable. Command 2 writes the SZS status returned by Paradox, and command 3 asserts that the status must be Satisfiable (it obviously is). A conjecture is then provided, and command 4 invokes the E ATP system to prove it's a theorem. Command 5 writes the SZS status returned by E, after which command 6 stops the TPI system.
fof(an,axiom,p).
fof(another,axiom,p => q).
tpi(1,execute,
'SZS_STATUS' = '$TPTP_HOME/Systems/Paradox---4.0/paradox --time 300 --tstp $getgroups(tpi)').
tpi(2,write,'Axiom status:' & $getenv('SZS_STATUS')).
tpi(3,assert,$getenv('SZS_STATUS') = 'Satisfiable').
fof(a,conjecture,q).
tpi(4,execute,
'SZS_STATUS' = '$TPTP_HOME/Systems/E---1.6/eprover -s --auto --cpu-limit=300 --tstp-format $getgroups(tpi)').
tpi(5,write,'Conjecture status:' & $getenv('SZS_STATUS')).
tpi(6,exit,exit).
The following example is a variant of the last one, with the axioms being checked for satisfiability in parallel with the proof attempt. Two axioms are provided, after which command 1 invokes the Paradox ATP system to run asynchronously to establish that the axioms are satisfiable. A conjecture is then provided, and command 2 invokes the E ATP system to prove it's a theorem. Command 3 makes the TPI system wait for Paradox to complete its execution, after which command 4 writes the SZS statuses returned by Paradox and E. Command 5 stops the TPI system.
fof(an,axiom,p).
fof(another,axiom,p => q).
tpi(1,execute_async,
'ASYNC_SZS_STATUS' = '$TPTP_HOME/Systems/Paradox---4.0/paradox --time 300 --tstp $getgroups(tpi)').
fof(a,conjecture,q).
tpi(2,execute,
'SZS_STATUS' = '$TPTP_HOME/Systems/E---1.6/eprover -s --auto --cpu-limit=300 --tstp-format $getgroups(tpi)').
tpi(3,waitenv,'ASYNC_SZS_STATUS').
tpi(4,write,'Axioms status: ' & $getenv('ASYNC_SZS_STATUS')
& ' Conjecture status: ' & $getenv('SZS_STATUS')).
tpi(5,exit,exit).
The following example shows how a proved conjecture can be used as a lemma for a subsequent conjecture. It also (somewhat redundantly) illustrates deactivation and activation of logical formulae. The first two axioms are loaded as a group. The third axiom is not necessary for proving the subsequent conjecture, so it is deactivated before command 4 proves the conjecture from the first two axioms. Commands 5 and 6 write and verify the result. Command 7 changes the role of the proved conjecture to a lemma (i.e., it can be used like an axiom), command 8 activates the necessary axiom, command 9 deactivates the first two axioms, and a new conjecture is loaded. Command 10 proves the new conjecture, and command 11 writes out the result. Command 12 stops the TPI system.
tpi(1,start_group,about_a).
fof(a,axiom,a).
fof(ab,axiom,a=>b).
tpi(2,end_group,about_a).
fof(bc,axiom,b=>c).
tpi(3,deactivate,bc).
fof(b,conjecture,b).
tpi(4,execute,'SZS_STATUS' = 'E---1.8 300 $getgroups(tpi)').
tpi(5,write,'SZS_STATUS for b is ' & '$getenv(SZS_STATUS)').
tpi(6,assert,$getenv('SZS_STATUS') = 'Theorem').
tpi(7,set_role,b = lemma).
tpi(8,activate,bc).
tpi(9,deactivate_group,about_a).
fof(c,conjecture,c).
tpi(10,execute,'SZS_STATUS' = 'E---1.8 300 $getgroups(tpi)').
tpi(11,write,'SZS_STATUS for c is ' & '$getenv(SZS_STATUS)').
tpi(12,exit,exit).
The following example shows how the logical formulae can be filtered. Command 1 inputs a file containing a large theory problem, i.e., the file contains a conjecture and very many axioms of which only a few are necessary for a proof. Command 2 inputs some extra axioms. Command 3 invokes the E ATP system asynchronously to try to prove the conjecture from all the axioms (the --satauto option supresses E's internal axiom selection process). While E is running command 5 invokes the SInE system to select the axioms from the lt_problem group that are expected to be necessary for a proof, replacing the very many axioms in the group by the selected axioms (the conjecture is also retained by SInE). The selected axioms and the conjecture are placed in the sine_problem group by commands 4 and 6. Command 7 outputs the selected axioms and conjecture to the file SInEProblem.p. Command 8 invokes the E ATP system to prove the conjecture from the selected axioms. Command 9 makes the TPI system wait for the first instance of E to complete its execution, after which commands 10 and 11 write the SZS statuses returned by E. Command 12 stops the TPI system.
tpi(1,input,lt_problem = 'LTProblem.p').
tpi(2,input,'ExtraLTAxioms.ax').
tpi(3,execute_async,
'ASYNC_SZS_STATUS' = '$TPTP_HOME/Systems/E---1.6/eprover -s --satauto --cpu-limit=300 --tstp-format $getgroups(tpi)').
tpi(4,start_group,sine_problem).
tpi(5,filter,
'$TPTP_HOME/Systems/SInESelect---1.8/run_sine_select --mode axiom_selection $getgroups(lt_problem)').
tpi(6,end_group,sine_problem).
tpi(7,output,'SInEdProblem.p' = sine_problem).
tpi(8,execute,
'SZS_STATUS' = '$TPTP_HOME/Systems/E---1.6/eprover -s --satauto --cpu-limit=300 --tstp-format $getgroups(sine_problem)').
tpi(9,waitenv,'ASYNC_SZS_STATUS').
tpi(10,write,'Conjecture status with all axioms:' & $getenv('ASYNC_SZS_STATUS')).
tpi(11,write,'Conjecture status with selected axioms:' & $getenv('SZS_STATUS')).
tpi(12,exit,exit).
The following example shows how competition parallelism can be implemented. Command 1 inputs the problem. Commands 2 and 3 invoke the ATP systems asynchronously to try to prove the theorem at the same time. Command 4 makes the TPI system wait for either of the ATP systems to complete their execution. Command 5 writes out the SZS statuses returned by the ATP systems - note that it is likely that only one of them will have returned a status. Command 6 stops the TPI system. This implementation relies on the TPI system stopping the second ATP system that might still be running when command 6 is executed.
tpi(1,input,'Simple.p').
tpi(2,execute_async,'EP_SZS' = 'E---1.6/eprover -s --auto --cpu-limit=300 --tstp-format $getgroups(tpi)').
tpi(3,execute_async,'VAMPIRE_SZS' = 'Vampire---2.6/vampire_rel --proof tptp --output_axiom_names on --mode casc -t 300 $getgroups(tpi)').
tpi(4,waitenv,'EP_SZS' | 'VAMPIRE_SZS').
tpi(5,write,'EP_SZS = $getenv(EP_SZS) VAMPIRE_SZS = $getenv(VAMPIRE_SZS)').
tpi(6,exit,exit).
The following example shows how to write a meta-prover. With the TPI commmands in a file named Meta.tpi, and the problem in a file named Simple.p, a TPI system would be invoked like this:
my_tpi_system Meta.tpi 'E---1.6/eprover --auto $getgroups(tpi)' Simple.p
Command 1 inputs the file of formulae named on the command line, and command 2
invokes the ATP system named on the command line.
Command 3 writes the SZS status returned by the ATP system.
Command 4 stops the TPI system.
tpi(1,input,$getenv(1)).
tpi(2,execute,'SZS_VAR' = '$getargv(0)').
tpi(3,write,'The SZS status is' & $getenv('SZS_VAR')).
tpi(4,exit,exit).
As part of the TPTP World, the TPII is distributed alongside the SystemOnTPTP utility that hosts and executes ATP systems in a flexible way. TPII's execute and execute_async commands have been extended to support direct access to the SystemOnTPTP utility. If the ATP command starts with a system name in the form System---Version then that system will be executed by the SystemOnTPTP utility. The Version can be empty, in which case the latest version of the System will be used. The System---Version must be followed by an integer CPU time limit, and a single $getgroups term to specify the formulae to be passed to the SystemOnTPTP utility. Some examples are:
tpi(1,execute,'E---1.8 300 $getgroups(tpi)').
tpi(2,execute,'SZS_STATUS' = 'E--- $getargv(0) $getgroups(axioms,my_conjectures)').
This makes it easy to parameterize the competition parallelism example.
With the TPI commands in a file named CompPar.tpi, TPII
would be invoked with
TPII CompPar.tpi E---1.6 Vampire---2.6 300 Simple.p
The TPI commands in CompPar.tpi would be changed to
tpi(1,input,$getargv(3)).
tpi(2,execute_async,'SZS_RESULT_1' = '$getargv(0) $getargv(2)').
tpi(3,execute_async,'SZS_RESULT_2' = '$getargv(1) $getargv(2)').
tpi(4,waitenv,'SZS_RESULT_1' | 'SZS_RESULT_2').
tpi(5,write,'$getargv(0) SZS_RESULT = $getenv(SZS_RESULT_1) '
& '$getargv(1) SZS_RESULT = $getenv(SZS_RESULT_2)').
tpi(6,exit,exit).
Similarly, the meta-system can be parameterized, by invoking TPII with
the command line
TPII Meta.tpi E---1.6 300 Simple.p
and the TPI commands in Meta.tpi changed to
tpi(1,input,$getargv(2)).
tpi(2,execute,'SZS_VAR' = '$getargv(0) $getargv(1)').
tpi(3,write,'The SZS status is' & $getenv('SZS_VAR')).
tpi(4,exit,exit).
For execute and execute_async commands, TPII scans the
ATP system's output for a line that contains the string "SZS status", which
is the standard prefix for an SZS ontology result.
The first time such a string is found the SZS status is expected to be
the next word in that line.
TPII is minimally robust against ill-formed input, and exits if any errors are found. If there is an error then 1 is returned to the operating system as the exit status (so this should be avoided as a user exit code).