Lab for Automated Reasoning and Analysis 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] (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//.
  
-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]]
  
 
sav08/proof_theory_for_propositional_logic.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice