Abstract
Proving that something is a consequence of a set of axioms can be very difficult. The Knuth-Bendix completion algorithm attempts to automate this process when the axioms are equations. The algorithm is bound up in the area of term rewriting, and so this paper contains an introduction to the theory of term rewriting, followed by an overview of the algorithm. Finally a formal specification of the algorithm is given using the language Z [7, 8].
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
B. D. Bramson “Tools for the Specification, Design, Analysis and Verification of software”. RSRE report number 87005 (1987)
N. Dershowitz “Termination of Rewriting” pp 69–115 in Journal of Symbolic Computation, Vol 3 (1987)
A. J. J. Dick “Automated Equational Reasoning and the Knuth-Bendix Algorithm: An Informal Introduction” Rutherford Appleton Laboratory report number RAL-88–043 (1988)
D.E. Knuth and P.B. Bendix “Simple Word Problems in Universal Algebras” pp 263–297 in Computational Problems in Abstract Algebra, ed J. Leech, Pergamon press (1970)
MALPAS Intermediate Language (Version 4.0). Rex, Thompson and partners (1987)
J. A. Robinson “A Machine-Oriented Logic Based on the Resolution Principle” pp 23–41 in Journal of the Association for Computing Machinery, Vol 12, No 1 (1965)
C. T. Sennett “Review of Type Checking and Scope Rules of the Specification Language Z”. RSRE report number 87017 (1987)
J. M. Spivey “The Z Notation: A Reference Manual” Prentice-Hall International, Series in Computing Science (1988)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1990 Springer-Verlag London
About this paper
Cite this paper
Smith, A. (1990). The Knuth-Bendix Completion Algorithm and Its Specification in Z. In: Nicholls, J.E. (eds) Z User Workshop. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3877-8_14
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3877-8_14
Publisher Name: Springer, London
Print ISBN: 978-3-540-19627-3
Online ISBN: 978-1-4471-3877-8
eBook Packages: Springer Book Archive