Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Tue 15 Jan 2019 12:00 - 12:30 at Sala XII - Research Papers: Rewriting, Automated Reasoning Chair(s): Andrei Popescu

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 Jan

CPP-2019
11:00 - 12:30: CPP 2019 - Research Papers: Rewriting, Automated Reasoning at Sala XII
Chair(s): Andrei PopescuMiddlesex University, London
CPP-201911:00 - 11:30
Research paper
Kathrin StarkSaarland University, Germany, Steven SchäferSaarland University, Jonas Kaiser
DOI
CPP-201911:30 - 12:00
Research paper
Alexander Lochmann, Christian SternagelUniversity of Innsbruck, Austria
DOI
CPP-201912:00 - 12:30
Research paper
DOI