Differences

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

--- sav08:deciding_quantifier-free_fol [2008/04/17 13:41]
vkuncak
+++ sav08:deciding_quantifier-free_fol [2009/05/05 22:49]
vkuncak
@@ Line 13: / Line 13: @@
 is the following
 \[
-   (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) = 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