equal
deleted
inserted
replaced
1 <HTML><HEAD><TITLE>Modal/ReadMe</TITLE></HEAD><BODY> |
|
2 |
|
3 <H2>Modal: First-Order Modal Sequent Calculus</H2> |
|
4 |
|
5 This directory contains the Standard ML sources of the Isabelle system for |
|
6 Modal Logic. Important files include |
|
7 |
|
8 <DL> |
|
9 <DT>ROOT.ML |
|
10 <DD>loads all source files. Enter an ML image containing LK |
|
11 Isabelle and type: use "ROOT.ML";<P> |
|
12 |
|
13 <DT>ex |
|
14 <DD>subdirectory containing examples. Files Tthms.ML, S4thms.ML and |
|
15 S43thms.ML contain the theorems of Modal Logics, so arranged since |
|
16 T<S4<S43. To execute them, enter an ML image containing Modal |
|
17 and type: use "ex/ROOT.ML"; |
|
18 </DL> |
|
19 |
|
20 Thanks to Rajeev Gore' for supplying the inference system for S43.<P> |
|
21 |
|
22 Useful references on Modal Logics: |
|
23 |
|
24 <UL> |
|
25 <LI>Melvin C Fitting,<BR> |
|
26 Proof Methods for Modal and Intuitionistic Logics (Reidel, 1983) |
|
27 <LI>Lincoln A. Wallen,<BR> |
|
28 Automated Deduction in Nonclassical Logics (MIT Press, 1990) |
|
29 </UL> |
|
30 </BODY></HTML> |
|