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

Formalization of the first order theory of rewriting

Venue: 
online - link

Lecturer:
Alexander Lochmann, Researcher at CL

 

Abstract: 

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