<HTML><HEAD><TITLE>Modal/ReadMe</TITLE></HEAD><BODY>
<H2>Modal: First-Order Modal Sequent Calculus</H2>
This directory contains the Standard ML sources of the Isabelle system for
Modal Logic. Important files include
<DL>
<DT>ROOT.ML
<DD>loads all source files. Enter an ML image containing LK
Isabelle and type: use "ROOT.ML";<P>
<DT>ex
<DD>subdirectory containing examples. Files Tthms.ML, S4thms.ML and
S43thms.ML contain the theorems of Modal Logics, so arranged since
T<S4<S43. To execute them, enter an ML image containing Modal
and type: use "ex/ROOT.ML";
</DL>
Thanks to Rajeev Gore' for supplying the inference system for S43.<P>
Useful references on Modal Logics:
<UL>
<LI>Melvin C Fitting,<BR>
Proof Methods for Modal and Intuitionistic Logics (Reidel, 1983)
<LI>Lincoln A. Wallen,<BR>
Automated Deduction in Nonclassical Logics (MIT Press, 1990)
</UL>
</BODY></HTML>