# 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 Go 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 Go 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]]
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 2, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "math_score": 0.769097089767456, "perplexity": 11651.812603492224}, "config": {"markdown_headings": true, "markdown_code": false, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "warc_path": "s3://commoncrawl/crawl-data/CC-MAIN-2019-47/segments/1573496669795.59/warc/CC-MAIN-20191118131311-20191118155311-00284.warc.gz"}