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

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

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.