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 -