Equational Theories and Validity for Logically Constrained Term Rewriting (Full Version)
Takahito Aoto, Naoki Nishida, Jonas Schöpf
TL;DR
This work establishes a semantic foundation for logically constrained term rewriting by formulating constrained equations $s \approx t$ and CE-theories, and defining CE-validity relative to a background model. It develops a sound inference system $CEC_0$ to prove CE-validity and introduces CE-algebras to capture invalidity via algebraic semantics, proving soundness and completeness results for consistent CE-theories. A key contribution is the tight link between CE-validity and rewrite conversion, enabling semantic verification of constrained equations and supporting a rigorous framework beyond purely syntactic reasoning. The results provide a comprehensive semantic basis for CE reasoning in LCTRSs and pave the way for future automation and extensions to broader theories.
Abstract
Logically constrained term rewriting is a relatively new formalism where rules are equipped with constraints over some arbitrary theory. Although there are many recent advances with respect to rewriting induction, completion, complexity analysis and confluence analysis for logically constrained term rewriting, these works solely focus on the syntactic side of the formalism lacking detailed investigations on semantics. In this paper, we investigate a semantic side of logically constrained term rewriting. To this end, we first define constrained equations, constrained equational theories and validity of the former based on the latter. After presenting the relationship of validity and conversion of rewriting, we then construct a sound inference system to prove validity of constrained equations in constrained equational theories. Finally, we give an algebraic semantics, which enables one to establish invalidity of constrained equations in constrained equational theories. This algebraic semantics derive a new notion of consistency for constrained equational theories.