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

TL;DR

This paper presents a tableau-based decision procedure for the full multi-agent epistemic logic CMAEL(CD), enabling efficient satisfiability testing for formulas involving all coalitional operators for common and distributed knowledge.

Contribution

It introduces Hintikka structures for CMAEL(CD) and proves their equivalence to standard models, leading to a feasible tableau-based satisfiability testing method.

Findings

Developed a tableau-building procedure for CMAEL(CD)

Proved equivalence of Hintikka structures to standard models

Ensured the procedure terminates for satisfiable and unsatisfiable sets

Abstract

We develop a conceptually clear, intuitive, and feasible decision procedure for testing satisfiability in the full multi-agent 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.