Confluence of Logically Constrained Rewrite Systems Revisited
Open Access
- 2 July 2024
- book chapter
- Published by Springer Nature
- p. 298-316
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 critical 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.Keywords
All Related Versions
This publication has 18 references indexed in Scilit:
- Confluence Criteria for Logically Constrained Rewrite Systems2023
- Confluence by Critical Pair Analysis Revisited2019
- A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems2018
- CSI: New Evidence – A Progress Report2017
- Labelings for Decreasing DiagramsJournal of Automated Reasoning, 2014
- Term Rewriting with Logical Constraints2013
- Disproving Confluence of Term Rewriting Systems by Interpretation and Ordering2013
- Proving Confluence of Term Rewriting Systems Automatically2009
- Confluence without termination via parallel critical pairs1996
- Simple Word Problems in Universal Algebras††The work reported in this paper was supported in part by the U.S. Office of Naval Research.1970