Abstract

Numerous confluence criteria for plain term rewrite systems are known. For
logically constrained rewrite system, an attractive extension of term
rewriting in which rules are equipped with logical constraints, much less
is known. In this paper we extend the strongly-closed and (almost)
parallel-closed critical pair criteria of Huet and Toyama to the logically
constrained setting. We discuss the challenges for automation and present
crest, a new tool for logically constrained rewriting in which
the confluence criteria are implemented, together with experimental data.

BibTeX

@inproceedings{JSAM-CADE23,
 author    = "Jonas Sch\"{o}pf and Aart Middeldorp",
 title     = "Confluence Criteria for Logically Constrained Rewrite
              Systems",
 booktitle = "Proceedings of the 29th International Conference on Automated
              Deduction",
 editor    = "Brigitte Pientka and Cesare Tinelli",
 series    = "Lecture Notes in Artificial Intelligence",
 volume    = 14132,
 pages     = "474--490",
 year      = 2023,
 doi       = "10.1007/978-3-031-38499-8\_27"
}