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

2012/01/25 by Mai Ajspur, Ajspur, Mai, Valentin Goranko +3
Computer Science · #03B35 #03B42 #03B70 #68T15 #68T27 #Artificial Intelligence (cs.AI) #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #I.2.4 #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Multi-Agent Systems and Negotiation

paper · pdf · doi:10.48550/arxiv.1201.5346

openalex publication_date 2012/01/25 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Citations

• Cooperation, Knowledge, and Time: Alternating-time Temporal Epistemic Logic and its Applications
• A near-optimal method for reasoning about action
• Alternating-time temporal logic
• Optimal and Cut-free Tableaux for Propositional Dynamic Logic with\n Converse

Related

• Tableau-based procedure for deciding satisfiability in the full coalitional multiagent epistemic logic
• Completeness of Epistemic Coalition Logic with Group Knowledge
• Tableaux for epistemic Gödel logic
• Tableau-based decision procedures for logics of strategic ability in multi-agent systems
• Cayley structures and common knowledge