Journal Article

Tableau-based decision procedure for the multiagent epistemic logic with all coalitional operators for common and distributed knowledge

Mai Ajspur, Valentin Goranko and Dmitry Shkatov

in Logic Journal of the IGPL

Volume 21, issue 3, pages 407-437
Published in print June 2013 | ISSN: 1367-0751
Published online December 2012 | e-ISSN: 1368-9894 | DOI: http://dx.doi.org/10.1093/jigpal/jzs048
Tableau-based decision procedure for the multiagent epistemic logic with all coalitional operators for common and distributed knowledge

Show Summary Details

Preview

We develop a conceptually clear, intuitive and feasible decision procedure for testing satisfiability in the full multiagent epistemic logic CMAEL(CD) with operators for common and distributed knowledge for all coalitions of agents mentioned in the language. To that end, we introduce Hintikka structures for CMAEL(CD) and prove that satisfiability in such structures is equivalent to satisfiability in standard models. Using that result, we design an incremental tableau-building procedure that eventually constructs a satisfying Hintikka structure for every satisfiable input set of formulae of CMAEL(CD) and closes for every unsatisfiable input set of formulae.

Keywords: multi-agent epistemic logic; satisfiability; tableau; decision procedure

Journal Article.  0 words. 

Subjects: Logic

Full text: subscription required

How to subscribe Recommend to my Librarian

Users without a subscription are not able to see the full content. Please, subscribe or login to access all content.