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 might 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; the semantic relationships of inferred formulae with respect to their parents.

The TPTP format requires certain of these features to be acceptable (expressed as "must" in the documentation below), and other features are desirable to be nice (expressed as "should" in the documentation below) and highlighted with a ✅. ATP systems might usefully offer a flag to indicate whether just an acceptable derivation is required, or a nice derivation.

Specifying a TPTP Format Derivation

The top level building blocks of TPTP derivations are annotated formulae. An annotated formula has the form:

language(name,role,formula,source,useful info). A derivation is written in the TPTP language as a list of annotated formulae. Derivations should✅ show only inference steps that are relevant, i.e., in the DAG from leaves to a root.

Language: The languages currently supported are thf, tff, fof, and cnf. Proofs should not use a TPTP language that is more expressive than that of the problem.
Name: The name is a word starting lower case, e.g., original_f1, or a single quoted word, e.g., 'A crazy $ name', or a non-negative integer.
Role: The role is typically one of axiom for axiom leaves, definition for definition axiom leaves, conjecture for FOF conjecture leaves, negated_conjecture for negated conjectures, or plain for inferred formulae. A full list of the posssible roles is in the TPTP syntax.
Logical formula: The logical formula use the TPTP syntax.
Source: Each leaf formula has a file record or an introduced record, and each inferred formula has an inference record. Details below.
Useful information: The useful information is a []ed list of 'Prolog-like' terms.

The source and useful information are optional.

Sources:

File record: A file record contains the problem file name and the corresponding annotated formulae name in the problem file. Example:
```
     fof(john,axiom,
         human(john),
         file('CreatedEqual.p',john) ).
```
Introduced record: Example:
```
     fof(64,definition,
         ( sP1 <=> ! [X8] : ~ has_job(X8,boxer) ),
         introduced(definition,[new_symbols(definition,[sP1])],[])).
```
Definitions that introduce a new symbol must be recorded in this form of annotated formula. See the conventions for new symbol names.
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. Example:
```
     cnf(c_0_20,negated_conjecture,
         sK0 = john,
         inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_16,c_0_17])]) ).
```
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. The most common ones are:
  - status(thm) when the inferred formula is a theorem (logical consequence) of its parents. This used for most inference rules.
  - status(cth) when the negation of the inferred formula is a theorem (logical consequence) of its parents. This used for, e.g., the step negating the conjecture for a proof by refutation.
  - status(esa) when the inferred formula is equisatisfiable with its single parent. This used for, e.g., Skolemization steps.
- Special information about recognized types of inferences, e.g., Skolemization.
- Details of new symbols introduced in the inference, following the conventions for new symbol names.

Definitions

Definitions that introduce new symbols must the following form:

The annotated formula must have the definition role.
The formula must be binary, with an equality, equivalence, implication, or reverse implication connective.
The defined symbol must be on the left hand side of the connective, possibly under a negation.
Variable arguments of the new symbol must be universally quantified.
The source must be an introduced() record.
The type of introduction can be anything, but definition is conventional.
The useful information must include a new_symbols() record with definition as its type, and the new symbol in the seconf argument list.
The parents of the introduction can be anything.

Examples

tff(square,definition,
    ! [I: $int] :
      ( square(I) = $product(I,I) ),
    introduced(definition,[new_symbols(definition,[square])],[])).

fof(pugalist,definition,
    ( no_fighters <=> ! [X] : ~ has_job(X,boxer) ),
    introduced(definition,[new_symbols(definition,[no_fighters])],[])).

tff(bad_cat,definition,
    ! [C: cat] :
      ( ~ friendly(C) <=> ( horrible(C) & bad_pet(C) ) ),
    introduced(definition,[new_symbols(definition,[friendly])],[])).

Skolemization

Optimally, each Skolemization step of one existentially quantified variable should be performed and recorded in separate annotated formulae. However, it is possible to record multiple Skolemization steps in one annotated formula. So far three variants have emerged, each of which has particular output requirements.

Variables in the formula to be Skolemized must be uniquely (re)named.
Skolem symbols must be new, regardless of arity
New Skolem symbols must be recorded in a new_symbols() record, in the annotated formula where the new symbols first appear in the logical formula.
The existentially quantified variables and the replacement Skolem terms must be recorded in skolemize() records, in the annotated formula where the existentially quantified variables are replaced.
If ε-terms are used:
- ε-terms must be defined before their use.
If choice axioms are used:
- The axioms should be given after the Skolemization steps where the Skolem symbols have been recorded in new_symbols() records.
- The annotated formula should have the axiom role.
- The annotated formulae must record the introduction of the axioms with introduced(choice_axiom,[],[]) records.
- In the parents list of the inference record of the Skolemized formula, please list the choice axioms before the real parent formula (because GDV needs an upgrade :-).

Plain example, single steps:

%----Starting formula
fof(marriage,plain,
    ! [Marriage] :
    ? [Bride] :
    ? [Groom] :
      in_love(Groom,Bride) ).

%----Skolemize Bride
fof(bride,plain,
    ! [Marriage] :
    ? [Groom] :
      in_love(Groom,sK0(Marriage)),
    inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(Bride,sK0(Marriage))],[marriage]) ).

%----Skolemize Groom
fof(groom,plain,
    ! [Marriage] :
      in_love(sK1(Marriage),sK0(Marriage)),
    inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(Groom,sK1(Marriage))],[bride]) ).

Plain example, multiple steps:

%----Starting formula
fof(marriage,plain,
    ! [Marriage] :
    ? [Bride] :
    ? [Groom] :
      in_love(Groom,Bride) ).

%----Skolemize Bride and Groom
fof(groom,plain,
    ! [Marriage] :
      in_love(sK1(Marriage),sK0(Marriage)),
    inference(skolemize,[status(esa),new_symbols(skolem,[sk0,sK1]),skolemize(Bride,sK0(Marriage)),skolemize(Groom,sK1(Marriage))],[marriage]) ).

ε-term example:
For people who justify Skolemization with an ε-term.

%----Starting formula
fof(marriage,plain,
    ! [Marriage] :
    ? [Bride] :
    ? [Groom] :
      in_love(Groom,Bride) ).

%----New symbol sK0 recorded here in the definition of the ε term. Default typing with $i.
tff(sK0_defn,definition,
    ! [Marriage] :
      ( sK0(Marriage)
      = ( # [Bride] :
          ? [Groom] : in_love(Groom,Bride) ) ),
    introduced(definition,[new_symbols(skolem,[sK0])],[marriage]) ).

%----Skolemize Bride
fof(bride,plain,
    ! [Marriage] :
    ? [Groom] :
      in_love(Groom,sK0(Marriage)),
    inference(skolemize,[status(esa),skolemize(Bride,sK0(Marriage))],[marriage,sK0_defn]) ).

tff(sK1_defn,definition,
    ! [Marriage: $i] :
      ( sK1(Marriage)
      = ( # [Groom: $i] : in_love(Groom,sK1(Marriage)) ) ),
    introduced(definition,[new_symbols(skolem,[sK1])],[bride]) ).

%----Skolemize Groom
fof(groom,plain,
    ! [Marriage] :
      in_love(sK1(Marriage),sK0(Marriage)),
    inference(skolemize,[status(esa),skolemize(Groom,sK1(Marriage))],[bride,sK1_defn]) ).

Choice axiom example:
For people who believe that its just fine to output a "choice axiom" to justify a Skolemization step.

%----Starting formula
fof(marriage,plain,
    ! [Marriage] :
    ? [Bride] :
    ? [Groom] :
      in_love(Groom,Bride) ).

%----Skolemize Bride
fof(bride,plain,
    ! [Marriage] :
    ? [Groom] :
      in_love(Groom,sK0(Marriage)),
    inference(skolemize,[status(thm),new_symbols(skolem,[sK0]),skolemize(Bride,sK0(Marriage))],[gift_of_choice_sK0,marriage]) ).

%----Choice axiom
fof(gift_of_choice_sK0,axiom,
    ( ! [Marriage] :
      ? [Bride] :
      ? [Groom] :
        in_love(Groom,Bride)
   => ! [Marriage] :
      ? [Groom] :
        in_love(Groom,sK0(Marriage)) ),
    introduced(choice_axiom,[],[]) ).

%----Skolemize Groom
fof(groom,plain,
    ! [Marriage] :
      in_love(sK1(Marriage),sK0(Marriage)),
    inference(skolemize,[status(thm),new_symbols(skolem,[sK1]),skolemize(Groom,sK1(Marriage))],[bride,gift_of_choice_sk1]) ).

fof(gift_of_choice_sk1,axiom,
    ( ! [Marriage] :
      ? [Groom] :
        in_love(Groom,sK0(Marriage))
   => ! [Marriage] :
        in_love(sK1(Marriage),sK0(Marriage)) ),
    introduced(choice_axiom,[],[]) ).

New Symbol Names

New symbols may be introduced in derivations, e.g., to provide definitions for complex terms and formulae, in Skolemization and Herbrandization, in splitting. These conventions provide guidelines for reasonable naming of such symbols, and spefiy how the new symbols must be introduced in inference() and introduced() records.

New non-variable symbol names are recommended to be of the form sKN, where K is an uppercase letter indicating the type of new symbol, and N is a non-negative integer used to make the basic symbol name unique.

The conventions for K are
- K for Skolems
- F for defined functions
- G for function symbols with other uses
- P for defined predicates
- Q for predicate symbols with other uses, e.g., for splitting
The index N should be global across all symbol types, or local to each symbol type.
Examples: sK1, sF99, sP127.

New symbol names can optionally be extended by an underscore then one or more alphanumeric and underscore characters. For examples, sK1_iProver, sF99_Splitting, sP127_3, SV99_ForallIntro. The names should remain unique without the extension, using the N suffix.

The introduction of new non-variable symbols should be recorded in a <new_symbol_record> in the <useful_info> field of the <inference_record> of a derived formula, or in the <optional_info> field of the <internal_source> of an introduced formula. The new form will have the format new_symbols(Type,[Symbols]). The Type indicates the type of new symbol, with possible values skolem, definition, other. Symbols is a comma separated list of new symbols of that type. The <useful_info> field can have multiple new_symbols() terms. For examples:
```
fof(bride,plain,
    ! [Marriage] :
    ? [Groom] :
      in_love(Groom,sK0(Marriage)),
    inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(Bride,sK0(Marriage))],[marriage]) ).
    
fof(pugalist,definition,
    ( no_fighters <=> ! [X] : ~ has_job(X,boxer) ),
    introduced(definition,[new_symbols(definition,[no_fighters])],[])). 
```
ATP systems should check for clashes whenever they generate a new symbol, and whenever they read input after any new symbols have been generated.

If you are interested in the history and motivations behind this convention, read the source of this web page.

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 E):

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

%----If E believed in epsilon terms ...
% tff(sK0_defn,definition,
%     ( sK0
%     = ( # [X3: $i] :
%           ( human(X3)
%           & ( grade(X3) = a ) ) ) ),
%     introduced(definition,[new_symbols(skolem,[sK0])],[someone_got_an_a]) ).

fof(c_0_9,plain,
    ( human(sK0)
    & grade(sK0) = a ),
    inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X3,sK0)],[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(sK0),
    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,
    ( sK0 = john
    | ~ created_equal(sK0,john) ),
    inference(spm,[status(thm)],[c_0_12,c_0_13]) ).

cnf(c_0_17,plain,
    created_equal(sK0,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(sK0) = a,
    inference(split_conjunct,[status(thm)],[c_0_9]) ).

cnf(c_0_20,negated_conjecture,
    sK0 = 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

To check the syntax of a derivation you can run it through tptp4X, available 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". Click "ProcessSolution". If the syntax is faulty you'll get an error massage.

You can download and install TPTP4X on your own Linux computer, from Github. You must get the JJParser submodule too, i.e.,
git clone --recurse-submodules https://github.com/TPTPWorld/TPTP4X.

You can verify a derivation using GDV, also available in SystemOnTSTP. Select the "TSTP formulae" option and paste the formulae into the text box. Select "GDV" as the system, and ensure that the "Output mode" is "System". Click "ProcessSolution". It might take a while for output to appear. If the derivation is dubious or faulty, you'll get an WARNING/ERROR messages.

You can download and install GDV on your own Linux computer, from Github. You must get the JJParser submodule too, i.e.,
git clone --recurse-submodules https://github.com/TPTPWorld/GDV.git.

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"
}