Path calculus in the modal logic S4
- 23 Downloads
We describe the tableau and inverse calculi for the propositional modal logic S4. The formulas are treated as sets of paths. We obtain the upper bound for the number of applications of rules in the deduction tree.
Keywordsmodal logic S4 tableau method inverse method
Unable to display preview. Download preview PDF.
- 1.A. Degtyarev and A. Voronkov, The inverse method, Handbook of Automated Reasoning, Elsevier Science Publishers (2001).Google Scholar
- 2.G. Mints, V. Orevkov, and T. Tammet, Transfer of sequent calculus strategies to resolution for S4, Proof Theory and Modal Logic, Kluwer Academic Publishers (1996).Google Scholar
- 3.G. Mints, Gentzen-type systems and resolution rule. Part I, Lecture Notes in Comput. Sci., 417, 198–231 (1988).Google Scholar