If ⊨ then ⊢

Lemma

• Define TPTP format from Domain & Mappings
• Extend Domain & Mappings to interpret TPTP format

• Domain & Extended mappings ⊢ TPTP format

Theorem

• If TPTP axiom ⊨ Problem formulae, then
  Domain & Extended mappings ⊢ Problem formulae
• Domain & Extended mappings ⊢ Problem formulae iff
  Domain & Mappings ⊢ Problem formulae

• If TPTP axiom ⊨ Problem formulae, then
  Domain & Mappings ⊢ Problem formulae