1 Department of Applied Mathematics and Computer Science, Technical University of Denmark2 Algorithms and Logic, Department of Applied Mathematics and Computer Science, Technical University of Denmark3 Roskilde Universitet4 Department of Informatics and Mathematical Modeling, Technical University of Denmark5 University of Witwaterstrand
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.
Interest Group in Pure and Applied Logics. Logic Journal, 2013, Vol 21, Issue 3, p. 407-437