Analytic cut-free tableaux for regular modal logics of agent beliefs

Rajeev Goré; Linh Anh Nguyen

doi:10.1007/978-3-540-88833-8_15

Analytic cut-free tableaux for regular modal logics of agent beliefs

Rajeev Goré^*, Linh Anh Nguyen

^*Corresponding author for this work

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

6 Citations (Scopus)

Abstract

We present a sound and complete tableau calculus for a class of extended regular modal logics which contains useful epistemic logics for reasoning about agent beliefs. Our calculus is cut-free and has the analytic superformula property so it gives a decision procedure. Applying sound global caching to the calculus, we obtain the first optimal (EXPTime) tableau decision procedure for . We demonstrate the usefulness of logics and our tableau calculus using the wise men puzzle and its modified version, which requires axiom (5) for single agents.

Original language	English
Title of host publication	Computational Logic in Multi-Agent Systems - 8th International Workshop, CLIMA VIII, Revised Selected and Invited Papers
Publisher	Springer Verlag
Pages	268-287
Number of pages	20
ISBN (Print)	3540888322, 9783540888321
DOIs	https://doi.org/10.1007/978-3-540-88833-8_15
Publication status	Published - 2008
Event	8th International Workshop on Computational Logic in Multi-Agent Systems, CLIMA VIII - Porto, Portugal Duration: 10 Sept 2007 → 11 Sept 2007

Publication series

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

Conference

Conference	8th International Workshop on Computational Logic in Multi-Agent Systems, CLIMA VIII
Country/Territory	Portugal
City	Porto
Period	10/09/07 → 11/09/07

Access to Document

10.1007/978-3-540-88833-8_15

Cite this

Goré, R., & Nguyen, L. A. (2008). Analytic cut-free tableaux for regular modal logics of agent beliefs. In Computational Logic in Multi-Agent Systems - 8th International Workshop, CLIMA VIII, Revised Selected and Invited Papers (pp. 268-287). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5056 LNAI). Springer Verlag. https://doi.org/10.1007/978-3-540-88833-8_15

Goré, Rajeev ; Nguyen, Linh Anh. / Analytic cut-free tableaux for regular modal logics of agent beliefs. Computational Logic in Multi-Agent Systems - 8th International Workshop, CLIMA VIII, Revised Selected and Invited Papers. Springer Verlag, 2008. pp. 268-287 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{f73bcb923174458f98a9281b55f6e47d,

title = "Analytic cut-free tableaux for regular modal logics of agent beliefs",

abstract = "We present a sound and complete tableau calculus for a class of extended regular modal logics which contains useful epistemic logics for reasoning about agent beliefs. Our calculus is cut-free and has the analytic superformula property so it gives a decision procedure. Applying sound global caching to the calculus, we obtain the first optimal (EXPTime) tableau decision procedure for . We demonstrate the usefulness of logics and our tableau calculus using the wise men puzzle and its modified version, which requires axiom (5) for single agents.",

author = "Rajeev Gor{\'e} and Nguyen, {Linh Anh}",

year = "2008",

doi = "10.1007/978-3-540-88833-8_15",

language = "English",

isbn = "3540888322",

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

publisher = "Springer Verlag",

pages = "268--287",

booktitle = "Computational Logic in Multi-Agent Systems - 8th International Workshop, CLIMA VIII, Revised Selected and Invited Papers",

address = "Germany",

note = "8th International Workshop on Computational Logic in Multi-Agent Systems, CLIMA VIII ; Conference date: 10-09-2007 Through 11-09-2007",

}

Goré, R & Nguyen, LA 2008, Analytic cut-free tableaux for regular modal logics of agent beliefs. in Computational Logic in Multi-Agent Systems - 8th International Workshop, CLIMA VIII, Revised Selected and Invited Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5056 LNAI, Springer Verlag, pp. 268-287, 8th International Workshop on Computational Logic in Multi-Agent Systems, CLIMA VIII, Porto, Portugal, 10/09/07. https://doi.org/10.1007/978-3-540-88833-8_15

Analytic cut-free tableaux for regular modal logics of agent beliefs. / Goré, Rajeev; Nguyen, Linh Anh.
Computational Logic in Multi-Agent Systems - 8th International Workshop, CLIMA VIII, Revised Selected and Invited Papers. Springer Verlag, 2008. p. 268-287 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5056 LNAI).

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

TY - GEN

T1 - Analytic cut-free tableaux for regular modal logics of agent beliefs

AU - Goré, Rajeev

AU - Nguyen, Linh Anh

PY - 2008

Y1 - 2008

N2 - We present a sound and complete tableau calculus for a class of extended regular modal logics which contains useful epistemic logics for reasoning about agent beliefs. Our calculus is cut-free and has the analytic superformula property so it gives a decision procedure. Applying sound global caching to the calculus, we obtain the first optimal (EXPTime) tableau decision procedure for . We demonstrate the usefulness of logics and our tableau calculus using the wise men puzzle and its modified version, which requires axiom (5) for single agents.

AB - We present a sound and complete tableau calculus for a class of extended regular modal logics which contains useful epistemic logics for reasoning about agent beliefs. Our calculus is cut-free and has the analytic superformula property so it gives a decision procedure. Applying sound global caching to the calculus, we obtain the first optimal (EXPTime) tableau decision procedure for . We demonstrate the usefulness of logics and our tableau calculus using the wise men puzzle and its modified version, which requires axiom (5) for single agents.

UR - http://www.scopus.com/inward/record.url?scp=56749159036&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-88833-8_15

DO - 10.1007/978-3-540-88833-8_15

M3 - Conference contribution

SN - 3540888322

SN - 9783540888321

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

SP - 268

EP - 287

BT - Computational Logic in Multi-Agent Systems - 8th International Workshop, CLIMA VIII, Revised Selected and Invited Papers

PB - Springer Verlag

T2 - 8th International Workshop on Computational Logic in Multi-Agent Systems, CLIMA VIII

Y2 - 10 September 2007 through 11 September 2007

ER -

Goré R, Nguyen LA. Analytic cut-free tableaux for regular modal logics of agent beliefs. In Computational Logic in Multi-Agent Systems - 8th International Workshop, CLIMA VIII, Revised Selected and Invited Papers. Springer Verlag. 2008. p. 268-287. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-540-88833-8_15

Analytic cut-free tableaux for regular modal logics of agent beliefs

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this