The logic of the hide and seek game LHS was proposed to reason about search missions and interactions between agents in pursuit-evasion environments. As proved in literature, having an equality constant in the language of LHS drastically increases its computational complexity: the satisfiability problem for LHS with multiple relations is undecidable. In this work we improve the existing result by showing that LHS with a single relation is undecidable. With the existing findings, we provide a van Benthem style characterization theorem for the expressive power of the logic. Finally, by `splitting' the language of LHS-, a crucial fragment of LHS without the equality constant, into two `isolated parts', we provide a complete Hilbert style proof system for LHS- and prove that its satisfiability problem is decidable, whose proofs would indicate significant differences between the proposals of LHS- and of ordinary product logics. Although LHS and 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.

翻译：捉迷藏博弈逻辑（LHS）旨在推理搜索任务及追逃环境中智能体间的交互。文献已证明，在LHS语言中包含相等常数会显著增加其计算复杂度：具有多个关系的LHS可满足性问题是不可判定的。本文改进了现有结果，证明仅含单一关系的LHS也是不可判定的。基于已有发现，我们为该逻辑的表达力提供了van Benthem风格的刻画定理。最后，通过将LHS-（LHS不含相等常数的关键片段）的语言“分裂”为两个“孤立部分”，我们为LHS-建立了完备的希尔伯特风格证明系统，并证明其可满足性问题是可判定的，其证明过程将表明LHS-与普通乘积逻辑提案之间的显著差异。尽管LHS和LHS-是面向2个智能体交互的框架，本文所有结果可轻松推广至任意n>2个智能体的情境中。