Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
sav08:proof_theory_for_propositional_logic [2008/03/09 19:43] vkuncak |
sav08:proof_theory_for_propositional_logic [2008/03/11 16:38] vkuncak |
||
|---|---|---|---|
| Line 28: | Line 28: | ||
| We can prove all valid formulas. | We can prove all valid formulas. | ||
| - | ===== Case analysis proof system ===== | + | ===== Some Example Proof Systems ===== |
| - | A sound and complete proof system. | + | === Case analysis proof system === |
| - | Case analysis rule: | + | A simple A sound and complete proof system. |
| + | |||
| + | **Rule 1:** Case analysis rule: | ||
| \[ | \[ | ||
| \frac{P\{p \mapsto {\it true}\}\ ;\ P\{p \mapsto {\it false}\}} | \frac{P\{p \mapsto {\it true}\}\ ;\ P\{p \mapsto {\it false}\}} | ||
| Line 38: | Line 40: | ||
| \] | \] | ||
| - | Evaluation rule: derive $P$ if $P$ has no variables and it evaluates to //true//. | + | **Rule 2:** Evaluation rule: derive $P$ if $P$ has no variables and it evaluates to //true//. |
| - | Adding simplification rules. Adding sound rules preserves soundness and completeness. | + | We can also add simplification rules. Adding sound rules preserves soundness and completeness. |
| - | ===== Gentzen proof system ===== | + | === Gentzen proof system === |
| Recall Gentzen's proof system from [[proofs and induction]] part of [[lecture02]], ignoring rules for predicates and induction. | Recall Gentzen's proof system from [[proofs and induction]] part of [[lecture02]], ignoring rules for predicates and induction. | ||
| - | ===== Resolution ===== | + | === Resolution === |
| - | + | ||
| - | Definition and soundness. Completeness in next lecture. | + | |
| + | [[Definition of Propositional Resolution]] | ||