• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of logic and computation >Event Calculus Reasoning Through Satisfiability
【24h】

Event Calculus Reasoning Through Satisfiability

机译：通过可满足性进行事件演算推理

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

We present an implemented method for encoding reasoning problems of a discrete version of the classical logic event calculus in propositional conjunctive normal form, enabling the problems to be solved efficiently by off-the-shelf complete satisfiability (SAT) solvers. We build on the previous encoding method of Shanahan and Witkowski, extending it to support causal constraints, concurrent events, determining fluents, effect axioms with conditions, events triggered by conditions, gradual change, incompletely specified initial situations, state constraints, and release from the commonsense law of inertia. We present an alternative classical logic axiomatization of the event calculus and prove its equivalence to a standard axiomatiza-tion for integer time. We describe our encoding method based on the alternative axiomatization and prove its correctness. We evaluate the method on 14 benchmark reasoning problems for the event calculus and compare performance with the causal calculator on eight problems in the zoo world domain.
机译：我们提出了一种用于以命题合取范式形式编码经典逻辑事件演算的离散版本的推理问题的实现方法，使这些问题可以通过现成的完全可满足性（SAT）求解器得到有效解决。我们以Shanahan和Witkowski的先前编码方法为基础，将其扩展为支持因果约束，并发事件，确定流利，带有条件的影响公理，条件触发的事件，逐渐变化，不完全指定的初始情况，状态约束以及从常识惯性定律。我们提出了事件演算的替代经典逻辑公理化，并证明了其与整数时间标准公理化的等效性。我们描述了基于替代公理化的编码方法，并证明了其正确性。我们评估了针对事件演算的14个基准推理问题的方法，并与因果计算器对动物园世界域中的8个问题的性能进行了比较。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号