From Simplified Kripke-Style Semantics to Simplified Analytic Tableaux for Some Normal Modal Logics

摘要

Modal logics K45, KB4, KD45 and S5 are of particular interest in knowledge representation, especially in the context of knowledge and belief modelling. Pietruszczak showed that these logics are curious for another reason, namely for the fact that their Kripke-style semantics can be simplified. A simplified frame has the form (W, A), where A C W. A reachability relation R may be defined as R = W × A, which, however, makes it superfluous to explicitly refer to it. It is well-known that S5 is determined by Kripke frames with R = W × W, i.e., A = W. Pietruszczak showed what classes of simplified frames determine K45, KD45, and KB4. These results were generalized to the extensions of these logics by Segerberg's formulas. In this paper, we devise sound, complete and terminating prefixed tableau algorithms based on simplified semantics for these logics. Since no separate rules are needed to handle the reachability relation and prefixes do not store any extra information, the calculi are accessible and conceptually simple and the process of countermodel-construction out of an open tableau branch is straightforward. Moreover, we obtain a nice explanation of why these logics are computationally easier than most modal logics, in particular NP-complete.