Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: A Formalization of Knuth–Bendi...

Email Gateway (Aug 23 2022 at 09:08):

From: Tobias Nipkow <nipkow@in.tum.de>
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!
smime.p7s

Last updated: Feb 01 2025 at 20:19 UTC