X-variant Interpretation (Satisfiability Modulo Theory)

Definition

$X$-variant Interpretation (Satisfiability Modulo Theory)

Let $I$ and $I^{\prime }$ be interpretations over the same signature $\Sigma$, and let $X$ be a set of variables. The interpretation $I^{\prime }$ is an $X$-variant of $I$, written $I^{\prime }{\equiv }_{X}I$, if both interpretations have the same carriers and agree on every signature symbol and every variable outside $X$:

$$\begin{array}{rlrl}{D}_s^{I^{\prime }}& =D_s^I& & \text{for every sort }s,\\ {\sigma }^{I^{\prime }}& ={\sigma }^I& & \text{for every symbol }\sigma \in \Sigma ,\\ y^{I^{\prime }}& =y^I& & \text{for every variable }y\notin X.\end{array}$$

Variables in $X$ may be assigned any value of their respective carriers. If $X=\{x\}$, then $I^{\prime }$ is an $x$-variant of $I$.