Lab for Automated Reasoning and Analysis 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/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