2026-08-20T02:01:28Z
https://drops.dagstuhl.de/oai
oai:drops-oai.dagstuhl.de:19680
2024-03-06T11:04:38Z
ddc:004
open_access
Confluence of Conditional Rewriting Modulo
Lucas, Salvador
Conditional rewriting
Confluence
Program analysis
We investigate confluence of rewriting with Equational Generalized Term Rewriting Systems R, consisting of Horn clauses, some of them defining conditional equations s = t β c and rewriting rules π β 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 semi-equational) Conditional Term Rewriting Systems. A set of equations E defines an equivalence =_E and quotient set T(F,X)/=_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 Ο, which can be viewed as logical sentences, to prove and disprove confluence of β_{R/E} by (dis)proving joinability of such conditional pairs Ο.
Schloss Dagstuhl β Leibniz-Zentrum fΓΌr Informatik
Salvador Lucas
2024
Is Part Of LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)
InProceedings
Text
doc-type:ResearchArticle
publishedVersion
application/pdf
doi:10.4230/LIPIcs.CSL.2024.37
urn:nbn:de:0030-drops-196809
https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.37
eng
https://creativecommons.org/licenses/by/4.0/legalcode