### 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.

### License

BSD License

### Topics

- Logic/Rewriting

### Session Knuth_Bendix_Order

- Order_Pair
- Lexicographic_Extension
- KBO

### Depends on

- First-Order Terms
- Executable Matrix Operations on Matrices of Arbitrary Dimensions
- Polynomial Factorization

### Used by

- Undecidability Results on Orienting Single Rewrite Rules
- Regular Tree Relations
- A Formalization of Weighted Path Orders and Recursive Path Orders
- A Verified Functional Implementation of Bachmair and Ganzinger’s Ordered Resolution Prover

### Auto-related entries

- Abstract Rewriting

## Cite

×

Knuth_Bendix_Order-AFP

    @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},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- May 16, 2020 : Isabelle2020
- May 15, 2020 : Isabelle2020