Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Last revision Both sides next revision | ||
|
sav08:congruence_closure_theorem [2008/04/26 17:05] damien |
sav08:congruence_closure_theorem [2009/05/05 23:23] 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 | ||