LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

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