Tableau-based procedure for deciding satisfiability in the full coalitional multiagent epistemic logic

TL;DR

This paper introduces a tableau-based decision procedure for the multiagent epistemic logic CMAELCD, enabling effective satisfiability testing by leveraging Hintikka structures and their equivalence to standard models.

Contribution

It presents a novel tableau-based method for deciding satisfiability in CMAELCD, utilizing Hintikka structures to bridge to standard models.

Findings

Satisfiability in Hintikka structures is equivalent to standard models.

The proposed tableau procedure is incremental and effective for CMAELCD.

The method advances decision procedures for complex multiagent epistemic logics.

Abstract

We study the multiagent epistemic logic CMAELCD with operators for common and distributed knowledge for all coalitions of agents. We introduce Hintikka structures for this logic and prove that satisfiability in such structures is equivalent to satisfiability in standard models. Using this result, we design an incremental tableau based decision procedure for testing satisfiability in CMAELCD.