Decision Procedures for Epistemic Logic Exploiting Belief Bases

Abstract

We provide tableau-based PSPACE satisfiability checking procedures for a family of multi-agent epistemic logics with a semantics defined in terms of belief bases. Such logics distinguish an agent's explicit beliefs, i.e., all facts included in the agent's belief base, from the agent's implicit beliefs, i.e., all facts deducible from the agent's belief base. We provide a simple dynamic extension for one of these logics by propositional assignments performed by agents. A propositional assignment captures a simple form of action that changes not only the environment but also the agents' beliefs depending on how they jointly perceive its execution. After having provided a PSPACE satisfiability checking procedure for this dynamic extension, we show how it can be used in human-robot interaction in which both the human and the robot have higher-order beliefs about the other's beliefs and can modify the environment by acting.