Skip to main content
SpringerLink
Log in

An Algebra of Resolution

  • Conference paper
Rewriting Techniques and Applications (RTA 2000)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1833))

Included in the following conference series:

Abstract

We propose an algebraic reconstruction of resolution as Knuth-Bendix completion. The basic idea is to model propositional ordered Horn resolution and resolution as rewrite-based solutions to the uniform word problems for semilattices and distributive lattices. Completion for non-symmetric transitive relations and a variant of symmetrization normalize and simplify the presentation. The procedural content of resolution, its refutational completeness and redundancy elimination techniques thereby reduce to standard algebraic completion techniques. The reconstruction is analogous to that of the Buchberger algorithm by equational completion.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bachmair, L.: Canonical Equational Proofs. Birkhäuser, Basel (1991)

    MATH  Google Scholar 

  2. Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: Aït-Kacy, H., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures. Rewriting Techniques, ch. 1, vol. 2, pp. 1–30. Academic Press, London (1989)

    Google Scholar 

  3. Bachmair, L., Plaisted, D.: Termination orderings for associative-commutative rewriting systems. J. Symbolic Computation 1(4), 329–349 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  4. Buchberger, B.: Basic features and development of the critical-pair/completion procedure. In: Jouannaud, J.-P. (ed.) RTA 1985. LNCS, vol. 202, pp. 1–45. Springer, Heidelberg (1985)

    Google Scholar 

  5. Bündgen, R.: Buchberger’s algorithm: The term rewriter’s point of view. Theoretical Computer Science 159(2), 143–190 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  6. Delor, C., Puel, L.: Extension of the associative path ordering to a chain of associative-commutative symbols. In: Kirchner, C. (ed.) RTA 1993. LNCS, vol. 690, pp. 389–404. Springer, Heidelberg (1993)

    Google Scholar 

  7. Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Formal Models and Semantics, ch. 6, vol. B, pp. 244–320. Elsevier, Amsterdam (1990)

    Google Scholar 

  8. Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15, 1155–1194 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  9. Le Chenadec, P.: Canonical Forms in Finitely Presented Algebras. Research Notes in Theoretical Computer Science. Pitman [u.a.], London (1986)

    MATH  Google Scholar 

  10. Leitsch, A.: The Resolution Calculus. Springer, Heidelberg (1997)

    MATH  Google Scholar 

  11. Levy, J., Agustí, J.: Bi-rewrite systems. J. Symbolic Computation 22, 279–314 (1996)

    Article  MATH  Google Scholar 

  12. Lorenzen, P.: Algebraische und logistische Untersuchungen über freie Verbände. The Journal of Symbolic Logic 16(2), 81–106 (1951)

    Article  MATH  MathSciNet  Google Scholar 

  13. Martin, U., Nipkow, T.: Ordered rewriting and confluence. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 366–380. Springer, Heidelberg (1990)

    Google Scholar 

  14. Socher-Ambrosius, R.: Boolean algebra admits no convergent term rewriting system. In: Book, R.E. (ed.) 4th International Conference on Rewriting Techniques and Applications. LNCS, vol. 488, pp. 264–274. Springer, Heidelberg (1991)

    Google Scholar 

  15. Struth, G.: Non-symmetric rewriting. Technical Report MPI-I-96-2-004, Max- Planck-Institut für Informatik, Saarbrücken (1996)

    Google Scholar 

  16. Struth, G.: On the word problem for free lattices. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 128–141. Springer, Heidelberg (1997)

    Google Scholar 

  17. Struth, G.: Canonical Transformations in Algebra, Universal Algebra and Logic. PhD thesis, Institut für Informatik, Universität des Saarlandes (1998)

    Google Scholar 

  18. Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning, vol. 2, pp. 466–483. Springer, Heidelberg (1983) (reprint)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Albert-Ludwigs-Universität Freiburg, Georges-Köhler-Allee, D-79110, Freiburg i. Br., Germany

    Georg Struth

Authors
  1. Georg Struth
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Stony Brook University, Stony Brook, P.O. Box, New York

    Leo Bachmair

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Struth, G. (2000). An Algebra of Resolution. In: Bachmair, L. (eds) Rewriting Techniques and Applications. RTA 2000. Lecture Notes in Computer Science, vol 1833. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10721975_15

Download citation

  • DOI: https://doi.org/10.1007/10721975_15

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67778-9

  • Online ISBN: 978-3-540-44980-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation