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.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. S. Boyer and J S. Moore. A Computational Logic. Academic Press Inc., New York, 1979.
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.
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.
P. Y Gloess, J-P Laurent. Adding Dynamic Paramodulation to Rewrite Algorithms. Technical Report CSL-102, SRI International, Menlo Park, CA94025, December, 1979.
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.
G. Huet. Equations and Rewrite Rules: a Survey. CSL-111, SRI International, Menlo Park, California 94025, January, 1980.
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.
D. S. Lankford. Canonical Inference. Automatic Theorem Proving Project Report ATP-32, University of Texas, December, 1975.
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
Author information
Authors and Affiliations
Editor information
Rights 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