捉迷藏博弈逻辑：刻画、公理化与可判定性
逻辑
2023-05-26 v1 计算机科学中的逻辑
摘要
捉迷藏博弈逻辑 LHS 被提出用于推理追踪-逃逸环境中的搜索任务与智能体间交互。如文献所证，在 LHS 的语言中引入等号常量会急剧提升其计算复杂度：带多个关系的 LHS 的可满足性问题是不可判定的。本文改进了已有结果，证明带单个关系的 LHS 也是不可判定的。结合已有发现，我们给出了关于该逻辑表达力的 van Benthem 风格刻画定理。最后，通过将 LHS-——LHS 不带等号常量的关键片段——的语言“拆分”为两个“孤立部分”，我们为 LHS- 提供了完备的 Hilbert 风格证明系统，并证明其可满足性问题是可判定的，相关证明将表明 LHS- 与普通积逻辑提案之间的显著差异。尽管 LHS 与 LHS- 是面向 2 个智能体交互的框架，文中所有结果均可轻易推广至任意 n > 2 个智能体设定的泛化版本。
引用
@article{arxiv.2305.16021,
title = {Logic of the Hide and Seek Game: Characterization, Axiomatization, Decidability},
author = {Qian Chen and Dazhu Li},
journal= {arXiv preprint arXiv:2305.16021},
year = {2023}
}