Jonas Schöpf, Fabian Mitterwallner, Aart Middeldorp
Proceedings of the 12th International Joint Conference on Automated Reasoning (IJCAR 2024), Lecture Notes in Artificial Intelligence 14740, pp. 298-316, 2024.
Abstract
We show that (local) confluence of terminating logically constrained rewrite systems is undecidable, even when the underlying theory is decidable. Several confluence criteria for logically constrained rewrite systems are known. These were obtained by replaying existing proofs for plain term rewrite systems in a constrained setting, involving a non-trivial effort. We present a simple transformation from logically constrained rewrite systems to term rewrite systems such that criticalx pairs of the latter correspond to constrained critical pairs of the former. The usefulness of the transformation is illustrated by lifting the advanced confluence results based on (almost) development closed critical pairs as well as on parallel critical pairs to the constrained setting.
pdf 
doi:10.1007/978-3-031-63501-4_16
BibTeX
@inproceedings{JSFMAM-IJCAR24, author = "Jonas Sch\"{o}pf and Fabian Mitterwallner and Aart Middeldorp", title = "Confluence of Logically Constrained Rewrite Systems Revisited", booktitle = "Proceedings of the 12th International Joint Conference on Automated Reasoning", editor = "Christoph Benzm\"{u}ller and Marijn J. H. Heule and Renate A. Schmidt", series = "Lecture Notes in Artificial Intelligence", volume = 14740, pages = "298--316", year = 2024, doi = "10.1007/978-3-031-63501-4\_16"}