TPTP Format for Derivations

What is a Derivation?

• A directed acyclic graph (DAG)
• Leaf nodes are formulae from the input
• Interior nodes are inferred formulae
• Root nodes are the final derived formulae
• Required: Input and inferred formulae; Parent references for inferred formulae
• Optional: Formulae roles; Inference rule + usage; Semantics

Specifying a TPTP Format Derivation

• Recall the TPTP language
• A list of annotated formulae
  • File source for leaf formulae
  • plain role for inferred formulae
  • Inference source for inferred formulae
• Inference source contains ...
  • Inference rule name
  • Parent annotated formulae names
  • SZS relationship with parents (often status(thm))
  • Other special information, e.g., new symbols, theories, splitting

Example

• A toy problem

  %------------------------------------------------------------------------ 
  %----All (hu)men are created equal. John is a human. John got an F grade. 
  %----There is someone (a human) who got an A grade. An A grade is not 
  %----equal to an F grade. Grades are not human. Therefore there is a 
  %----human other than John. 
  
  fof(all_created_equal,axiom,( 
      ! [H1,H2] : 
        ( ( human(H1) 
           & human(H2) ) 
       => created_equal(H1,H2) ) )). 
  
  fof(john,axiom,( 
      human(john) )). 
  
  fof(john_failed,axiom,( 
      grade(john) = f )). 
  
  fof(someone_got_an_a,axiom,( 
      ? [H] : 
        ( human(H) 
        & grade(H) = a ) )). 
  
  fof(distinct_grades,axiom,( 
      a != f )). 
  
  fof(grades_not_human,axiom,( 
      ! [G] : ~ human(grade(G)) )). 
  
  fof(someone_not_john,conjecture,( 
      ? [H] : 
        ( human(H) 
        & H != john ) )). 
  %-------------------------------------------------------------------- 
  

• A TPTP format refutation (by E)

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