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.

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"
}