LARA

Partial Congruences

Instead of a congruence on the (typically infinite) set of all ground terms we will compute congruences on a given finite set of ground terms. We call these congruences partial congruences; they are simply congruences on a subset of the original set.

Theorem: Let $T$ be a set of ground terms and $s$ a congruence on $T$. Then $CC(s) \cap T^2 = s$ where $CC(s)$ denotes the congruence closure of $s$.

Proof:

Show $C^i(s) \cap T^2 = s$ for all $i \ge 0$, by induction.

  • $i = 0$: s = s
  • $i \rightarrow i+1$:

$C^{i+1}(s) \cap T^2 = C(C^i(s) \cap T^2) \cap T^2 $, by induction hypothesis $C^i(s) \cap T^2 =s$. Thus $C(C^i(s) \cap T^2) \cap T^2 = C(s) \cap T^2$. As $C$ adds only needed term for congruence, the added term are either not in $T^2$ or $s$ in not a congruence. By hypothesis $s$ is a congruence, so $C(s) \cap T^2 = s$. Therefore $C^{i+1}(s) \cap T^2 = s$.

Proof End.

When checking a formula we compute congruences on a finite set of terms that occur in the formula.

We apply the congruence condition only to terms that already exist in the set, using congruence condition:

\begin{equation*}
\begin{array}{l}
   \forall x_1,\ldots,x_n,y_1,\ldots,y_n. \bigwedge_{i=1}^n (x_i,y_i) \in r\ \land \ f(x_1,\ldots,x_n) \in T \land f(y_1,\ldots,y_n) \in T  \rightarrow \\ 
    (f(x_1,\ldots,x_n),f(y_1,\ldots,y_n)) \in r
\end{equation*}