Abstract
Knuth and Bendix (1970) proposed a procedure that attempts to transform a given set of equations into a convergent rewrite system. This completion procedure must be supplied with a reduction ordering, which determines the direction in which an equation is to be oriented into a rewrite rule. It deduces new equations by a process called superposition. An intriguing feature of the procedure is that rewrite rules can be used to simplify other, already deduced equations. Terms can therefore be kept in fully simplified form and redundant equations can be discarded. Deduction and simplification are the two main components of completion. While simplification accounts for the practicality of completion, it also complicates the task of verifying that a procedure is correct (i. e., does in fact produce a convergent set of equations).
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1991 Birkhäuser Boston
About this chapter
Cite this chapter
Bachmair, L. (1991). Standard Completion. In: Canonical Equational Proofs. Progress in Theoretical Computer Science. Birkhäuser Boston. https://doi.org/10.1007/978-1-4684-7118-2_2
Download citation
DOI: https://doi.org/10.1007/978-1-4684-7118-2_2
Publisher Name: Birkhäuser Boston
Print ISBN: 978-0-8176-3555-8
Online ISBN: 978-1-4684-7118-2
eBook Packages: Springer Book Archive