I was recently trying to deal with extensions of the modal logic system S3, and finding I'm not very good at it.
So, I wrote a tool. It allows you to investigate extensions of systems with finite affirmative modalities that equivalence pairs of modalities of the parent system.
It takes in implications of the form Ap => Bp, where A and B are strings of modalities, with L being Necessity, and M being Possibility. It assumes that the underlying system has Lp == ~M~p, and double negation, modus ponens, and modus tollens.
checkmodal is written in perl.
One also needs some canned systems to get started.
This page is http://www.cc.utah.edu/~nahaj/logic/checkmodal © Copyright 2000 by John Halleck, All Rights Reserved. This page was last modified on January 22nd, 2000.