Abstract
Recognising common knowledge is a crucial component of practical reasoning to allow agents to coordinate efficiently with others. However, while common knowledge has been the focus of many logical theories, these focus on representing propositions that are known to be common knowledge rather than explaining how a proposition comes to be common knowledge. Consequently, there is an absence of both algorithms and software for practical reasoning with common knowledge.
In this paper, we extend and implement philosopher David Lewis's informal analysis of common knowledge based on a formalisation by Cubitt and Sugden. Unlike this prior work, we provide specific practical mechanisms for determining when a state of affairs $A$ indicates that a proposition $P$ holds, and how shared background knowledge and reasoning capabilities are represented: by using theory of mind (ToM) rules and a forward-chaining rule engine. We prove that only two levels of ToM modelling is required to recognise the existence of common knowledge. The approach is implemented using the Prolog Forward Chaining (Pfc) library and is demonstrated in a scenario from classical Athens of decision-making requiring common knowledge.