Differences
This shows you the differences between two versions of the page.
Next revision Both sides next revision | |||
sav08:congruence_closure_theorem [2008/04/23 06:45] vkuncak created |
sav08:congruence_closure_theorem [2008/04/26 17:05] damien |
||
---|---|---|---|
Line 3: | Line 3: | ||
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 of Equality]]). | ||
- | **Theorem** Let $E$ be a set of ground equalities and disequalities. Then the following are equivalent: | + | **Theorem** Let $E$ be a set of ground equalities and disequalities |
+ | ($E := \bigwedge_{i = 0}^m t_i = t_i^\prime \wedge \bigwedge_{i = m+1}^n t_i \neq t_i^\prime$). | ||
+ | Then the following are equivalent: | ||
* $E$ is satisfiable | * $E$ is satisfiable | ||
* there exists a congruence on ground terms in which $E$ is true | * there exists a congruence on ground terms in which $E$ is true |