Logic of the Hide and Seek Game: Characterization, Axiomatization, Decidability

The logic of the hide and seek game \(\textsf{LHS}\) was proposed to reason about search missions and interactions between agents in pursuit-evasion environments. As proved in [15, 16], having an equality constant in the language of \(\textsf{LHS}\) drastically increases its computational complexity: the satisfiability problem for \(\textsf{LHS}\) with multiple relations is undecidable. In this work, we improve the existing proof for the undecidability by showing that \(\textsf{LHS}\) with a single relation is undecidable. With the findings of [15, 16], we provide a van Benthem style characterization theorem for the expressive power of the logic. Finally, by ‘splitting’ the language of \(\textsf{LHS}^-\) , a crucial fragment of \(\textsf{LHS}\) without the equality constant, into two ‘isolated parts’, we provide a complete Hilbert style proof system for \(\textsf{LHS}^-\) and prove that its satisfiability problem is decidable, whose proofs would indicate significant differences between the proposals of \(\textsf{LHS}^-\) and of ordinary product logics. Although \(\textsf{LHS}\) and \(\textsf{LHS}^-\) are frameworks for interactions of 2 agents, all results in the article can be easily transferred to their generalizations for settings with any \(n>2\) agents.