This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
J-P. Jouannaud, H. Kirchner. (1984) Completion of a Set of Rules Modulo a Set of Equations. Proceedings 11th POPL, Salt Lake City.
C. Kirchner. (1987) Methods and Tools for Equational Unification. Proceedings of the Colloquium on the Resolution of Equations in Algebraic Structures, Lakeway, Texas.
D. Knuth and P. Bendix. (1970) Simple Word Problems in Universal Algebras. in J. Leech, ed., Computational Problems in Abstract Algebra, 263–297, Pergamon Press, Oxford, U.K.
D. Lankford, M. Ballantyne. (1977) Decision Procedures for Simple Equational Theories with Commutative Axioms: Complete Sets of Commutative Reductions. U.T. Austin Math Tech Report ATP-35.
P. Lincoln and J. Christian. (1988) Adventures in Associative-Commutative Unification. Proceedings CADE-9 358–367. Full version to appear in Journal of Symbolic Computation.
R. Lusk, W. McCune, R. Overbeek. Implementation of Theorem Provers: An Argonne Perspective. Lecture notes from a seminar at CADE-9.
G. Peterson, M. Stickel. (1981) Complete Sets of Reductions for Some Equational Theories. JACM 28, 233–264.
D. H. Warren. (1983) An Abstract Prolog Instruction Set. SRI Technical Note 309.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Christian, J. (1989). Fast Knuth-Bendix completion: Summary. In: Dershowitz, N. (eds) Rewriting Techniques and Applications. RTA 1989. Lecture Notes in Computer Science, vol 355. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-51081-8_136
Download citation
DOI: https://doi.org/10.1007/3-540-51081-8_136
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-51081-9
Online ISBN: 978-3-540-46149-4
eBook Packages: Springer Book Archive