Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav07_lecture_4 [2007/03/27 16:46] 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 305: | 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) | ||
| Line 314: | Line 304: | ||
| a ≡ b (mod n) is a congruence in respect to addition. Indeed: | a ≡ b (mod n) is a congruence in respect to addition. Indeed: | ||
| - | a ≡ b (mod n) ∧ c ≡ d (mod n) -> a + c ≡ b + d (mod n) | + | a ≡ b (mod n) ∧ c ≡ d (mod n) -> a + c ≡ b + d (mod n) |
| Equality is a congruence with respect to all function symbols. | Equality is a congruence with respect to all function symbols. | ||