Confluence of Conditional Rewriting Modulo





Publicado en

Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023)

Licencia Creative Commons


We investigate confluence of rewriting with equational generalized rewrite systems R, consisting of Horn clauses, some of them defining *conditional equations s=t <= c and one-step reductions l -> r <= c. In both cases, c is a sequence of atoms, possibly defined by using additional Horn clauses. Such systems include equational term rewriting systems and (join, oriented, and semiequational) conditional term rewriting systems. Equations E define the equivalence =E and quotient set T/=E of terms, where reductions s ->R/E t using rules in R occur. For such systems, we obtain a finite set of conditional pairs $\pi$, which can be viewed as logical sentences, to prove and disprove confluence of ->R/E by (dis)proving joinability of such conditional pairs $\pi$.


Acerca de Lucas, Salvador

Palabras clave

Conditional Rewriting, Confluence, Equational Rewriting, Program Analysis
Página completa del ítem
Notificar un error en este artículo
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX