Belief Update for Proper Epistemic Knowledge Bases.

Reasoning about the nested beliefs of others is important in many multi-agent scenarios. While epistemic and doxastic logics lay a solid groundwork to approach such reasoning, the computational complexity of these logics is often too high for many tasks. Proper Epistemic Knowledge Bases (PEKBs) enforce two syntactic restrictions on formulae to obtain efficient querying: both disjunction and infinitely long nestings of modal operators are not permitted. PEKBs can be compiled, in exponential time, to a prime implicate formula that can be queried in polynomial time, while more recently, it was shown that consistent PEKBs had certain logical properties that meant this compilation was unnecessary, while still retaining polynomial-time querying. In this paper, we present a belief update mechanism for PEKBs that ensures the knowledge base remains consistent when new beliefs are added. This is achieved by first erasing any formulae that contradict these new beliefs. We show that this update mechanism can be computed in polynomial time, and we assess it against the well-known KM postulates for belief update.