Abstract
Proper epistemic knowledge bases (PEKBs) are syntactic knowledge bases that use multi-agent epistemic logic to represent nested multi-agent knowledge and belief. PEKBs have certain syntactic restrictions that lead to desirable computational properties; primarily, a PEKB is a conjunction of modal literals, and therefore contains no disjunction. Sound entailment can be checked in polynomial time, and is complete for a large set of arbitrary formulae in logics Kn and KDn. In this paper, we extend PEKBs to deal with a restricted form of disjunction: 'knowing whether'. An agent i knows whether Ψ iff agent i knows Ψ or knows ¬Ψ; that is, □i? ∨ □i¬Ψ. In our experience, the ability to represent that an agent knows whether something holds is useful in many multi-agent domains. We represent knowing whether with a modal operator, Δi, and present sound polynomial-time entailment algorithms on PEKBs with Δi in Kn and KDn, but which are complete for a smaller class of queries than standard PEKBs.