TY - GEN
T1 - A tableau calculus for multimodal logics and some (Un)decidability results
AU - Baldoni, Matteo
AU - Giordano, Laura
AU - Martelli, Alberto
PY - 1998
Y1 - 1998
N2 - In this paper we present a prefixed analytic tableau calculus for a class of normal multimodal logics and we present some results about decidability and undecidability of this class. The class is characterized by axioms of the form [t1].[tn]'ℓ⊃ [s1].[s m]ℓ', called inclusion axioms, where the ti's and sj 's are constants. This class of logics, called grammar logics, was introduced for the first time by Fariñas del Cerro and Penttonen to simulate the behaviour of grammars in modal logics, and includes some well-known modal systems. The prefixed tableau method is used to prove the undecidability of modal systems based on unrestricted, context sensitive, and context free grammars. Moreover, we show that the class of modal logics, based on right-regular grammars, are decidable by means of the filtration methods, by defining an extension of the Fischer-Ladner closure.
AB - In this paper we present a prefixed analytic tableau calculus for a class of normal multimodal logics and we present some results about decidability and undecidability of this class. The class is characterized by axioms of the form [t1].[tn]'ℓ⊃ [s1].[s m]ℓ', called inclusion axioms, where the ti's and sj 's are constants. This class of logics, called grammar logics, was introduced for the first time by Fariñas del Cerro and Penttonen to simulate the behaviour of grammars in modal logics, and includes some well-known modal systems. The prefixed tableau method is used to prove the undecidability of modal systems based on unrestricted, context sensitive, and context free grammars. Moreover, we show that the class of modal logics, based on right-regular grammars, are decidable by means of the filtration methods, by defining an extension of the Fischer-Ladner closure.
KW - Decidability
KW - Formal grammars
KW - Multimodal logics
KW - Prefixed Tableaux methods
UR - http://www.scopus.com/inward/record.url?scp=84886297088&partnerID=8YFLogxK
U2 - 10.1007/3-540-69778-0_13
DO - 10.1007/3-540-69778-0_13
M3 - Conference contribution
AN - SCOPUS:84886297088
SN - 3540644067
SN - 9783540644064
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 44
EP - 59
BT - Automated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1998, Proceedings
PB - Springer Verlag
T2 - International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 1998
Y2 - 5 May 1998 through 8 May 1998
ER -