A Formalization of Knuth–Bendix Orders

Title:	A Formalization of Knuth–Bendix Orders
Authors:	Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com) and René Thiemann
Submission date:	2020-05-13
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{http://isa-afp.org/entries/Knuth_Bendix_Order.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	First_Order_Terms, Matrix, Polynomial_Factorization
Used by:	Functional_Ordered_Resolution_Prover
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.