Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:deciding_quantifier-free_fol [2008/04/17 13:41] vkuncak |
sav08:deciding_quantifier-free_fol [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 8: | Line 8: | ||
Example: is the following formula satisfiable: | Example: is the following formula satisfiable: | ||
- | \[ | + | \begin{equation*} |
a=f(a) \land a \neq b | a=f(a) \land a \neq b | ||
- | \] | + | \end{equation*} |
is the following | is the following | ||
- | \[ | + | \begin{equation*} |
- | (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) |
- | \] | + | \end{equation*} |
- | + | ||
- | ===== 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 | + | |