Knuth-Bendix algorithm

Show Summary Details

Quick Reference

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.

Subjects: Computing.

Reference entries

Users without a subscription are not able to see the full content. Please, subscribe or login to access all content.