Differences

This shows you the differences between two versions of the page.

--- sav08:deriving_propositional_resolution [2008/03/19 17:18]
tatjana
+++ sav08:deriving_propositional_resolution [2015/04/21 17:30] (current)
@@ Line 4: / Line 4: @@
 We are extending the notion of [[Substitution Theorems for Propositional Logic|substitution on formulas]] to sets of formulas by
-\[
+\begin{equation*}
     subst(\sigma,S) = \{ subst(\sigma,F) \mid F \in S \}
-\]
+\end{equation*}
 To make intuition clearer, we will next use quantification over potentially infinitely many variables and conjunctions over infinitely many formulas.
@@ Line 17: / Line 17: @@
 The condition that $S$ is satisfiable is equivalent to the truth of
-\[
+\begin{equation*}
   \exists p_1,p_2,p_3,\ldots.\ \bigwedge_{F \in S} F
-\]
+\end{equation*}
 which, by changing the order of quantifiers, is:
-\[
+\begin{equation*}
   \exists p_2,p_3,\ldots.\ \exists p_1. \bigwedge_{F \in S} F
-\]
+\end{equation*}
 By expanding existential quantifier, $\exists p_1. \bigwedge_{F \in S} F$ is eqivalent to
-\[
+\begin{equation*}
     ((\bigwedge_{F \in S} subst(p_1 \mapsto {\it false},F)) \lor
     (\bigwedge_{F \in S} subst(p_1 \mapsto {\it true},F))
-\]
+\end{equation*}
 which, by distributivity of $\lor$ through $\land$ is:
-\[
+\begin{equation*}
     \bigwedge_{F_1,F_2 \in S}
      (subst(p_1 \mapsto {\it false},F_1) \lor
       subst(p_1 \mapsto {\it true},F_2))
-\]
+\end{equation*}
 Let
-\[
+\begin{equation*}
    ProjectForm(F_1,F_2,p) = (subst(p \mapsto {\it false},F_1) \lor
                         (subst(p \mapsto {\it true},F_2))
-\]
+\end{equation*}
 Then we conclude that $\exists p. S$ is equivalent to $ProjectSet(S,p)$ defined by
-\[
+\begin{equation*}
    ProjectSet(S,p) = \{ ProjectForm(F_1,F_2,p) \mid F_1,F_2 \in S \}
-\]
+\end{equation*}
 ==== Projection Proof Rules ====
-Th justified the use of $ProjectForm(F_1,F_2,p)$ as an inference rule.  We write such rule:
+Above we justified the use of $ProjectForm(F_1,F_2,p)$ as an inference rule.  We write such rule:
-\[
+\begin{equation*}
 \frac{F_1 \; \ F_2}
      {(subst(p \mapsto {\it false},F_1) \lor
       (subst(p \mapsto {\it true},F_2))}
-\]
+\end{equation*}
 The soundness of projection rule follows from the fact that
 for every interpretation $I$, if $I \models S$, then also $I \models ProjectSet(S,p)$.
 Applying the projection rule we obtain formulas with fewer and fewer variables.  We therefore also add the "ground contradiction rule"
-\[
+\begin{equation*}
 \frac{F}
 {{\it false}}
-\]
+\end{equation*}
-where $F$ is formula that has no variables and that evaluates to //false// (ground contradictory formula).  This rule is trivially sound.
+where $F$ is formula that has no variables and that evaluates to //false// (ground contradictory formula).  This rule is trivially sound: we can never
+have a model of a ground formula that evaluates to false.
 ==== Iterating Rule Application ====
 Given some enumeration $p_1,p_2,\ldots$ of propositional variables in $S$, we define the notion of applying projection along all propositional variables, denoted $P^*$:
-\[\begin{array}{l}
+\begin{equation*}\begin{array}{l}
    P_0(S) = S \\
    P_{n+1}(S) = ProjectSet(P_n(S),p_{n+1}) \\
    P^*(S) = \bigcup_{n \geq 0} P_n(S)
-\end{array}\]
+\end{array}\end{equation*}
 ==== Completeness of Projection Rules ====
@@ Line 90: / Line 87: @@
 Consider any finite $T \subseteq S$.  We show that $T$ it is satisfiable.  Let $T = \{F_1,\ldots,F_n\}$ and let $FV(F_1) \cup \ldots \cup FV(F_n) \subseteq \{p_1,\ldots,p_M\}$.  Consider the set
-\[
+\begin{equation*}
     A = \bigcup_{i=1}^M P_i(S)
-\]
+\end{equation*}
 By definition of $P_i$, we can show that the set $A$ contains the conjunctive normal form of the expansion of
-\[
+\begin{equation*}
     \exists p_1,\ldots,p_M. (F_1 \land \ldots \land F_n)
-\]
+\end{equation*}
 Each of these conjuncts is a ground formula (all variables $p_1,\ldots,p_M$ have been instantiated), so the formula evaluates to either //true// or //false//.  By assumption, $P^*(S)$ and therefore $A$ do not contain a ground contradiction.  Therefore, each conjunct of $\exists p_1,\ldots,p_M. (F_1 \land \ldots \land F_n)$ is true and $T$ is satisfiable.
@@ Line 110: / Line 107: @@
 Instead of arbitrary formulas, use clauses as sets of literals.  The projection rule becomes
-\[
+\begin{equation*}
 \frac{C_1 \; \ C_2}
      {(subst(p \mapsto {\it false},C_1) \cup
       (subst(p \mapsto {\it true},C_2))}
-\]
+\end{equation*}
 If $C$ is a clause, then
-\[
+\begin{equation*}
    subst(\{p \mapsto {\it false}\},C)
-\]
+\end{equation*}
 ++++
 is equivalent to
 |
-\[
+\begin{equation*}
 \left\{\begin{array}{l}
   C \setminus \{p\}, \ \ p \in C \\
@@ Line 129: / Line 126: @@
   C, \mbox{ otherwise}
 \end{array}\right.
-\]
+\end{equation*}
 ++++
@@ Line 138: / Line 135: @@
 Therefore, for clauses, projection (with some elimination of redundant conclusions) is exactly the resolution proof rule.