Skip to main content
SpringerLink
Log in

Linear completion

  • Chapter 3 Extension Of Knuth-Bendix Completion
  • Conference paper
  • First Online:
Conditional and Typed Rewriting Systems (CTRS 1990)

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

Included in the following conference series:

Abstract

We give an example of a set of linear equational axioms such that no finite canonical rewrite system can be computed by ordered completion with a complete reduction ordering, although such a rewrite system does trivially exist. We then describe a set of inference rules for a completion procedure, called linear completion, that solves the problem when the axioms are linear.

This work has been partially supported by GRECO de Programmation du CNRS

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. L. Bachmair, “Proofs Methods for Equational Theories”, Thesis: University of Illinois at Urbana-Champaign, 1987.

    Google Scholar 

  2. L. Bachmair, N. Dershowitz and J. Hsiang, “Orderings for Equational Proofs”, Symposium on Logic in Computer Science, Boston, June 1986.

    Google Scholar 

  3. N. Dershowitz, “Personal Communication”, Montréal, June 1990.

    Google Scholar 

  4. N. Dershowitz and J.-P. Jouannaud, “Term Rewriting Systems”, in Handbook for Theoretical Computer Science, North-Holland, to appear.

    Google Scholar 

  5. N. Dershowitz and J.-P. Jouannaud, “Notations for Rewriting”, to appear

    Google Scholar 

  6. N. Dershowitz, L. Marcus and A. Tarlecki, “Existence, Uniqueness, and Construction of Rewrite Systems”, Technical Report.

    Google Scholar 

  7. J. Hsiang and M. Rusinowitch, “On Word Problems in Equational Theories”, 14th ICALP, 1987.

    Google Scholar 

  8. G. Huet, “Confluence Reductions: Abstract Properties and Applications to Term Rewritings, JACM, 27, 1980, pp. 797–821.

    Google Scholar 

  9. G. Huet, “A Complete Proof of Correctness of Knuth-Bendix Completion Algorithm”, JCSS, 23, 1981, pp.11–21.

    Google Scholar 

  10. G. Huet and D.C. Oppen, “Equations and Rewrite Rules: A Survey”, Formal Langages: Perspectives and Open Problems, R. Book, Academic Press, 1980.

    Google Scholar 

  11. D.E. Knuth and P.B. Bendix, “Simple Word Problems in Universal Algebra”, Computational Algebra, J. Leach, Pergamon Press, 1970, pp.263–297.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LRI, Université Paris-Sud, Bât 490, 91405, ORSAY Cedex, France

    Hervé Devie

Authors
  1. Hervé Devie
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

S. Kaplan M. Okada

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Devie, H. (1991). Linear completion. In: Kaplan, S., Okada, M. (eds) Conditional and Typed Rewriting Systems. CTRS 1990. Lecture Notes in Computer Science, vol 516. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54317-1_94

Download citation

  • DOI: https://doi.org/10.1007/3-540-54317-1_94

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-54317-6

  • Online ISBN: 978-3-540-47558-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation