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. |
+ |