An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting
Dohan Kim, Teppei Saito, René Thiemann, and Akihisa YamadaProceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2025), 2025.
Abstract
In this paper, we present an Isabelle/HOL formalization of corewrite 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.
BibTeX
@inproceedings{DBLP:conf/cpp/0001ST025,
author = {Dohan Kim and
Teppei Saito and
Ren{\’{e}} Thiemann and
Akihisa Yamada},
editor = {Kathrin Stark and
Amin Timany and
Sandrine Blazy and
Nicolas Tabareau},
title = {An Isabelle Formalization of Co-rewrite Pairs for Non-reachability
in Term Rewriting},
booktitle = {Proceedings of the 14th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2025, Denver, CO, USA, January
20-21, 2025},
pages = {272—282},
publisher = {{ACM}},
year = {2025},
url = {https://doi.org/10.1145/3703595.3705889},
doi = {10.1145/3703595.3705889},
timestamp = {Mon, 03 Mar 2025 21:01:02 +0100},
biburl = {https://dblp.org/rec/conf/cpp/0001ST025.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}