Skip to main content
SpringerLink
Log in

Clausal Presentation of Theories in Deduction Modulo

  • Regular Paper
  • Published:
Journal of Computer Science and Technology Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

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

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  Google Scholar 

  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.

    Article  MATH  MathSciNet  Google Scholar 

  8. Burel G, Kirchner C. Regaining cut admissibility in deduction modulo using abstract completion. Information and Computation, 2010, 208(2): 140–164.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, 100190, China

    Jian-Hua Gao

  2. University of Chinese Academy of Sciences, Beijing, 100049, China

    Jian-Hua Gao

  3. The National Institute for Research in Computer Science and Control, Paris, 78153, France

    Jian-Hua Gao

Authors
  1. Jian-Hua Gao
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jian-Hua Gao.

Additional information

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.

Electronic supplementary material

Below is the link to the electronic supplementary material.

ESM 1

(DOC 28 kb)

Rights and permissions

Reprints and permissions

About this article

Cite this article

Gao, JH. Clausal Presentation of Theories in Deduction Modulo. J. Comput. Sci. Technol. 28, 1085–1096 (2013). https://doi.org/10.1007/s11390-013-1399-0

Download citation

  • Received:

  • Revised:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11390-013-1399-0

Keywords

Search

Navigation