An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting

Dohan Kim, Teppei Saito, René Thiemann, and Akihisa Yamada
Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2025), 2025.

 pdf

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