Differences
This shows you the differences between two versions of the page.
| Next revision | Previous revision | ||
|
sav08:congruence_closure_theorem [2008/04/23 06:45] vkuncak created |
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. 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 | ||
| Line 11: | 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. | ||