TY - GEN

T1 - Strongly analytic tableaux for normal modal logics

AU - Massacci, F.

PY - 1994

Y1 - 1994

N2 - © 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.

AB - © 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.

U2 - 10.1007/3-540-58156-1_52

DO - 10.1007/3-540-58156-1_52

M3 - Conference contribution

SN - 9783540581567

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 723

EP - 737

BT - Automated Deduction — CADE-12 - 12th International Conference on Automated Deduction, Proceedings

A2 - Bundy, A.

PB - Springer Verlag

T2 - 12th International Conference on Automated Deduction, CADE-12 1994

Y2 - 26 June 1994 through 1 July 1994

ER -