# 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
S1^{0} + 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.*