Differences
This shows you the differences between two versions of the page.
sav08:proof_theory_for_propositional_logic [2008/03/09 19:43] vkuncak |
sav08:proof_theory_for_propositional_logic [2015/04/21 17:30] |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Proof Theory for Propositional Logic ====== | ||
- | |||
- | ===== Notion of a proof system ==== | ||
- | |||
- | 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 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. | ||
- | |||
- | Proof tree and proof sequences. | ||
- | |||
- | Proof complexity: given $F$ such that $\vdash_S F$, the size of smallest proof of $F$ in $S$. | ||
- | |||
- | ===== Soundness of a proof system ===== | ||
- | |||
- | System $S$ is sound if for every formula $F$, | ||
- | \[ | ||
- | (\vdash_S F) \rightarrow (\models F) | ||
- | \] | ||
- | We can only prove true formulas. | ||
- | |||
- | ===== Completeness of a proof system ===== | ||
- | |||
- | System $S$ is complete if for every formula $F$, | ||
- | \[ | ||
- | (\models F) \rightarrow (\vdash F) | ||
- | \] | ||
- | We can prove all valid formulas. | ||
- | |||
- | ===== Case analysis proof system ===== | ||
- | |||
- | A sound and complete proof system. | ||
- | |||
- | Case analysis rule: | ||
- | \[ | ||
- | \frac{P\{p \mapsto {\it true}\}\ ;\ P\{p \mapsto {\it false}\}} | ||
- | {P} | ||
- | \] | ||
- | |||
- | Evaluation rule: derive $P$ if $P$ has no variables and it evaluates to //true//. | ||
- | |||
- | Adding simplification rules. Adding sound rules preserves soundness and completeness. | ||
- | |||
- | ===== Gentzen proof system ===== | ||
- | |||
- | Recall Gentzen's proof system from [[proofs and induction]] part of [[lecture02]], ignoring rules for predicates and induction. | ||
- | |||
- | ===== Resolution ===== | ||
- | |||
- | Definition and soundness. Completeness in next lecture. | ||
- | |||