TPTP Format for Derivations

Introduction

A derivation is a directed acyclic graph (DAG) whose leaf nodes are formulae from the input, whose internal 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. Other useful information that might be recorded includes: the role of each formula; references from the leaf formulae to the corresponding problem formulae; 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 between inferred formulae and their parent formulae.

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 as a list of annotated formulae.

Language: The languages currently supported are thf, tff, fof, and cnf.
Name: The name is a word starting with a lower case letter, 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 leaves, conjecture for conjecture leaves, negated_conjecture for negated conjectures, or plain for inferred formulae. A full list of the possible roles is in the TPTP syntax.
Logical formulae: The logical formulae 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 records: A file() record contains the problem file name and the corresponding annotated formula name in the problem file. Example:
```
     fof(john,axiom,
         human(john),
         file('CreatedEqual.p',john) ).
```
Introduced records: An introduced() record contains the introduction rule name, a list of useful introduction information, and a list of any parent formulae. 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 like this.
- Tautologies that are introduced must be recorded like this.
- Theory axioms that are introduced and have to be accepted on faith, e.g., arithmetic axioms, must be recorded like this.
Inference records: An inference() record contains the inference rule name, a list of useful inference information, and a list of its parents. Parents can be annotated formula names or nested inference() records. 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 is used for most inference rules.
  - status(cth) when the negation of the inferred formula is a theorem (logical consequence) of its parents. This is 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 is used for, e.g., Skolemization steps.
- Special information about recognized types of inferences, e.g., Skolemization.
- Details of new symbols introduced in the inference, e.g., by Herbrandization, documented in a new_symbols() record. New symbols should follow the conventions for new symbol names.

Acceptable Derivations

The TPTP format has requirements for a derivation to deemed acceptable, e.g., for the CADE ATP System Competition (CASC). The requirements are expressed as "must" in the documentation below, and marked❗. Other features that are desirable are expressed as "should" in the documentation below.

Proofs should not use a TPTP language that is more expressive than that of the problem.
Proofs must be syntactically correct in TPTP format.❗ This is checked using the BNFParser and TPTP4X, available in SystemB4TPTP.
Proofs must be structurally correct:❗
1. Annotated formulae must be uniquely named.
2. Proofs must be acyclic.
3. Proofs must have formulae from the problem as leaves, and must end at the conjecture (for axiomatic proofs) or $false formulae (for proofs by contradiction, e.g., CNF refutations and closed tableaux).
4. If a problem file is provided then each leaf must have a file() record that specifies a problem file name (it might be different from that of the problem file provided) and the name of the corresponding formula in the problem file. The formula named in a file() record must exist with the same name in the problem file, and the leaf formula must be alpha-equivalent to the formula in the problem file.
5. Proofs must show only relevant inference steps, i.e., in the DAG from leaves to a root.
6. Inference steps must be documented in a correctly formed inference() record.
  - The TPTP World does not standardize inference rule names.
  - The useful information list must contain exactly one status() record.
  - The named parent annotated formulae must exist in the derivation.
7. Proofs that negate the conjecture must correctly annotate the step as status(cth), and have a single parent with the role conjecture.
8. Inference steps must aim to list exactly those parents that are used in the inference. Inference steps may list parents that are not necessary for the inference. For example, in the inference of p(a) from p(a) and a = a, the equality is not necessary but might be used in an (unnecessary) equality substitution step. In contrast, p(b) would probably not be used in that inference step. A genuine effort must be made to avoid listing unnecessary parents.
9. New symbols introduced in derivations, e.g., to provide definitions for complex terms and formulae, in Skolemization and Herbrandization, in splitting, etc. must be documented in a new_symbols() record. The first argument to the new_symbols() record gives a label for the new symbols, and the second argument is a []ed list of the new symbols. The new symbols must be unique and globally new, and should follow the conventions for new symbol names.
10. Proofs that make assumptions must propagate and eventually discharge the assumptions.
Proof structure is checked using GDV, available in SystemB4TSTP. To check only the structure of the derivation change GDV's "Command" to run_GDV %s 30 -d -u (i.e., add -d -u on the end).
Translations from one form to another, e.g., FOF to CNF, must be adequately documented.❗
Inference steps must be reasonably fine-grained. TO BE DECIDED.
Proofs should graft in subproofs from external systems.
Steps with particular requirements
1. Definitions that introduce a new symbol must be recorded like this.❗
2. Tautologies that are introduced must be recorded like this.❗
3. Theory axioms that are introduced and have to be accepted on faith, e.g., arithmetic axioms, must be recorded like this.❗
4. Each Skolemization step of one existentially quantified variable must be performed and recorded in a separate annotated formula like this.❗

Definitions

If a derivation defines a new symbol, the definition annotated formula must have the following form:

The annotated formula must have the definition role.

If the defined symbol has variables in its arguments, the formula must have a top level universal quantifier binding those variables. The scope of the universal quantifier must be the entire definition.

The definition must be either atomic with an equality predicate, or binary with an equality, equivalence, implication, or reverse implication connective.

The defined symbol must be on the left hand side of the equality/connective, either outermost or under a single negation.

The source must be an introduced() record, with the type definition.

The useful information of the introduced(definition,...) record must include a new_symbols(definition,...) record with the new symbol in the argument list.

The parents of the introduced() record can be anything.

See the conventions for new symbol names.

(In problems, definitions are axiom-like and do not need an introduced() record.)

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])],[])).

Tautologies

If a derivation introduces a tautology, the annotated formula must have the following form:

The annotated formula must have the axiom role.
The source must be an introduced() record, with the type tautology.
The useful information and parents of the introduced() record can be anything.

Examples

tff(soliloquy,axiom,
    ! [X: alive] :
      ( to_be(X) | ~ to_be(X) ),
    introduced(tautology,[that_is_the_question],[hamlet])).

Theory Axioms

If a derivation introduces a theory axiom that has to be accepted on faith, e.g., arithmetic axioms, the annotated formula must have the following form:

The annotated formula must have the axiom role.
The source must be an introduced() record, with the type theory.
The useful information and parents of the introduced() record can be anything.

Examples

tff(square_root_2,axiom,
    ~ ? [X: $rat] :
        $product(X,X) = 2,
    introduced(theory,[],[hippasus_of_metapontum])).

Skolemization

Each Skolemization step of one existentially quantified variable must be performed and recorded in a separate annotated formula. These requirements are for using Skolem symbols. The requirements for using ε-terms are given below.

Variables in the formula to be Skolemized must be uniquely (re)named.

The Skolem symbol must be new, regardless of arity. See the conventions for new symbol names.
The Skolem term must have all the universally quantified variables that are in scope as arguments, in outer-to-inner order.
The annotated formula must have the plain role.
The source must be an inference() record.
The useful information of the inference() record must include a status(esa) record.
The useful information of the inference() record must include a new_symbols(skolem,...) record with the new symbol in the argument list.
The useful information of the inference() record must include a skolemize() record with the existentially quantified variable and the replacement Skolem term as arguments.

Plain example, single steps:

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

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

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

"Hidden" existential quantification:
It is possible, but not nice, to do Skolemization steps with the existential quantification hidden, e.g., under a negated universal quantification.

fof(bride,plain,
    ! [Marriage] :
    ! [Parent] :
    ~ ! [Groom] :
        ~ ( in_love(Groom,sK0(Marriage))
         => give_hand_in_marriage(Parent,sK0(Marriage),Groom,Marriage) ) ).

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

Plain example, multiple steps:
It is possible, but not acceptable, to record multiple Skolemization steps in one annotated formula.

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

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

Using ε-terms:
For people who justify Skolemization with ε-terms. The requirements given above for Skolemization are the same for this case, except:

The ε-term must be defined in a definition before its use.
The useful information of the Skolemized formula's inference() record must not repeat the new_symbols(skolem,...) record ... that is in the definition's annotated formula.

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

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

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

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

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

New Symbol Names

These conventions provide guidelines for reasonable naming of such symbols, and specify 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 either 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 must be recorded in a new_symbols() record in the second argument of an inference() or introduced() record. The format is new_symbols(Type,[Symbols]). The Type indicates the type of new symbol, with possible values skolem, definition, and others. Symbols is a comma separated list of new symbols of that type. An inference() or introduced() record can have multiple new_symbols() records. 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 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"
}