Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: A Formalization of Weighted Pa...

view this post on Zulip Email Gateway (Sep 26 2021 at 13:49):

From: Tobias Nipkow <>
A Formalization of Weighted Path Orders and Recursive Path Orders
Christian Sternagel, René Thiemann and Akihisa Yamada

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.


Last updated: Dec 08 2021 at 08:24 UTC