Bounded Completion


We propose a constraint-based framework for Knuth-Bendix completion.
Completion aims to construct from an equational system E a confluent and
terminating term rewrite system R equivalent to the input E. Our approach
encodes all requirements to R as order constraints. We present theoretical
properties of our framework, such as subsumption of Knuth and Bendix'
procedure, and show experimental data of our prototype implementation.