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:definition_of_propositional_resolution [2009/05/14 10:00]
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 42: Line 43:
      - application of the resolution rule produces no new clauses      - application of the resolution rule produces no new clauses
  
-**Example:​** prove a tautology from [[sav08:propositional_logic_informally|examples in this lecture]], e.g. +[[sav09:Example of Using Propositional Resolution]]
-\[ +
-    ((p \rightarrow q) \land\ ((\lnot p) \rightarrow r)) \leftrightarrow ((p \land q)\ \lor\ ((\lnot p) \land r)) +
-\]+
  
 ===== Soundness of Resolution Rule ===== ===== Soundness of Resolution Rule =====