Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Conditional Term Rewriting Systems

CTRS 1987: Conditional Term Rewriting Systems pp 62–83Cite as

A completion procedure for conditional equations

  • Part 1 Research Articles
  • Conference paper
  • First Online:

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

Abstract

The paper presents a new completion procedure for conditional equations. The work is based on the notion of reductive conditional rewriting. The procedure has been designed to also handle nonreductive equations that are generated during completion. The paper in particular presents techniques for simplification of conditional equations and rules, so that the procedure terminates on more specifications. The correctness proofs which form a substantial part of this paper employ recursive path orderings on proof trees, an extension of the ideas of Bachmair, Dershowitz and Hsiang to the conditional case.

This work is partially supported by the ESPRIT-project PROSPECTRA, ref#390.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Solvable cases of the decision problem. North-Holland, 1954.

    Google Scholar 

  2. Bachmair, L.: Proof methods for equational theories. PhD-Thesis, U. of Illinois, Urbana Champaign, 1987.

    Google Scholar 

  3. Bachmair, L., Dershowitz, N. and Hsiang, J.: Proof orderings for equational proofs. Proc. LICS 86, 346–357.

    Google Scholar 

  4. Bertling, H., Ganzinger, H. and Schäfers, R.: CEC: A system for conditional equation completion. User Manual, U. Dortmund, 1987.

    Google Scholar 

  5. Bergstra, J. and Klop, J.W.: Conditional rewrite rules: Confluence and termination. Report IW 198/82, Mathematisch Centrum, Amsterdam, 1982.

    Google Scholar 

  6. Dershowitz, N.: Termination. Proc. RTA 1985, LNCS 202 1985, 180–224.

    Google Scholar 

  7. Dershowitz, N. and Manna, Z.: Proving termination with multiset orderings. CACM 22 (1979), 465–476.

    Google Scholar 

  8. Ganzinger, H.: Ground term confluence in parametric conditional equational specifications. Proc. STACS 1987, LNCS 247, 1987.

    Google Scholar 

  9. Huet, G. and Oppen, D.C.: Equations and Rewrite Rules. A Survey. In: R. Book (ed): Formal Languages: Perspectives and open Problems. Academic Press, New York, 1980, 349–405.

    Google Scholar 

  10. Huet, G.: A complete proof of the correctness of the Knuth-Bendix completion algorithm. JCSS 23 (1981), 11–21.

    Google Scholar 

  11. Hussmann, H.: Unification in conditional-equational theories. Proc. Eurocal 1985, LNCS 204, 1985, 543–553.

    Google Scholar 

  12. Jouannaud, J.P. and Waldmann, B.: Reductive conditional term rewriting systems. Proc. 3rd TC2 Working Conference on the Formal Description of Prog. Concepts, Ebberup, Denmark, Aug. 1986, North-Holland, to appear.

    Google Scholar 

  13. Kaplan, St.: Conditional rewrite rules. TCS 33 (1984), 175–193.

    Article  Google Scholar 

  14. Kaplan, St.: Fair conditional term rewrite systems: unification, termination and confluence. Report 194, U. de Paris-Sud, Centre d'Orsay, Nov. 1984.

    Google Scholar 

  15. Kaplan, St.: A compiler for conditional term rewriting. Proc. RTA 1987, LNCS 256, 1987, 25–41.

    Google Scholar 

  16. Kaplan, St. and Remy J.-L.: Completion algorithms for conditional rewriting systems. MCC Workshop on Resolution of Equations in Algebraic Structures, Austin, May 1987.

    Google Scholar 

  17. Kounalis, E. and Rusinowitch, M.: On word problems in Horn logic. This volume.

    Google Scholar 

  18. Küchlin, W.: A confluence criterion based on the generalised Newman lemma. Proc. Eurocal 1985, LNCS 204, 1985, 390–399.

    Google Scholar 

  19. Küchlin, W.: Equational completion by proof transformation. Ph.D. thesis, Dep't. of Mathematics, ETH Zürich, 1986.

    Google Scholar 

  20. Orejas, F.: Theorem Proving in Conditional-Equational Theories. This volume.

    Google Scholar 

  21. Winkler, F. and Buchberger, B.: A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm. Coll. on Algebra, Combinatorics and Logic in Comp. Sci., Györ, 1983.

    Google Scholar 

  22. Remy, J.L. and Zhang, H.: REVEUR 4: A system for validating conditional algebraic specifications of abstract data types. Proc. 6th ECAI, Pisa 1984, 563–572.

    Google Scholar 

  23. Zhang, H. and Remy, J.L.: Contextual rewriting. Conf. on Rewriting Techniques and Applications, Dijon 1985, LNCS 202.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fachbereich Informatik, Universität Dortmund, D-4600, Dortmund 50, W. Germany

    Harald Ganzinger

Authors
  1. Harald Ganzinger
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

S. Kaplan J. -P. Jouannaud

Rights and permissions

Reprints and permissions

Copyright information

© 1988 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ganzinger, H. (1988). A completion procedure for conditional equations. In: Kaplan, S., Jouannaud, J.P. (eds) Conditional Term Rewriting Systems. CTRS 1987. Lecture Notes in Computer Science, vol 308. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-19242-5_6

Download citation

  • DOI: https://doi.org/10.1007/3-540-19242-5_6

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-19242-8

  • Online ISBN: 978-3-540-39166-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation