Knowledge Compilation in Multi-Agent Epistemic Logics

TL;DR

This paper introduces a new normal form SDNF for knowledge compilation in multi-agent epistemic logics, enabling tractable reasoning and modular algorithms, with applications to multi-agent epistemic planning.

Contribution

It proposes SDNF as a normal form for epistemic formulas, demonstrating its properties and applicability to multi-agent epistemic planning, extending to K45n logic.

Findings

Every epistemic formula can be compiled into SDNF.

Major reasoning tasks in SDNF are tractable.

Formulas in SDNF have logical separability.

Abstract

Epistemic logics are a primary formalism for multi-agent systems but major reasoning tasks in such epistemic logics are intractable, which impedes applications of multi-agent epistemic logics in automatic planning. Knowledge compilation provides a promising way of resolving the intractability by identifying expressive fragments of epistemic logics that are tractable for important reasoning tasks such as satisfiability and forgetting. The property of logical separability allows to decompose a formula into some of its subformulas and thus modular algorithms for various reasoning tasks can be developed. In this paper, by employing logical separability, we propose an approach to knowledge compilation for the logic Kn by defining a normal form SDNF. Among several novel results, we show that every epistemic formula can be equivalently compiled into a formula in SDNF, major reasoning tasks in SDNF are tractable, and formulas in SDNF enjoy the logical separability. Our results shed some lights on modular approaches to knowledge compilation. Furthermore, we apply our results in the multi-agent epistemic planning. Finally, we extend the above result to the logic K45n that is Kn extended by introspection axioms 4 and 5.