有限域情境演算时间推理可判定新方法

针对情境演算中常用的为每个动作附加实值 time(a) 函数表示时间的方法，论文证明：即使域中只有有限多个对象，判断是否存在满足给定公式的可达情境也是不可判定的。 为此，作者借鉴时间自动机理论，引入时钟作为带受限后继状态公理和比较算子的实值 fluent，证明有限域基本动作理论的可达性问题可判定。 基于该方法，论文还给出确定 Golog 程序成功执行动作序列的可判定过程。该工作由 Till Hofmann 等作者提交。

AI 根据报道生成 · 2 小时前更新

还没有足够的连续观测数据，暂不绘制趋势。