views updated

Knuth–Bendix algorithm A partial algorithm for turning a finite term rewriting system (e.g. derived from a set of equations) into an equivalent complete set of rewrite rules. The algorithm, however, does not always return an input. The process is relevant to the implementation of specification languages, such as OBJ, that allow equational specifications to be written and executed symbolically.

Knuth–Bendix algorithm

Updated About encyclopedia.com content Print Article Share Article