LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:congruence_closure_theorem [2008/04/26 17:05]
damien
sav08:congruence_closure_theorem [2009/05/06 00:25]
vkuncak
Line 1: Line 1:
 ====== A Congruence Closure Theorem ====== ====== A Congruence Closure Theorem ======
  
-Recall that we convert all relation symbols into function symbols (to simplify the [[Axioms ​of Equality]]).+Recall that we convert all relation symbols into function symbols (to simplify the [[Axioms ​for Equality]]).
  
 **Theorem** Let $E$ be a set of ground equalities and disequalities **Theorem** Let $E$ be a set of ground equalities and disequalities
Line 13: Line 13:
 **Proof:** **Proof:**
  
-The equivalence of first two statements ++|follows from the construction of [[Herbrand Universe for Equality]].++  ​+The equivalence of first two statements ++|follows from the construction of [[Herbrand Universe for Equality]]. We also directly show this special case.++  ​
  
 The equivalence of last two statements follows by definition. The equivalence of last two statements follows by definition.