Efficient Reasoning About Knowledge and Common Knowledge

We investigate the properties of an epistemic logic with models where propositional variables can be true or false and can be observed or not. Beyond that, there can be observation about other agents’ observations and there can be joint observation. We prove that the resulting Epistemic Logic of Observation (EL-O) can be identified with a fragment of epistemic logic: boolean combinations of ‘knowing-whether’ atoms, that is, sequences of ‘individually knowing-whether’ and ‘commonly knowing-whether’ operators that are followed by a propositional variable. We give a complete axiomatisation of EL-O, taking advantage of a new formulation of the induction axiom for common knowledge that we have recently established. We also prove that the complexity of EL-O satisfiability is NP-complete, which makes it particularly interesting for knowledge representation.