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:definition_of_propositional_resolution [2009/05/14 10:38]
vkuncak
sav08:definition_of_propositional_resolution [2015/04/21 17:30] (current)
Line 18: Line 18:
 Viewing clauses as sets, propositional resolution is the following rule: Viewing clauses as sets, propositional resolution is the following rule:
  
-\[+\begin{equation*}
 \frac{C \cup \{\lnot p\}\ \ \ D \cup \{p\}} \frac{C \cup \{\lnot p\}\ \ \ D \cup \{p\}}
      {C \cup D}      {C \cup D}
-\]+\end{equation*}
  
 Here $C,D$ are clauses and $p \in V$ is a propositional variable. Here $C,D$ are clauses and $p \in V$ is a propositional variable.
  
 Intuition: consider equivalent formulas Intuition: consider equivalent formulas
-\[+\begin{equation*}
 \frac{((\lnot C) \rightarrow (\lnot p))\ \ \ ((\lnot p) \rightarrow D)} \frac{((\lnot C) \rightarrow (\lnot p))\ \ \ ((\lnot p) \rightarrow D)}
      ​{(\lnot C) \rightarrow D}      ​{(\lnot C) \rightarrow D}
-\]+\end{equation*}
  
  
Line 43: Line 43:
      - application of the resolution rule produces no new clauses      - application of the resolution rule produces no new clauses
  
-[[Example of Using Propositional Resolution]]+[[sav09:Example of Using Propositional Resolution]]
  
 ===== Soundness of Resolution Rule ===== ===== Soundness of Resolution Rule =====
 
sav08/definition_of_propositional_resolution.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice