We use cookies to improve your experience with our site.

Indexed in:

SCIE, EI, Scopus, INSPEC, DBLP, CSCD, etc.

Submission System
(Author / Reviewer / Editor)
Advanced Search
Volume 28 Issue 6
November  2013
Turn off MathJax
Article Contents
Abstract
References
Related Articles
Jian-Hua Gao. Clausal Presentation of Theories in Deduction Modulo[J]. Journal of Computer Science and Technology, 2013, 28(6): 1085-1096. DOI: 10.1007/s11390-013-1399-0
Citation: Jian-Hua Gao. Clausal Presentation of Theories in Deduction Modulo[J]. Journal of Computer Science and Technology, 2013, 28(6): 1085-1096. DOI: 10.1007/s11390-013-1399-0
shu

Clausal Presentation of Theories in Deduction Modulo

  • 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

Funds: 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.
More Information
  • Received Date: December 03, 2012
  • Revised Date: April 15, 2013
  • Published Date: November 04, 2013
    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.
    • FullText(HTML)
    • References (8)
  • [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.
    • Relative Articles

  • Related Articles

    [1]NIE Xumin, GUO Qing. Renaming a Set of Non-Horn Clauses[J]. Journal of Computer Science and Technology, 2000, 15(5): 409-415.
    [2]NIE Xumin, GUO Qing. Renaming a Set of Non-Horn Clauses[J]. Journal of Computer Science and Technology, 2000, 15(5).
    [3]SONG Fangmin, QIAN Yuechen. A Syntactic Proof of the Conservativity ofλ_ω overλ_2[J]. Journal of Computer Science and Technology, 1999, 14(2): 129-134.
    [4]Xu Manwu. An Implementation of Pure Horn Clause Logic Programming in a Reduction System[J]. Journal of Computer Science and Technology, 1993, 8(3): 53-61.
    [5]Nie Xumin. On the Complexities of Non-Horn Clause Logic Programming[J]. Journal of Computer Science and Technology, 1992, 7(2): 114-122.
    [6]Liu Dongbo, Li Deyi. A Fuzzy Proof Theory[J]. Journal of Computer Science and Technology, 1990, 5(1): 92-96.
    [7]Zhu Mingyuan. Two Congruent Semantics for Prolog with CUT[J]. Journal of Computer Science and Technology, 1990, 5(1): 82-91.
    [8]Jiang Xinjie, Xu Yongsen. A Proof Rule for While Loop in VDM[J]. Journal of Computer Science and Technology, 1989, 4(2): 178-183.
    [9]Li Renwei. A Natural Deduction System of Temporal Logic[J]. Journal of Computer Science and Technology, 1988, 3(3): 173-185.
    [10]Jin Zhiquan, A. Silberschatz. Proof Techniques for Port-Directed Communication and Broadcast[J]. Journal of Computer Science and Technology, 1987, 2(2): 81-91.
    • Supplements (0)

Catalog

    Get Citation
    PDF
    XML
    Article views (31) PDF downloads (1140) Cited by()
    Related

    Copyright ©2025 JCST, All Rights Reserved     京ICP备05002829号-1

    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

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return