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.

The source and useful information are optional. The languages currently supported are

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)`.

- Explicit splitting, as done by SPASS:
The keyword is
- Details of new symbols introduced in the inference.

- The semantic relationship of the formula to its parents as an
SZS ontology value in a

- Useful information:
The useful information in a
`[]`ed list of 'Prolog-like' terms.

%-------------------------------------------------------------------- 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])). %--------------------------------------------------------------------

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.