LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision 		Previous revision
sav08:proof_theory_for_propositional_logic [2008/03/06 12:23]
vkuncak 		sav08:proof_theory_for_propositional_logic [2008/03/11 16:38]
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.
 +
 +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 =====  ===== Soundness of a proof system ===== 
Line 24: Line 28:
 We can prove all valid formulas. We can prove all valid formulas.
  
-===== Case analysis proof system ​=====+===== Some Example Proof Systems ===== 
 + 
 +=== Case analysis proof system ===
  
-A sound and complete proof system.+A simple ​A sound and complete proof system.
  
-Case analysis rule:+**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 34: Line 40:
 \] \]
  
-Evaluation rule: derive $P$ if $P$ has no variables and it evaluates to {\it 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.+[[Definition ​of Propositional Resolution]]