A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL
It is well known that (ground) confluence is a decidable property of ground term rewrite systems, and that this extends to larger classes. Here we present a formally verified ground confluence checker for linear, variable-separated rewrite systems. To this end, we formalize procedures for ground tree transducers and so-called RR_n relations. The ground confluence checker is an important milestone on the way to formalizing the decidability of the first-order theory of ground rewriting for linear, variable-separated rewrite systems. It forms the basis for a formalized confluence checker for left-linear, right-ground systems.
Tue 15 JanDisplayed time zone: Belfast change
11:00 - 12:30
|Autosubst 2: Reasoning with Multi-Sorted de Bruijn Terms and Vector Substitutions|
|A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL|