TPTP Encoded Modal Systems

Definitional Appproach

• Files with all formula definitions
  • PCAxiomDefns.ax
  • ModalAxiomDefns.ax
  • ModalRuleDefns.ax
  • OperatorDefns.ax
• Files for basic systems
  • Use (selective) include directives
  • K.sys
  • S1-0.sys
• Files for modal systems
  • M.sys
  • S5=KM4B.sys
  • etc
• Check the modal systems files for consistency ... Mace4 succeeds

Proving Equivalence

• Example: S5=KM5_to_S5=KM4B.p