TPTP Encoding

TPTP Syntax

• Improved syntax introduced in TPTP v3.0.0
• Annotated formulae as building blocks
  • Language
  • Name, type, and the logical formula
  • Optional source and user annotations

Definitional Appproach

• All formulae defined with <=>
• Allows easy reference to formulae
• Example:

  fof(axiom_K,axiom,
      ( axiom_K
    <=> ! [X,Y] : is_a_theorem(implies(necessarily(implies(X,Y)),
  implies(necessarily(X),necessarily(Y))))  )).