Proofs of Equivalence in
Modal Logic Systems

Abstract

The equivalence of different axiomatizations of modal logics is well known and documented in the literature, e.g., S5 may be equivalently axiomatized by PC + necessitation + K (distribution) + M + 5, and by S10 + M6 + S3 + M9 + B. Many proofs of equivalence are available from books. Some proofs of equivalence have been done using automated theorem proving (ATP) systems. This seminar describes some early work in a project whose goal is to build an online database of equivalence proofs that have been found using ATP.

Acknowledgement: John Halleck of the University of Utah, and his Logic Structures WWW site, are significant sources of modal logic knowledge that is necessary for this work.