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.

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