Strongly analytic tableaux for normal modal logics

Abstract

A strong analytic tableau calculus is presentend for the most common normal modal logics. The method combines the advantages of both sequent-like tableaux and prefixed tableaux. Proper rules are used, instead of complex closure operations for the accessibility relation, while non determinism and cut rules, used by sequent-like tableaux, are totally eliminated. A strong completeness theorem without cut is also given for symmetric and euclidean logics. The system gains the same modularity of Hilbert-style formulations, where the addition or deletion of rules is the way to change logic. Since each rule has to consider only adjacent possible worlds, the calculus also gains efficiency. Moreover, the rules satisfy the strong Church Rosser property and can thus be fully parallelized. Termination properties and a general algorithm are devised. The propo- sitional modal logics thus treated are K, D, T, KB, K4, K5, K45, KDB, D4, KD5, KD45, B, S4, S5, OM, OB, OK4, OS4, OM+, OB+, OK4+, OS4+. Other logics can be constructed with different combinations of the proposed rules, but are not presented here.