Clausal Tableau Systems for Propositional Modal Logics

In the thesis, we propose so called clausal tableau systems for the propositional modal logics K, KD, T, KB, KDB, B, K4, KD4, and S4 (see Sections 2.5 and 3.1, and Tables 3.1, 3.2, and 3.3). Basing on these systems we give decision procedures for the logics with improved upper space bounds.

Our tableau systems are defined only for sets of basic clauses. If we use letters a and b to denote primitive propositions and their negations, then by a basic clause we mean a formula of one of the forms $\Box^s\lnot\Box a$, $\Box^s(a_1 \lor \ldots \lor a_k)$, and $\Box^s(a \lor B)$, where $s \geq 0$, $k \geq 1$, and B is a formula of the form $\Box b$ or $\lnot\Box b$. Given a formula, we can translate it to an equisatisfiable set of basic clauses to be usable by our systems (see Section 2.3).

Our formulation of tableau systems is based on the work of Hintikka [6], Rautenberg [11], Goré [5], and Hudelmaier [8]. For the logics K, KD, T, KB, KDB, and B, we introduce the connective $\blacksquare$, which has the same semantics as $\Box$, but it plays a specific syntactical role, namely, formulae of the form $\blacksquare^s\phi$ are blocked from being principal clauses. For the logics K4 and KD4, we introduce the connective $\boxdot$ to simulate the connective $\Box$ of S4, in the way such that $M,w \vDash\boxdot\phi$ iff $M,w \vDash(\Box\phi \land \phi)$. For the logics K4 and KD4, the connective $\blacksquare$ has the same semantics as $\boxdot$, but formulae of the form $\blacksquare^s\phi$ are blocked from being principal clauses.

Our tableau systems are sound and complete (see Theorems 3.4.9, 3.5.9, and 3.6.9), and have the finite tableau property (see Section 3.3).