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

Abstract

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.