Thursday, 9th of December 2021, 12:00 – 1:00

Formalization of the first order theory of rewriting

online - link

Alexander Lochmann, Researcher at CL



The first-order theory of rewriting is a decidable theory for finite left-linear right-ground rewrite systems. We present a formally verified variant of the decision procedure for the class of linear variable-separated rewrite systems. This variant supports a more expressive theory and is based on the concept of anchored ground tree transducers. The correctness of the decision procedure is formalized in Isabelle/HOL.


Nach oben scrollen