Skip to main content
SpringerLink
Log in
Book cover

International Conference on Automated Deduction

CADE 1980: 5th Conference on Automated Deduction Les Arcs, France, July 8–11, 1980 pp 195–207Cite as

Adding dynamic paramodulation to rewrite algorithms

  • Thursday Morning
  • Conference paper
  • First Online:

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

Abstract

A practical and effective solution to a problem resulting from the existence of critical pairs in a set of rewrite rules is presented.

We show how to modify rewrite algorithms by introducing a dynamic paramodulation of rules. This can be done in different ways. The related issues are discussed.

A concrete example is given in the case of the "depth first" rewrite algorithm.

International Fellow at SRI, supported by a grant from I.R.I.A., 78150 Le Chesnay, France, and AFOSR contract F49620-79-C-0099.

supported by a NATO grant.

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. R. S. Boyer and J S. Moore. A Computational Logic. Academic Press Inc., New York, 1979.

    Google Scholar 

  2. Robert S. Boyer, J Strother Moore. A Theorem Prover for Recursive Functions: a User's Manual. CSL-91, NR 049–378, SRI International, Menlo-Park, California 94025, June, 1979.

    Google Scholar 

  3. P. Y Gloess. A Proof of the Correctness of a Simple Parser of Expressions by the Boyer-Moore System. Technical Report N00014-75-C-0816-SRI-7, SRI International, Menlo Park, California 94025, August, 1978.

    Google Scholar 

  4. P. Y Gloess, J-P Laurent. Adding Dynamic Paramodulation to Rewrite Algorithms. Technical Report CSL-102, SRI International, Menlo Park, CA94025, December, 1979.

    Google Scholar 

  5. G. Huet. Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems. Rapport Laboria no250, IRIA-LABORIA, Domaine de Voluceau, 78150 Le Chesnay, France, August, 1977.

    Google Scholar 

  6. G. Huet. Equations and Rewrite Rules: a Survey. CSL-111, SRI International, Menlo Park, California 94025, January, 1980.

    Google Scholar 

  7. D. E. Knuth and P. G. Bendix. Simple Word Problems in Universal Algebras. In J. Leech, Ed., Computational Problems in Abstract Algebra, Pergamon Press, New York, 1970, pp. 263–297.

    Google Scholar 

  8. D. S. Lankford. Canonical Inference. Automatic Theorem Proving Project Report ATP-32, University of Texas, December, 1975.

    Google Scholar 

  9. D. R. Musser. Convergent Sets of Rewrite Rules for Abstract Data Types. USC Information Sciences Institute, 4676 Admiralty Way, Marina del Rey, California 90291, December, 1978. Extended Abstract

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. SRI International, 94025, Menlo Park, California, U.S.A.

    Paul Y Gloess & Jean-Pierre H Laurent (Maître Assistant)

  2. Universitè de Caen, 14032, Caen Cedex, France

    Jean-Pierre H Laurent (Maître Assistant)

Authors
  1. Paul Y Gloess
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jean-Pierre H Laurent
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Wolfgang Bibel Robert Kowalski

Rights and permissions

Reprints and permissions

Copyright information

© 1980 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gloess, P.Y., Laurent, JP.H. (1980). Adding dynamic paramodulation to rewrite algorithms. In: Bibel, W., Kowalski, R. (eds) 5th Conference on Automated Deduction Les Arcs, France, July 8–11, 1980. CADE 1980. Lecture Notes in Computer Science, vol 87. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-10009-1_16

Download citation

  • DOI: https://doi.org/10.1007/3-540-10009-1_16

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-38140-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation