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.

翻译：逻辑约束项重写是一种相对较新的形式化方法，其中规则配备了基于任意理论的约束。尽管近年来在逻辑约束项重写的归纳、完备化、复杂性分析和合流性分析方面取得了许多进展，但这些工作仅关注该形式化方法的语法层面，缺乏对语义的深入探讨。本文研究了逻辑约束项重写的语义层面。为此，我们首先定义了约束等式、约束等式理论以及基于后者对前者的有效性。在阐述了有效性与重写转换之间的关系后，我们构建了一个可靠的推理系统，用于证明约束等式在约束等式理论中的有效性。最后，我们提出了一种代数语义，使得能够判定约束等式在约束等式理论中的无效性。该代数语义导出了约束等式理论一致性的新概念。