A Formalization of Knuth–Bendix Orders

Christian Sternagel and René Thiemann

13 May 2020


We define a generalized version of Knuth–Bendix orders, including subterm coefficient functions. For these orders we formalize several properties such as strong normalization, the subterm property, closure properties under substitutions and contexts, as well as ground totality.
BSD License

Depends On

Used by


Related Entries