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 | ||
|
sav08:proof_theory_for_propositional_logic [2008/03/06 16:04] vkuncak |
sav08:proof_theory_for_propositional_logic [2008/03/09 19:43] vkuncak |
||
|---|---|---|---|
| Line 3: | Line 3: | ||
| ===== Notion of a proof system ==== | ===== Notion of a proof system ==== | ||
| - | Deriving formulas from zero or more other formulas. | + | A set of proof rules, each of which specifies how to derive a formula from zero or more other formulas. |
| - | * Typical requirement: polynomial-time algorithm to check rule application. | + | * Typical requirement: polynomial-time algorithm to check whether a rule application is valid according to the rule system |
| We write $\vdash_S F$ if we can derive formula in some proof system $S$. We omit $S$ when it is clear. | We write $\vdash_S F$ if we can derive formula in some proof system $S$. We omit $S$ when it is clear. | ||
| Line 48: | Line 48: | ||
| ===== Resolution ===== | ===== Resolution ===== | ||
| - | Definition and soundness. | + | Definition and soundness. Completeness in next lecture. |
| + | |||