The aim of this paper is to explain our new results relating modal propositional logic and rewrite rule systems. More precisely, we give complete term rewriting systems for the modal propositional systems known as K,Q,T and S5. These systems are presented as extensions of Hsiang's system for classical propositional calculus [7]. We have checked local confluence with the rewrite rule system K.B. developped by the Formel project at INRIA[2,4]. We prove that these systems are noetherian, and then infer their confluence from Newman's lemma. Therefore each term rewriting system provides a new automated decision procedure and defines a canonical form for the corresponding logic. We also show how to characterize the canonical forms thus obtained.
CITATION STYLE
Foret, A. (1988). Rewrite rule systems for modal propositional logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 343 LNCS, pp. 147–156). Springer Verlag. https://doi.org/10.1007/3-540-50667-5_66
Mendeley helps you to discover research relevant for your work.