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_5 [2007/04/03 17:35] vaibhav.rajan |
sav07_lecture_5 [2007/04/03 17:37] vaibhav.rajan |
||
---|---|---|---|
Line 166: | Line 166: | ||
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 175: | ||
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 188: | ||
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. |