A Logical Analysis of Hanabi

The card game Hanabi has recently gained popularity as a benchmark for handling epistemic reasoning in AI systems. However it has until now mostly been approached through the lens of machine learning rather than formal logical analysis. This is mostly due to the fact that modeling Hanabi in the standard epistemic logic DEL is untractable. In this paper we take a different approach to formalizing Hanabi, using the simple epistemic logic EL-O as a starting point. We generalize common knowledge in EL-O to arbitrary groups of agents and show how to overcome some of the limitations EL-O places on agent reasoning by introducing a special reasoning action. Analyzing our formalization of Hanabi finally leads us to introduce an alternative semantics for our generalization of EL-O in which models are finite and satisfiability checking is NP-complete, and which is enough to fully describe the evolution of knowledge in a game of Hanabi.