This shows you the differences between two versions of the page.

Link to this comparison view

sav08:partial_congruences [2008/04/23 07:50]
sav08:partial_congruences [2015/04/21 17:30]
Line 1: Line 1:
-====== 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$. 
-**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: 
-   ​\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