  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.
