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

Mai Ajspur, Valentin Goranko, Dmitry Shkatov

Research output: Contribution to journalJournal articleResearchpeer-review

Abstract

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.
Original languageEnglish
JournalLogic Journal of the IGPL
Volume21
Issue number3
Pages (from-to)407-437
ISSN1367-0751
DOIs
Publication statusPublished - 2013

Keywords

  • Multi-agent epistemic logic
  • Satisfiability
  • Tableau
  • Decision procedure

Fingerprint Dive into the research topics of 'Tableau-based decision procedure for the multiagent epistemic logic with all coalitional operators for common and distributed knowledge'. Together they form a unique fingerprint.

Cite this