TPTP Format for Derivations
Introduction
A derivation is a directed acyclic graph (DAG) whose leaf nodes are formulae
from the input, whose interior nodes are formulae inferred from parent
formulae, and whose root nodes are the final derived formulae.
For example, a proof of a FOF theorem from some axioms, by refutation of the
CNF of the axioms and negated conjecture, is a derivation whose leaf nodes
are the FOF axioms and conjecture, whose internal nodes are formed from the
process of clausification and then from inferences performed on the clauses,
and whose root node is the false formula.
The information required to record a derivation is, minimally, the leaf
formulae, and each inferred formula with references to its parent formulae.
More detailed information that may be recorded and useful includes:
the role of each formula; the name of the inference rule used in each
inference step; sufficient details of each inference step to deterministically
reproduce the inference; and the semantic relationships of inferred formulae
with respect to their parents.
Specifying a TPTP Format Derivation
The top level building blocks of TPTP files are annotated formulae, include
directives, and comments.
An annotated formula has the form:
language(name,role,formula,source,useful info).
The source and useful information are optional.
The languages currently supported are
thf - formulae in typed higher-order form,
tff - formulae in typed first-order form,
fof - formulae in first-order form,
and
cnf - formulae in clause normal form.
A derivation written in the TPTP language is a list of annotated formulae.
Each leaf formula should have a file record, and
each inferred formula has an inference record.
(This is a description of an ordinary derivation - the TPTP language can
do more than this.)
- Name:
The name is a word starting lower case, e.g., original_f1, or a
single quoted word, e.g., 'A crazy $ name'.
- Role:
The role is typically one of
axiom for axiom leaves,
conjecture for FOF conjecture leaves,
negated_conjecture for negated CNF conjectures, or
plain for inferred formulae.
A full list of the posssible roles is
in the TPTP syntax.
- Logical formula:
The logical formula uses a consistent and easily understood notation
that can be seen in the
BNF for THF,
BNF for TFF,
BNF for FOF,
and
BNF for CNF.
If a formula introduces a new symbol, e.g., a Skolem function, the new name should follow the
TSTP conventions for new symbol
names, and be correspondingly documented in the source field.
- Source: This is normally either a file record or an inference record.
- File record:
A file record contains the problem file name and the corresponding annotated formulae
name in the problem file.
- Inference record:
An inference record contains the inference rule name (starting with lowercase),
a list of useful inference information, and a list of references to its parent formulae.
Common types of useful inference information are:
- The semantic relationship of the formula to its parents as an
SZS ontology value in a status record, e.g., status(thm).
- An indicator that special reasoning was involved, e.g., theory(equality)
or theory(ac).
- Special information about recognized types of inferences, e.g., splitting, in a
record whose principle symbol is the inference rule name, whose first argument is
a keyword in TPTP conventions, and whose second argument is a list of useful
information about that type of inference.
- Explicit splitting, as done by SPASS:
The keyword is split.
The list of useful information can contain a position that record the
history of splits down to this formula.
Each split in the history adds an 's' and a digit to the position so far,
where the digit records the split child number.
For example, the third split child of a formula that is in the branch of the
first split child of an earlier split would have the position
position(s1s3).
- Details of new symbols introduced in the inference.
- Useful information:
The useful information in a []ed list of 'Prolog-like' terms.
Example Derivation
Consider the toy FOF problem in the problem quick guide.
Here is a derivation recording a proof by refutation of the CNF (adapted from the one produced
by the ATP system EP):
%--------------------------------------------------------------------
fof(3,axiom,(
grade(john) = f ),
file('CreatedEqual.p',john_failed)).
fof(4,axiom,(
? [X3] :
( human(X3)
& grade(X3) = a ) ),
file('CreatedEqual.p',someone_got_an_a)).
fof(5,axiom,(
a != f ),
file('CreatedEqual.p',distinct_grades)).
fof(7,conjecture,(
? [X3] :
( human(X3)
& X3 != john ) ),
file('CreatedEqual.p',someone_not_john)).
fof(8,negated_conjecture,(
~ ? [X3] :
( human(X3)
& X3 != john ) ),
inference(assume_negation,[status(cth)],[7])).
cnf(14,plain,
( grade(john) = f ),
inference(split_conjunct,[status(thm)],[3])).
fof(16,plain,
( human(esk1_0)
& grade(esk1_0) = a ),
inference(skolemize,[status(sap)],[4])).
cnf(17,plain,
( grade(esk1_0) = a ),
inference(split_conjunct,[status(thm)],[16])).
cnf(18,plain,
( human(esk1_0) ),
inference(split_conjunct,[status(thm)],[16])).
cnf(19,plain,
( a != f ),
inference(split_conjunct,[status(thm)],[5])).
fof(22,negated_conjecture,(
! [X3] :
( ~ human(X3)
| X3 = john ) ),
inference(fof_nnf,[status(thm)],[8])).
cnf(24,negated_conjecture,
( X1 = john
| ~ human(X1) ),
inference(split_conjunct,[status(thm)],[22])).
cnf(25,negated_conjecture,
( john = esk1_0 ),
inference(spm,[status(thm)],[24,18])).
cnf(28,plain,
( f = a ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[17,25]),14])).
cnf(29,plain,
( $false ),
inference(sr,[status(thm)],[28,19])).
%--------------------------------------------------------------------
Checking a Derivation
A quick way to check the syntax of a derivation is to run it through tptp4X, available online in
SystemOnTSTP.
Select the "TSTP formulae" option and paste the formulae into the text box.
Select tptp4X as the system, and ensure that the output mode is System.
ProcessSolution and if the syntax is faulty you'll get an error massage.
You can do a comprehansive check of the syntax and semantics of a derivation using GDV.
It's also available online in
SystemOnTSTP.
For more information about GDV, you can read ...
@Article{Sut06,
Author = "Sutcliffe, G.",
Year = "2006",
Title = "{Semantic Derivation Verification}",
Journal = "International Journal on Artificial Intelligence Tools",
Volume = "15",
Number = "6",
Pages = "1053-1070"
}
Once the syntax is OK, go back to SystemOnTSTP and choose IDV as the
System.
That'll render your derivation DAG and provide access to a lot
of postprocessing tools.