### Abstract

We define the weighted path order (WPO) and formalize several properties such as strong normalization, the subterm property, and closure properties under substitutions and contexts. Our definition of WPO extends the original definition by also permitting multiset comparisons of arguments instead of just lexicographic extensions. Therefore, our WPO not only subsumes lexicographic path orders (LPO), but also recursive path orders (RPO). We formally prove these subsumptions and therefore all of the mentioned properties of WPO are automatically transferable to LPO and RPO as well. Such a transformation is not required for Knuth–Bendix orders (KBO), since they have already been formalized. Nevertheless, we still provide a proof that WPO subsumes KBO and thereby underline the generality of WPO.

### License

BSD License

### Topics

- Logic/Rewriting

### Session Weighted_Path_Order

- Status
- Precedence
- Relations
- List_Order
- Multiset_Extension_Pair
- Multiset_Extension_Pair_Impl
- Multiset_Extension2
- Multiset_Extension2_Impl
- WPO
- RPO
- LPO
- KBO_Transformation
- KBO_as_WPO
- Executable_Orders

### Depends on

- A Formalization of Knuth–Bendix Orders

### Used by

- A Verified Efficient Implementation of the Weighted Path Order
- Given Clause Loops
- The Generalized Multiset Ordering is NP-Complete

### Auto-related entries

- A Verified Efficient Implementation of the Weighted Path Order

## Cite

×

Weighted_Path_Order-AFP

    @article{Weighted_Path_Order-AFP,
      author  = {Christian Sternagel and René Thiemann and Akihisa Yamada},
      title   = {A Formalization of Weighted Path Orders and Recursive Path Orders},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Weighted_Path_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
- Sep 26, 2021 : Isabelle2021