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]
@@ Line 1: / Line 1: @@
-====== Deriving Propositional Resolution ======
-We next consider proof rules for checking [[Satisfiability of Sets of Formulas]].
-We are extending the notion of [[Substitution Theorems for Propositional Logic|substitution on formulas]] to sets of formulas by
-\[
-    subst(\sigma,S) = \{ subst(\sigma,F) \mid F \in S \}
-\]
-To make intuition clearer, we will next use quantification over potentially infinitely many variables and conjunctions over infinitely many formulas.
-===== Proof System Based on Projecting Variables =====
-We first derive a more abstract proof system and that show that resolution is a special case of it.
-==== Key Idea ====
-The condition that $S$ is satisfiable is equivalent to the truth of
-\[
-  \exists p_1,p_2,p_3,\ldots.\ \bigwedge_{F \in S} F
-\]
-which, by changing the order of quantifiers, is:
-\[
-  \exists p_2,p_3,\ldots.\ \exists p_1. \bigwedge_{F \in S} F
-\]
-By expanding existential quantifier, $\exists p_1. \bigwedge_{F \in S} F$ is eqivalent to
-\[
-    ((\bigwedge_{F \in S} subst(p_1 \mapsto {\it false},F)) \lor
-    (\bigwedge_{F \in S} subst(p_1 \mapsto {\it true},F))
-\]
-which, by distributivity of $\lor$ through $\land$ is:
-\[
-    \bigwedge_{F_1,F_2 \in S}
-     (subst(p_1 \mapsto {\it false},F_1) \lor
-      subst(p_1 \mapsto {\it true},F_2))
-\]
-Let
-\[
-   ProjectForm(F_1,F_2,p) = (subst(p \mapsto {\it false},F_1) \lor
-                        (subst(p \mapsto {\it true},F_2))
-\]
-Then we conclude that $\exists p. S$ is equivalent to $ProjectSet(S,p)$ defined by
-\[
-   ProjectSet(S,p) = \{ ProjectForm(F_1,F_2,p) \mid F_1,F_2 \in S \}
-\]
-==== Projection Proof Rules ====
-Th justified the use of $ProjectForm(F_1,F_2,p)$ as an inference rule.  We write such rule:
-\[
-\frac{F_1 \; \ F_2}
-     {(subst(p \mapsto {\it false},F_1) \lor
-      (subst(p \mapsto {\it true},F_2))}
-\]
-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"
-\[
-\frac{F}
-{{\it false}}
-\]
-where $F$ is formula that has no variables and that evaluates to //false// (ground contradictory formula).  This rule is trivially sound.
-==== 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}
-   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}\]
-==== Completeness of Projection Rules ====
-We wish to show that projection rules are a sound and complete approach for checking satisfiability of finite and infinite sets formulas.  More precisely:
-  * if we can derive //false// from $S$ using projection rules, then $S$ is unsatisfiable
-  * if $S$ is unsatisfiable, then we can derive //false// using projection rules
-Because we can derive //false// precisely when we have a ground false formula, these statements become:
-  * if ${\it false} \in P^*(S)$ then $S$ is not satisfiable
-  * if $S$ is not satisfiable then ${\it false} \in P^*(S)$
-The first statement follows from soundness of projection rules.  We next prove the second statement.
-Suppose that it ${\it false} \notin P^*(S)$.  We claim that $S$ is satisfiable.  We show that every finite set is satisfiable, so the property will follow from the [[Compactness Theorem]].
-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
-\[
-    A = \bigcup_{i=1}^M P_i(S)
-\]
-By definition of $P_i$, we can show that the set $A$ contains the conjunctive normal form of the expansion of
-\[
-    \exists p_1,\ldots,p_M. (F_1 \land \ldots \land F_n)
-\]
-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.
-==== Improvement: Subsumption Rules ====
-Note also that if $\models (F \rightarrow G)$, where $F$ has been derived before, and $FV(G) \subseteq FV(F)$, then deriving $G$ does not help derive a ground contradiction, because the contradiction would also be derived using $F$.  If we derive such formula, we can immediately delete it so that it does not slow us down.
-In particular, a ground true formula can be deleted.
-===== Resolution as Projection =====
-Recall [[Definition of Propositional Resolution]].
-Instead of arbitrary formulas, use clauses as sets of literals.  The projection rule becomes
-\[
-\frac{C_1 \; \ C_2}
-     {(subst(p \mapsto {\it false},C_1) \cup
-      (subst(p \mapsto {\it true},C_2))}
-\]
-If $C$ is a clause, then
-\[
-   subst(\{p \mapsto {\it false}\},C)
-\]
-++++
-is equivalent to
-|
-\[
-\left\{\begin{array}{l}
-  C \setminus \{p\}, \ \ p \in C \\
-  true, \ \ \lnot p \in C \\
-  C, \mbox{ otherwise}
-\end{array}\right.
-\]
-++++
-There are several cases:
-  * if $p \notin C_1$ ++then| the result is subsumed by $C_1$, so it can be deleted++
-  * if $\lnot p \notin C_2$ ++then| the result is subsumed by $C_2$, so it can be deleted++
-  * if $p \in C_1$ and $(\lnot p) \in C_2$, ++then | the result is equivalent to$(C_1 \setminus \{p\}) \cup (C_2 \setminus \{\lnot p\})$, as given by the resolution rule++
-Therefore, for clauses, projection (with some elimination of redundant conclusions) is exactly the resolution proof rule.