We use cookies to improve your experience with our site.
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

Clausal Presentation of Theories in Deduction Modulo

  • 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.
  • loading

Catalog

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return