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 simplifies the complexity of the required reasoning, and importantly, achieves polynomial entailment checking without first having to compile the PEKB into a normal form. Also, we present an alternative approach that calculates the closure of a PEKB, which is exponential in the maximum depth of nested belief, but for which entailment checking is constant on average.