A Formalization of Knuth–Bendix Orders (Q7361077)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Knuth_Bendix_Order
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | A Formalization of Knuth–Bendix Orders |
AFP entry Knuth_Bendix_Order |
Statements
13 May 2020
0 references
Christian Sternagel
0 references
René Thiemann
0 references
A Formalization of Knuth–Bendix Orders (English)
0 references
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.
0 references
