Differences
This shows you the differences between two versions of the page.
Next revision | Previous revision Next revision Both sides next revision | ||
sav08:partial_congruences [2008/04/23 07:43] vkuncak created |
sav08:partial_congruences [2008/04/23 07:50] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Partial Congruences ====== | ====== 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. | + | 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. |
- | Let $T$ be a finite set of ground terms. | + | **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$. | ||
+ | |||
+ | **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{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 | ||
+ | \] | ||