Implication Checker for Modal Logic systems with Finite Modalities

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.

Go to ...

This page is
© Copyright 2000 by John Halleck, All Rights Reserved.
This page was last modified on January 22nd, 2000.