Proofs of Equivalence in Modal Logic Systems

Geoff Sutcliffe
Department of Computer Science
University of Miami

and 

Daphne Simmonds
Mona Institute of Applied Science
University of the West Indies

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.