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
,
,
and
,
where
,
,
and B is a formula of the form
or
.
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
,
which has the same semantics as
,
but it plays a specific syntactical role, namely, formulae of the form
are blocked from being principal clauses. For the logics K4 and KD4, we introduce the connective
to simulate the connective
of S4, in the way such that
iff
.
For the logics K4 and KD4, the connective
has the same semantics as
,
but formulae of the form
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).