Proof Theory for Distributed Knowledge

The proof theory of multi-agent epistemic logic extended with operators for distributed knowledge is studied. Distributed knowledge of A within a group G means that A follows from the totality of what the individual members of G know. There are known axiomatizations for epistemic logics with the distributed knowledge operator, but apparently no cut-free proof system for such logics has yet been presented. A Gentzen-style contraction-free sequent calculus system for propositional epistemic logic with operators for distributed knowledge is given, and a cut-elimination theorem for the system is proved. Examples of reasoning about distributed knowledge using the calculus are given.

• Type: Conference
• Year: 2007
• Where: CLIMA
• Authors: Raul Hakli, Sara Negri
• Keywords: CLIMA 2007, Distributed Knowledge, Epistemic Logic, Intelligent Agents, Multi-agent Epistemic Logic