[<<][meta][>>][..]Wed Feb 10 17:07:38 CET 2010

Let's see if I get this right. Given a set of _equalities_ and an order relation on terms, it is possible to construct a confluent rewriting system (if one exists?). The order relation on terms serves to define normal forms. [1] http://en.wikipedia.org/wiki/Knuth–Bendix_completion_algorithm

[Reply][About]

[<<][meta][>>][..]