# 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] (current) Both sides previous revision Previous revision 2008/03/11 16:38 vkuncak 2008/03/09 19:43 vkuncak 2008/03/06 19:44 vkuncak 2008/03/06 16:04 vkuncak 2008/03/06 12:29 vkuncak 2008/03/06 12:23 vkuncak 2008/03/06 12:18 vkuncak 2008/03/06 12:17 vkuncak 2008/03/06 12:10 vkuncak 2008/03/05 21:11 vkuncak 2008/03/05 21:11 vkuncak 2008/03/05 20:49 vkuncak created Next revision Previous revision 2008/03/11 16:38 vkuncak 2008/03/09 19:43 vkuncak 2008/03/06 19:44 vkuncak 2008/03/06 16:04 vkuncak 2008/03/06 12:29 vkuncak 2008/03/06 12:23 vkuncak 2008/03/06 12:18 vkuncak 2008/03/06 12:17 vkuncak 2008/03/06 12:10 vkuncak 2008/03/05 21:11 vkuncak 2008/03/05 21:11 vkuncak 2008/03/05 20:49 vkuncak created Line 15: Line 15: System $S$ is sound if for every formula $F$, System $S$ is sound if for every formula $F$, - $+ \begin{equation*} (\vdash_S F) \rightarrow (\models F) (\vdash_S F) \rightarrow (\models F) -$ + \end{equation*} We can only prove true formulas. We can only prove true formulas. Line 23: Line 23: System $S$ is complete if for every formula $F$, System $S$ is complete if for every formula $F$, - $+ \begin{equation*} (\models F) \rightarrow (\vdash F) (\models F) \rightarrow (\vdash F) -$ + \end{equation*} 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: + \begin{equation*} \frac{P\{p \mapsto {\it true}\}\ ;\ P\{p \mapsto {\it false}\}} \frac{P\{p \mapsto {\it true}\}\ ;\ P\{p \mapsto {\it false}\}} {P} {P} -$ + \end{equation*} - 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]]