Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems
Franziska Rapp, Aart Middeldorp · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2016
The first-order theory of rewriting is decidable for finite left-linear right-ground rewrite systems. We present a new tool that implements the decision procedure for this theory. It is based on tree automata techniques. The tool offers the possibility to synthesize rewrite systems that satisfy properties that are expressible in the first-order theory of rewriting.