Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
sav07_lecture_4 [2007/03/27 16:48] leander.eyer |
sav07_lecture_4 [2007/03/28 09:49] iulian.dragos |
||
---|---|---|---|
Line 289: | Line 289: | ||
===== Proving formulas with uninterpreted functions ===== | ===== Proving formulas with uninterpreted functions ===== | ||
- | |||
- | |||
- | |||
- | |||
- | |||
- | |||
- | |||
- | |||
- | |||
- | |||
- | |||
==== Congruence closure algorithm ==== | ==== Congruence closure algorithm ==== | ||
Line 306: | Line 295: | ||
Recall the following properties of the relation **equivalence**: | Recall the following properties of the relation **equivalence**: | ||
- | - x = x (everything is equal to itself) | + | - x = x (everything is equal to itself) (reflexivity) |
- | - x = y -> y = x (reflexivity) | + | - x = y -> y = x (symmetry) |
- x = y ∧ y = z -> x = z (transitivity) | - x = y ∧ y = z -> x = z (transitivity) | ||