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.