Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
sav07_lecture_5 [2007/04/03 17:35] vaibhav.rajan |
sav07_lecture_5 [2007/04/03 23:18] vkuncak |
||
|---|---|---|---|
| Line 4: | Line 4: | ||
| * Nelson-Oppen combination method | * Nelson-Oppen combination method | ||
| * Proof search | * Proof search | ||
| + | |||
| ===== Basic idea of Nelson-Oppen combination ===== | ===== Basic idea of Nelson-Oppen combination ===== | ||
| Line 87: | Line 88: | ||
| The models can be merged if \\ | The models can be merged if \\ | ||
| (1)the domains are of the same size, and \\ | (1)the domains are of the same size, and \\ | ||
| - | (2)[x = y]_m1 --> [f(x) = f(y]_m2, where f is an isomorphism from one model to the other. | + | (2)[x = y]_m1 --> [f(x) = f(y)]_m2, where f is an isomorphism from one model to the other. |
| Line 143: | Line 144: | ||
| * Basic idea, and in the above example (name i from the ∃i as i0, then instantiate ∀i also with i=i0) | * Basic idea, and in the above example (name i from the ∃i as i0, then instantiate ∀i also with i=i0) | ||
| - | * examples of incompleteness: | + | * example: |
| Given: f(0) > 0 & ∀x:x > 0. (f(x)>0) --> f(x+1)>0 | Given: f(0) > 0 & ∀x:x > 0. (f(x)>0) --> f(x+1)>0 | ||
| + | |||
| Prove: ∀x. (x >= 0) --> f(x+1)>0 | Prove: ∀x. (x >= 0) --> f(x+1)>0 | ||
| + | |||
| Proof: | Proof: | ||
| - | * f(5) > 0 | + | * f(5) > 0\\ |
| f(5): can be derived by deriving f(1), f(2), f(3) and f(4). | f(5): can be derived by deriving f(1), f(2), f(3) and f(4). | ||
| * Then its straightforward to use ∀x:x > 0. (f(x)>0) --> f(x+1)>0 and arrive at the proof. | * Then its straightforward to use ∀x:x > 0. (f(x)>0) --> f(x+1)>0 and arrive at the proof. | ||
| For formulas with quantifiers, example: (∀x.F1) & F2, substitute values for x in F1. | For formulas with quantifiers, example: (∀x.F1) & F2, substitute values for x in F1. | ||
| + | |||
| A heuristic that could be used is: Look at constants in F2 and try substituting them. | A heuristic that could be used is: Look at constants in F2 and try substituting them. | ||
| Line 166: | Line 170: | ||
| For more details, see [[http://verify.stanford.edu/summerschool2004|Combination of Decision Procedures Summer School 2004]]. | For more details, see [[http://verify.stanford.edu/summerschool2004|Combination of Decision Procedures Summer School 2004]]. | ||
| - | |||
| ===== The notion of formal proof ===== | ===== The notion of formal proof ===== | ||
| Line 176: | Line 179: | ||
| Notion of formal proof. | Notion of formal proof. | ||
| - | How do we define a prove in a program? | + | How do we define a proof in a program? |
| - | * Set of axiomes: Ax_1, Ax_2, ..., Ax_n | + | * Set of axioms: Ax_1, Ax_2, ..., Ax_n |
| * Set of inference rules | * Set of inference rules | ||
| - | A prouve then is nothing more than a sequence of formulas F_i. | + | A proof then is nothing more than a sequence of formulas F_i. |
| - | __Informal Definition:__ A prove is such that each F_i can be derived either from an axiom or | + | __Informal Definition:__ A proof is such that each F_i can be derived either from an axiom or |
| from a rule or from a formula F_j (j < i) that we have previously derived. | from a rule or from a formula F_j (j < i) that we have previously derived. | ||
| Line 189: | Line 192: | ||
| Proof rules for first-order logic. | Proof rules for first-order logic. | ||
| * propositional axioms: an instance of propositional tautology is an axiom | * propositional axioms: an instance of propositional tautology is an axiom | ||
| - | * instantiation: from (ALL x.F) derive F[x:=t]. | + | * instantiation: from (∀x.F) derive F[x:=t]. |
| - | * generalization: after proving F which contains a fresh variable x, conclude (ALL x.F) | + | * generalization: after proving F which contains a fresh variable x, conclude (∀x.F) |
| Example: axiomatizing some set operations. | Example: axiomatizing some set operations. | ||