Differences
This shows you the differences between two versions of the page.
sav08:deriving_propositional_resolution [2008/03/19 17:13] 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) = Proj(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 follows 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. |