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

Logic Journal of the IGPL 21 (3):407-437 (2013)
Download Edit this record How to cite View on PhilPapers
Abstract
We develop a conceptually clear, intuitive, and feasible decision procedure for testing satisfiability in the full multi\-agent epistemic logic \CMAELCD\ with operators for common and distributed knowledge for all coalitions of agents mentioned in the language. To that end, we introduce Hintikka structures for \CMAELCD\ 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 \CMAELCD\ and closes for every unsatisfiable input set of formulae.
Categories
PhilPapers/Archive ID
AJSTDP
Revision history
Archival date: 2018-04-20
View upload history
References found in this work BETA
Reasoning About Knowledge.Fagin, Ronald; Y. Halpern, Joseph; Moses, Yoram & Vardi, Moshe
Comparing Semantics of Logics for Multi-Agent Systems.Goranko, Valentin & Jamroga, Wojciech
Cut-Free Common Knowledge.Jäger, Gerhard; Kretz, Mathis & Studer, Thomas

View all 6 references / Add more references

Citations of this work BETA

Add more citations

Added to PP index
2016-06-30

Total views
63 ( #32,463 of 43,036 )

Recent downloads (6 months)
11 ( #37,297 of 43,036 )

How can I increase my downloads?

Downloads since first upload
This graph includes both downloads from PhilArchive and clicks to external links.