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



A Formalization of Knuth–Bendix Orders
Christian Sternagel and René Thiemann

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.

https://www.isa-afp.org/entries/Knuth_Bendix_Order.html

Enjoy this classic!

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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