A tableau calculus for multimodal logics and some (Un)decidability results

Matteo Baldoni; Laura Giordano; Alberto Martelli

doi:10.1007/3-540-69778-0_13

A tableau calculus for multimodal logics and some (Un)decidability results

Matteo Baldoni
, Laura Giordano
, Alberto Martelli

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

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 [t₁].[t_n]'ℓ⊃ [s₁].[s _m]ℓ', called inclusion axioms, where the t_i's and s_j '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.

Original language	English
Title of host publication	Automated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1998, Proceedings
Publisher	Springer Verlag
Pages	44-59
Number of pages	16
ISBN (Print)	3540644067, 9783540644064
DOIs	https://doi.org/10.1007/3-540-69778-0_13
Publication status	Published - 1998
Externally published	Yes
Event	International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 1998 - Oisterwijk, Netherlands Duration: 5 May 1998 → 8 May 1998

Publication series

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

Conference

Conference	International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 1998
Country/Territory	Netherlands
City	Oisterwijk
Period	5/05/98 → 8/05/98

Keywords

Decidability
Formal grammars
Multimodal logics
Prefixed Tableaux methods

Access to Document

10.1007/3-540-69778-0_13

Cite this

Baldoni, M., Giordano, L., & Martelli, A. (1998). A tableau calculus for multimodal logics and some (Un)decidability results. In Automated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1998, Proceedings (pp. 44-59). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1397 LNAI). Springer Verlag. https://doi.org/10.1007/3-540-69778-0_13

Baldoni, Matteo ; Giordano, Laura ; Martelli, Alberto. / A tableau calculus for multimodal logics and some (Un)decidability results. Automated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1998, Proceedings. Springer Verlag, 1998. pp. 44-59 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{fb02c4932d554ed5864e482bf537655b,

title = "A tableau calculus for multimodal logics and some (Un)decidability results",

abstract = "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{\~n}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.",

keywords = "Decidability, Formal grammars, Multimodal logics, Prefixed Tableaux methods",

author = "Matteo Baldoni and Laura Giordano and Alberto Martelli",

year = "1998",

doi = "10.1007/3-540-69778-0\_13",

language = "English",

isbn = "3540644067",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "44--59",

booktitle = "Automated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1998, Proceedings",

address = "Germany",

note = "International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 1998 ; Conference date: 05-05-1998 Through 08-05-1998",

}

Baldoni, M, Giordano, L & Martelli, A 1998, A tableau calculus for multimodal logics and some (Un)decidability results. in Automated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1998, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1397 LNAI, Springer Verlag, pp. 44-59, International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 1998, Oisterwijk, Netherlands, 5/05/98. https://doi.org/10.1007/3-540-69778-0_13

A tableau calculus for multimodal logics and some (Un)decidability results. / Baldoni, Matteo; Giordano, Laura; Martelli, Alberto.
Automated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1998, Proceedings. Springer Verlag, 1998. p. 44-59 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1397 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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 - https://www.scopus.com/pages/publications/84886297088

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 -

Baldoni M, Giordano L, Martelli A. A tableau calculus for multimodal logics and some (Un)decidability results. In Automated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1998, Proceedings. Springer Verlag. 1998. p. 44-59. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-69778-0_13

A tableau calculus for multimodal logics and some (Un)decidability results

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this