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

Logic Journal of the IGPL 21 (3):407-437 (2013)
  Copy   BIBTEX


We develop a conceptually clear, intuitive, and feasible decision procedure for testing satisfiability in the full multi\-agent epistemic logic \CMAELCD\ with operators for common and distributed knowledge for all coalitions of agents mentioned in the language. To that end, we introduce Hintikka structures for \CMAELCD\ 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 \CMAELCD\ and closes for every unsatisfiable input set of formulae.

Similar books and articles

First order common knowledge logics.Frank Wolter - 2000 - Studia Logica 65 (2):249-271.
Terminating tableau systems for hybrid logic with difference and converse.Mark Kaminski & Gert Smolka - 2009 - Journal of Logic, Language and Information 18 (4):437-464.
Distributed knowledge.Floris Roelofsen - 2007 - Journal of Applied Non-Classical Logics 17 (2):255-273.
Distributed morality in an information society.Luciano Floridi - 2013 - Science and Engineering Ethics 19 (3):727-743.


Added to PP

344 (#55,550)

6 months
111 (#32,166)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Valentin Goranko
Stockholm University

Citations of this work

Doxastic logic: a new approach.Daniel Rönnedal - 2018 - Journal of Applied Non-Classical Logics 28 (4):313-347.

Add more citations