Abstract

Term rewriting serves as a simple but powerful model of computation that is
Turing-complete. It offers a rich set of techniques to reason about properties
such as termination or confluence, where the latter ensures that the final
result is independent of the order in which rewrite rules are applied.
Logically constrained term rewriting extends this model by equipping rewrite
rules with logical constraints over some theory. This enables built-in support
for data structures and thus eases the analysis of real-world code. While plain
term rewriting has been extensively studied, logically constrained
rewriting – especially confluence analysis – is still in its infancy. In this
thesis, we lift several well-known confluence criteria from term rewrite
systems to logically constrained rewriting. Additionally, we present the first
known non-confluence criterion for logically constrained rewrite systems, along
with modular methods that significantly improve the automation of confluence
analysis. We also introduce formal semantics for logically constrained
rewriting, that serve as the foundation for future research on rewriting
induction. Finally, our tool crest presents an automated push-button confluence
analysis that implements all of our obtained results.

BibTeX

@phdthesis{JS25,
  author    = "Jonas Sch{\"{o}}pf",
  title     = "Automated Analysis of Logically Constrained Rewrite Systems",
  school    = "University of Innsbruck",
  year      = 2025
}