Epistemic Logic Tableau Solver

This tool checks whether a formula of CMAEL(CD) is satisfiable: that is, whether there exists a Kripke model and a state where the formula is true. CMAEL(CD) extends standard multiagent epistemic logic with operators for common knowledge (

\mathbf{C}_A \varphi

— every agent in coalition

A

knows

\varphi

, and everyone knows that everyone knows it, ad infinitum) and distributed knowledge (

\mathbf{D}_A \varphi

—

\varphi

follows from the combined knowledge of all agents in

A

Based on Ajspur, Goranko & Shkatov (2012)

Formula

Restricted cuts (C1/C2) Solving...

Examples

Syntax Reference

p — atomic proposition

~p —

\neg p

(p & q) —

(p \wedge q)

(p | q) —

(p \vee q)

(p -> q) —

(p \to q)

Ka p —

\mathbf{K}_a\, p

(agent a knows p)

K{a,b} p —

(\mathbf{K}_a\, p \wedge \mathbf{K}_b\, p)

(a and b knows)

D{a,b} p —

\mathbf{D}_{\{a,b\}}\, p

(distributed knowledge)

C{a,b} p —

\mathbf{C}_{\{a,b\}}\, p

(common knowledge)

⋮

Results will appear here

Enter a formula on the left and click Check Satisfiability, or try one of the examples.

Tableau Details

Rendering graph...

Click to expand

How It Works

The Algorithm

The algorithm is a tableau-based decision procedure that works in three phases:

Construction (Pretableau)
Starting from the input formula, the algorithm builds a graph of prestates and states. A prestate is a set of formulas waiting to be expanded. Each prestate is expanded into one or more fully expanded, downward saturated states by applying logical decomposition rules (splitting conjunctions, branching on disjunctions, and handling modal operators). For each diamond formula (

\neg \mathbf{D}_A \varphi

) in a state, a new prestate is created as a successor, ensuring the model has the required transitions. The process continues until no new prestates or states need to be created. This builds the pretableau.

Prestate Elimination
Prestates served as intermediate construction artifacts. In this phase, every prestate is removed and edges are rewired: if state s pointed to prestate p, and p expanded to state t, then s now points directly to t. This produces the initial tableau: a graph consisting only of states and direct transition edges.

State Elimination
The algorithm iteratively removes “defective” states. Two types of defects are checked in a dovetailed loop:

E1: If a state contains a diamond formula but has no matching successor, it is eliminated.
E2: Eventualities (arising from negated common knowledge formulas like $\neg \mathbf{C}_A \varphi$ ) must be realized: there must be a finite path of accessible states witnessing the eventuality. States where an eventuality cannot be realized are eliminated.

This loop continues until no more states can be removed, yielding the final tableau.

The input formula is satisfiable if and only if the final tableau still contains a state that includes the input formula. The tool also supports restricted cut conditions (C1/C2), an optimization from the paper that dramatically reduces the number of states explored (e.g., from 113 to 30 states in Example 5) without affecting correctness.

Operators at a glance

Operator	Syntax	Meaning
$\mathbf{K}_a \varphi$	`Ka p`	Agent a knows $\varphi$
$\bigwedge_{a \in A} \mathbf{K}_a \varphi$	`K{a,b} p`	Every agent in $A$ individually knows $\varphi$
$\mathbf{D}_A \varphi$	`D{a,b} p`	It is distributed knowledge among $A$ that $\varphi$
$\mathbf{C}_A \varphi$	`C{a,b} p`	It is common knowledge among $A$ that $\varphi$

Note: Ka p is equivalent to D{a} p — individual knowledge is distributed knowledge for a singleton coalition. K{a,b} p is syntactic sugar for (Ka p & Kb p).

Reference

Tableau-based decision procedure for the multiagent epistemic logic with all coalitional operators for common and distributed knowledge
Mai Ajspur, Valentin Goranko, and Dmitry Shkatov (2012)
arXiv:1201.5346v1