An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting
In this paper, we present an Isabelle/HOL formalization of co-rewrite pairs for non-reachability analysis in term rewriting. In particular, we formalize polynomial interpretations over negative integers as well as the weighted path order (WPO) and its variant co-WPO. With this formalization, the verified certifier CeTA is now able to check such non-reachability proofs, including those for non-reachability problems of a database where existing tools fail to provide certified proofs.
Authors
- Akihisa Yamada (ORCID: https://orcid.org/0000-0001-8872-2240)
- Teppei Saito (ORCID: https://orcid.org/0009-0001-9786-0044)
- René Thiemann (ORCID: https://orcid.org/0000-0002-0323-8829)
- Dohan Kim (ORCID: https://orcid.org/0000-0003-1973-615X)
Institutions
- Japan Advanced Institute of Science and Technology (JP)
- Universität Innsbruck (AT)
Publication Details
- Published
- 2025-01-10
- DOI
- https://doi.org/10.1145/3703595.3705889
- Primary Topic
- Logic, programming, and type systems
- Type
- article
- Field-Weighted Citation Impact
- 0.00
Funders
- Austrian Science Fund
- Japan Society for the Promotion of Science