Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:deciding_quantifier-free_fol [2008/04/17 13:41] vkuncak |
sav08:deciding_quantifier-free_fol [2008/04/23 06:49] vkuncak |
||
|---|---|---|---|
| Line 15: | Line 15: | ||
| (f(a)=b \lor (f(f(f(a))) = a \land f(a) \neq f(b))) \land f(f(f(f(a)) \neq b \land b=f(b) | (f(a)=b \lor (f(f(f(a))) = a \land f(a) \neq f(b))) \land f(f(f(f(a)) \neq b \land b=f(b) | ||
| \] | \] | ||
| - | |||
| - | ===== Congruence Closure Algorithm ===== | ||
| - | |||
| - | Recall [[Herbrand Universe for Equality]]. | ||
| - | |||
| - | What can we assume about the domain of interpretations of $a,b,f$? ++ | they are interpreted over elements of factor structure of ground terms ++ | ||
| - | |||
| - | Recall [[Axioms for Equality]]. | ||
| - | |||
| - | Suppose that there exists a model. What do we know about the congruence? | ||
| - | |||
| - | The family of all congruences that contain a given relation. | ||
| - | |||
| - | Closure under intersection. | ||
| - | |||
| - | Existence of smallest congruence containing a given relation. | ||
| - | |||
| - | Iterative algorithm for finding congruence closure. | ||
| - | |||
| - | ===== References ===== | ||
| - | |||
| - | * {{:nelsonoppen80decisionprocedurescongruenceclosure.pdf|Decision Procedures Based on Congruence Closure}} | ||
| - | * Greg Nelson's PhD thesis: Techniques for Program Verification, Stanford, 1981 | ||