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

• Theoretical Computer Science • Previous Articles     Next Articles

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

1147

Cited

1

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] Zhang Bo; Zhang Ling;. On Memory Capacity of the Probabilistic Logic Neuron Network[J]. , 1993, 8(3): 62 -66 .
[2] SHI Zhongzhi; TIAN Qijia; LI Yunfeng;. RAO Logic for Multiagent Framework[J]. , 1999, 14(4): 393 -400 .
[3] ZHAN Yongzhao; SONG Snunlin; XIE Li;. Demand Priority Protocol Simulation and Evaluation[J]. , 1999, 14(6): 599 -605 .
[4] Ping Hou. Some Representation Theorems for Recovering Contraction Relations[J]. , 2005, 20(4): 536 -541 .
[5] Imad Jawhar and Jie Wu. QoS Support in TDMA-Based Mobile Ad Hoc Networks[J]. , 2005, 20(6): 797 -810 .
[6] Kwangjin Park, Hyunseung Choo, and Chong-Sun Hwang. An Efficient Data Dissemination Scheme for Spatial Query Processing[J]. , 2007, 22(1): 131 -134 .
[7] Lizhong Dai and Dongmei Zhao. Uplink Scheduling for Supporting Real Time Voice Traffic in IEEE 802.16 Backhaul Networks[J]. , 2008, 23(5 ): 806 -814 .
[8] Jia-Hai Yang, Senior Member, CCF, Member, IEEE, Hui Zhang, Member, ACM, IEEE, Jin-Xiang Zhang, and Chang-Qing An. Towards Next Generation Internet Management: CNGI-CERNET2 Experiences[J]. , 2009, 24(3): 482 -494 .
[9] An Liu, Hai Liu, Qing Li, Member, CCF,Senior Member, IEEE, Liu-Sheng Huang,Senior Member, CCF,and Ming-Jun Xiao, Member, CCF. Constraints-Aware Scheduling for Transactional Services Composition[J]. , 2009, 24(4): 638 -651 .
[10] David Sankoff, Chunfang Zheng, Adriana Muñoz, Zhenyu Yang, Zaky Adam, Robert Warren, Vicky Choi, and Qian Zhu. Issues in the Reconstruction of Gene Order Evolution[J]. , 2010, 25(1): 10 -25 .

ISSN 1000-9000(Print)

         1860-4749(Online)
CN 11-2296/TP

 Home
Editorial Board
Author Guidelines
Subscription		 Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
Tel.:86-10-62610746
E-mail: jcst@ict.ac.cn
 
  Copyright ©2015 JCST, All Rights Reserved