Proofs of Equivalence in
Modal Logic Systems

Modal Logic

• Syntax and Semantics
• Common Modal Logics
• Equivalence of Systems

Encoding for ATP

• FOL Encoding
• TPTP Encoding
• TPTP Encoded Modal Systems
• PC Based Systems
• S1⁰ Based Systems

Proving Equivalence

• What is Proved
• S5=KM4B and S5=KM5
• S5=S1-0M6S3M9B and S5=KM5

Conclusion