A Formalization of Knuth–Bendix Orders

Christian Sternagel 📧 and René Thiemann 🌐

May 13, 2020

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

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.

License

BSD License

Topics

Session Knuth_Bendix_Order