›› 2013,Vol. 28 ›› Issue (6): 1085-1096.doi: 10.1007/s11390-013-1399-0

• Special Section on Selected Paper from NPC 2011 • 上一篇    下一篇

Deduction Modulo中理论的子句范式化

Jian-Hua Gao1, 2 (高建华)   

  • 收稿日期:2012-12-04 修回日期:2013-04-16 出版日期:2013-11-05 发布日期:2013-11-05
  • 作者简介:Jian-Hua Gao received his B.S. degree in computer science and technology from Wuhan University of Science and Technology in 2008. He is now a Ph.D. candidate in the University of Chinese Academy of Sciences. His research interest lies in theorem proving and model checking. He was selected by the 2010 Joint Doctoral Promotion Program between The Chinese Academy of Sciences and The French National Institute for Research in Computer Science and Control.

Clausal Presentation of Theories in Deduction Modulo

Jian-Hua Gao1, 2 (高建华)   

  1. 1 State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China University of Chinese Academy of Sciences, Beijing 100049, China;
    2 The National Institute for Research in Computer Science and Control, Paris 78153, France
  • Received:2012-12-04 Revised:2013-04-16 Online:2013-11-05 Published:2013-11-05
  • Supported by:

    Supported by the French National Research Agency{National Natural Science Foundation of China under Grant No. 61161130530 and the National Natural Science Foundation of China under Grant No. 60833001.

PDF (PC)

1147

Resolution Modulo通过添加重写规则将一阶Resolution扩展。在搜索证明的过程中,这些重写规则用来重写子句。在Resolution Modulo的第一个版本中,子句被重写成一般形式的命题。这些命题需要动态地转换成子句。如果重写系统是子句范式的,也就是,把子句重写成子句,那么就可以避免这些令人不愉快的动态转换。本文的工作是将任意一个重写系统转换成一个子句范式的重写系统,且保持了任意相继式无切证明的存在性。

Abstract: Resolution modulo is an extension of first-order resolution in which rewrite rules are used to rewrite clauses during the search. In the first version of this method, clauses are rewritten to arbitrary propositions. These propositions are needed to be dynamically transformed into clauses. This unpleasant feature can be eliminated when the rewrite system is clausal, i.e., when it rewrites clauses to clauses. We show in this paper how to transform any rewrite system into a clausal one, preserving the existence of cut free proofs of any sequent.

[1] Dowek G, Hardin T, Kirchner C. Theorem proving modulo. Journal of Automated Reasoning, 2003, 31(1): 33-72.

[2] Robinson J. A machine-oriented logic based on the resolution principle. Journal of the ACM, 1965, 12(1): 23-41.

[3] Robinson J, Voronkov A. Handbook of Automated Reasioning. The MIT Press, 2001.

[4] Dowek G. Proofs and Algorithms: An Introduction to Logic and Computability. Springer, 2011.

[5] Dowek G. Polarized resolution modulo. In IFIP Advances in Information and Communication Technology 323, Calude C, Sassone V (eds.), Springer-Verlag, 2010, pp.182-196.

[6] Burel G. Experimenting with deduction modulo. In Proc. the 23th International Conference on Automated Deduction, August 2011, pp.162-176.

[7] Hermant O. Resolution is cut-free. Journal of Automated Reasoning, 2010, 44(3): 245-276.

[8] Burel G, Kirchner C. Regaining cut admissibility in deduction modulo using abstract completion. Information and Computation, 2010, 208(2): 140-164.
No related articles found!
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
[1] 张钹; 张铃;. On Memory Capacity of the Probabilistic Logic Neuron Network[J]. , 1993, 8(3): 62 -66 .
[2] 史忠植; 田启家; 李云峰;. RAO Logic for Multiagent Framework[J]. , 1999, 14(4): 393 -400 .
[3] 詹永照; 宋顺林; 谢立;. Demand Priority Protocol Simulation and Evaluation[J]. , 1999, 14(6): 599 -605 .
[4] . 可恢复收缩关系的一些表示定理[J]. , 2005, 20(4): 536 -541 .
[5] . 基于时分多路访问的无线自组网中的服务质量支持[J]. , 2005, 20(6): 797 -810 .
[6] . 空间查询处理的一种有效的数据分发方案[J]. , 2007, 22(1): 131 -134 .
[7] . 在基于 IEEE 802.16的主干网中实行上行链路调度以支持实时语音话务[J]. , 2008, 23(5 ): 806 -814 .
[8] 杨家海 张辉 张金祥 安常青. 下一代互联网络管理研究及其在CNGI-CERNET2的实现[J]. , 2009, 24(3): 482 -494 .
[9] 刘安, 刘海, 李青, 黄刘生, 肖明军. 约束感知的事务型Web服务的调度机制[J]. , 2009, 24(4): 638 -651 .
[10] David Sankoff, Chunfang Zheng, Adriana Munoz, Zhenyu Yang, Zaky Adam, Robert Warren, Vicky Choi, Qian Zhu. 基因顺序的进化过程重建中的问题[J]. , 2010, 25(1): 10 -25 .
版权所有 © 《计算机科学技术学报》编辑部
本系统由北京玛格泰克科技发展有限公司设计开发 技术支持：support@magtech.com.cn
总访问量：