• English only

# 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)
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//.

-===== 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]]