[isabelle] New in the AFP: A Formalization of Knuth–Bendix

It would be useful to have a generator. If we also have a term order and terms are enumerable, the first approach for algorithms could be:
  a) enumerate all pairs (term,term) and
  b) decide if they are reducible
That could lead to a generalized TRS.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.