Efficient reasoning with consistent proper epistemic knowledge bases

Abstract

Reasoning about the nested beliefs or knowledge of other agents is essential for many collaborative and competitive tasks. However, reasoning with nested belief (for example through epistemic logics) is computationally expensive. Proper Epistemic Knowledge Bases (PEKBs) address this by enforcing syntactic restrictions on the knowledge base. By compiling a PEKB and query formula into a specific normal form, entailment can be checked in polynomial time, which is sound and complete for the epistemic logic K. The downside is that the complexity of compiling into the normal form is exponential in time and space. In this work, we extend PEKBs to handle belief in the logic of KD. We show that this ..