• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International Conference on Logic for Programming, Artificial Intelligence, and Reasoning(LPAR 2005); 20051202-06; Montego Bay(JM) >Automating Coherent Logic
【24h】

Automating Coherent Logic

机译：自动化相干逻辑

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

摘要

First-order coherent logic (CL) extends resolution logic in that coherent formulas allow certain existential quantifications. A substantial number of reasoning problems (e.g., in confluence theory, lattice theory and projective geometry) can be formulated directly in CL without any clausification or Skolemization. CL has a natural proof theory, reasoning is constructive and proof objects can easily be obtained. We prove completeness of the proof theory and give a linear translation from FOL to CL that preserves logical equivalence. These properties make CL well-suited for providing automated reasoning support to logical frameworks. The proof theory has been implemented in Prolog, generating proof objects that can be verified directly in the proof assistant Coq. The prototype has been tested on the proof of Hessenberg's Theorem, which could be automated to a considerable extent. Finally, we compare the prototype to some automated theorem provers on selected problems.
机译：一阶相干逻辑（CL）扩展了解析逻辑，因为相干公式允许某些存在的量化。大量推理问题（例如，在融合理论，格论和射影几何中）可以直接在CL中提出，而无需任何分类或科莱姆化。 CL具有自然的证明理论，推理具有建设性，并且可以轻松获得证明对象。我们证明了证明理论的完备性，并给出了从FOL到CL的线性翻译，以保留逻辑对等。这些属性使CL非常适合为逻辑框架提供自动推理支持。证明理论已在Prolog中实现，生成了可以直接在证明助手Coq中进行验证的证明对象。该原型已通过Hessenberg定理的证明进行了测试，该证明可以在相当大的程度上实现自动化。最后，我们将原型与针对选定问题的一些自动定理证明进行比较。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号