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(someone_not_john,conjecture, ? [X3] : ( human(X3) & created_equal(X3,john) & X3 != john ), file('CreatedEqual.p',someone_not_john) ). fof(all_created_equal,axiom, ! [X1,X2] : ( ( human(X1) & human(X2) ) => created_equal(X1,X2) ), file('CreatedEqual.p',all_created_equal) ). fof(someone_got_an_a,axiom, ? [X3] : ( human(X3) & grade(X3) = a ), file('CreatedEqual.p',someone_got_an_a) ). fof(john,axiom, human(john), file('CreatedEqual.p',john) ). fof(distinct_grades,axiom, a != f, file('CreatedEqual.p',distinct_grades) ). fof(john_failed,axiom, grade(john) = f, file('CreatedEqual.p',john_failed) ). fof(c_0_6,negated_conjecture, ~ ? [X3] : ( human(X3) & created_equal(X3,john) & X3 != john ), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[someone_not_john])]) ). fof(c_0_7,plain, ! [X6,X7] : ( ~ human(X6) | ~ human(X7) | created_equal(X6,X7) ), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[all_created_equal])])]) ). fof(c_0_8,negated_conjecture, ! [X5] : ( ~ human(X5) | ~ created_equal(X5,john) | X5 = john ), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_6])])]) ). fof(c_0_9,plain, ( human(esk1_0) & grade(esk1_0) = a ), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[someone_got_an_a])]) ). cnf(c_0_10,plain, ( created_equal(X1,X2) | ~ human(X1) | ~ human(X2) ), inference(split_conjunct,[status(thm)],[c_0_7]) ). cnf(c_0_11,plain, human(john), inference(split_conjunct,[status(thm)],[john]) ). cnf(c_0_12,negated_conjecture, ( X1 = john | ~ human(X1) | ~ created_equal(X1,john) ), inference(split_conjunct,[status(thm)],[c_0_8]) ). cnf(c_0_13,plain, human(esk1_0), inference(split_conjunct,[status(thm)],[c_0_9]) ). cnf(c_0_14,plain, ( created_equal(X1,john) | ~ human(X1) ), inference(spm,[status(thm)],[c_0_10,c_0_11]) ). fof(c_0_15,plain, a != f, inference(fof_simplification,[status(thm)],[distinct_grades]) ). cnf(c_0_16,negated_conjecture, ( esk1_0 = john | ~ created_equal(esk1_0,john) ), inference(spm,[status(thm)],[c_0_12,c_0_13]) ). cnf(c_0_17,plain, created_equal(esk1_0,john), inference(spm,[status(thm)],[c_0_14,c_0_13]) ). fof(c_0_18,plain, a != f, inference(fof_nnf,[status(thm)],[c_0_15]) ). cnf(c_0_19,plain, grade(esk1_0) = a, inference(split_conjunct,[status(thm)],[c_0_9]) ). cnf(c_0_20,negated_conjecture, esk1_0 = john, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_16,c_0_17])]) ). cnf(c_0_21,plain, grade(john) = f, inference(split_conjunct,[status(thm)],[john_failed]) ). cnf(c_0_22,plain, a != f, inference(split_conjunct,[status(thm)],[c_0_18]) ). cnf(c_0_23,plain, $false, inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_19,c_0_20]),c_0_21]),c_0_22]), [proof] ). %------------------------------------------------------------------------------

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.