Christian Sternagel, René Thiemann
Archive of Formal Proofs 2020.
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.
BibTex
@article{Knuth_Bendix_Order-AFP, author = {Christian Sternagel and René Thiemann}, title = {A Formalization of Knuth–Bendix Orders}, journal = {Archive of Formal Proofs}, month = may, year = 2020, note = {\url{https://isa-afp.org/entries/Knuth_Bendix_Order.html}, Formal proof development}, ISSN = {2150-914x},}