Strongly analytic tableaux for normal modal logics

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review


© Springer-Verlag Berlin Heidelberg 1994.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.
Original languageEnglish
Title of host publicationAutomated Deduction — CADE-12 - 12th International Conference on Automated Deduction, Proceedings
EditorsA. Bundy
PublisherSpringer Verlag
ISBN (Print)9783540581567
Publication statusPublished - 1994
Externally publishedYes
Event12th International Conference on Automated Deduction, CADE-12 1994 - Nancy, France
Duration: 26 Jun 19941 Jul 1994

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference12th International Conference on Automated Deduction, CADE-12 1994


Dive into the research topics of 'Strongly analytic tableaux for normal modal logics'. Together they form a unique fingerprint.

Cite this