arXiv cs.AI· Till Hofmann, Stefan Schupp, Gerhard Lakemeyer·· 3 天前AI 评分21
有限域情景演算理论中时间推理的可判定性研究
Decidable Reasoning About Time in Finite-Domain Situation Calculus Theories
AI 导读
研究发现，在情景演算中用实值函数 time(a) 为每个动作附加时间点的常见做法，即使域中仅含有限对象，判断是否存在满足给定公式的可达情景也是不可判定的。作者借鉴时间自动机理论，引入带受限后继状态公理和比较运算符的时钟（实值流变量），证明有限域基本动作理论的可达性问题可判定，并给出确定 Golog 程序成功执行动作序列的可判定过程。
正文 · AI 翻译
摘要：表示时间对于信息物理系统至关重要，并已在情境演算中得到广泛研究。最常用的方法是通过添加一个实值函数 $\mathit{time}(a)$ 来表示时间，该函数为每个动作并因此为每个情境附加一个时间点。我们表明，在这种方法中，检查是否存在满足给定公式的可达情境是不可判定的，即使论域中只包含有限多个对象。我们基于时间自动机理论中已确立的结果，提出了一种替代方法，通过引入作为实值流项的时钟，并限制后继状态公理和比较运算符。借助这一限制，我们可以证明有限域基本动作理论的可达性问题是可判定的。最后，我们将结果应用于 Golog 程序实现，给出了一个可判定过程，用于确定给定程序成功执行的动作序列。
| 主题： | 人工智能（cs.AI）；计算机科学中的逻辑（cs.LO） |
| 引用为： | arXiv:2402.03164 [cs.AI] |
| （或 arXiv:2402.03164v3 [cs.AI] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2402.03164 由 DataCite 颁发的 arXiv DOI |
|
| 相关 DOI： | https://doi.org/10.4230/OASIcs.TIME.2026.11
链接到相关资源的 DOI |
提交历史
来自：Till Hofmann [查看电子邮件]
[v1]
2024年2月5日星期一 16:32:12 UTC（78 KB）
[v2]
2026年9月21日星期一 20:54:55 UTC（583 KB）
[v3]
2026年10月13日星期二 14:15:35 UTC（569 KB）
来源：arXiv cs.AI · arxiv.org