# 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) Both sides previous revision Previous revision 2012/05/01 12:26 vkuncak 2008/03/19 17:18 tatjana 2008/03/19 17:15 tatjana 2008/03/19 17:13 tatjana 2008/03/19 17:12 tatjana 2008/03/18 02:00 tatjana 2008/03/12 12:58 vkuncak 2008/03/12 11:04 vkuncak 2008/03/12 11:03 vkuncak 2008/03/12 11:02 vkuncak 2008/03/11 23:08 vkuncak 2008/03/11 23:06 vkuncak 2008/03/11 19:52 vkuncak 2008/03/11 19:51 vkuncak 2008/03/11 19:44 vkuncak 2008/03/11 19:44 vkuncak 2008/03/11 19:43 vkuncak 2008/03/11 19:37 vkuncak 2008/03/11 16:48 vkuncak 2008/03/11 16:47 vkuncak 2008/03/10 20:31 vkuncak 2008/03/10 20:27 vkuncak 2008/03/10 20:25 vkuncak 2008/03/10 20:24 vkuncak 2008/03/10 20:22 vkuncak 2008/03/10 20:21 vkuncak 2008/03/10 20:09 vkuncak Next revision Previous revision 2012/05/01 12:26 vkuncak 2008/03/19 17:18 tatjana 2008/03/19 17:15 tatjana 2008/03/19 17:13 tatjana 2008/03/19 17:12 tatjana 2008/03/18 02:00 tatjana 2008/03/12 12:58 vkuncak 2008/03/12 11:04 vkuncak 2008/03/12 11:03 vkuncak 2008/03/12 11:02 vkuncak 2008/03/11 23:08 vkuncak 2008/03/11 23:06 vkuncak 2008/03/11 19:52 vkuncak 2008/03/11 19:51 vkuncak 2008/03/11 19:44 vkuncak 2008/03/11 19:44 vkuncak 2008/03/11 19:43 vkuncak 2008/03/11 19:37 vkuncak 2008/03/11 16:48 vkuncak 2008/03/11 16:47 vkuncak 2008/03/10 20:31 vkuncak 2008/03/10 20:27 vkuncak 2008/03/10 20:25 vkuncak 2008/03/10 20:24 vkuncak 2008/03/10 20:22 vkuncak 2008/03/10 20:21 vkuncak 2008/03/10 20:09 vkuncak 2008/03/10 19:59 vkuncak 2008/03/10 19:47 vkuncak 2008/03/10 19:37 vkuncak 2008/03/10 19:27 vkuncak 2008/03/10 19:06 vkuncak 2008/03/10 19:04 vkuncak 2008/03/10 19:03 vkuncak 2008/03/10 18:52 vkuncak 2008/03/10 18:50 vkuncak 2008/03/10 18:36 vkuncak 2008/03/10 18:33 vkuncak 2008/03/10 18:33 vkuncak 2008/03/10 18:17 vkuncak 2008/03/10 18:17 vkuncak 2008/03/10 18:09 vkuncak created Line 4: Line 4: We are extending the notion of [[Substitution Theorems for Propositional Logic|substitution on formulas]] to sets of formulas by 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 \} 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. 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 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 \exists p_1,​p_2,​p_3,​\ldots.\ \bigwedge_{F \in S} F -$ + \end{equation*} which, by changing the order of quantifiers,​ is: which, by changing the order of quantifiers,​ is: - $+ \begin{equation*} \exists p_2,​p_3,​\ldots.\ \exists p_1. \bigwedge_{F \in S} F \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 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 false},F)) \lor (\bigwedge_{F \in S} subst(p_1 \mapsto {\it true},F)) (\bigwedge_{F \in S} subst(p_1 \mapsto {\it true},F)) -$ + \end{equation*} which, by distributivity of $\lor$ through $\land$ is: which, by distributivity of $\lor$ through $\land$ is: - $+ \begin{equation*} \bigwedge_{F_1,​F_2 \in S} \bigwedge_{F_1,​F_2 \in S} ​(subst(p_1 \mapsto {\it false},F_1) \lor ​(subst(p_1 \mapsto {\it false},F_1) \lor subst(p_1 \mapsto {\it true},F_2)) subst(p_1 \mapsto {\it true},F_2)) -$ + \end{equation*} Let Let - $+ \begin{equation*} ​ProjectForm(F_1,​F_2,​p) = (subst(p \mapsto {\it false},F_1) \lor ​ProjectForm(F_1,​F_2,​p) = (subst(p \mapsto {\it false},F_1) \lor (subst(p \mapsto {\it true},F_2)) (subst(p \mapsto {\it true},F_2)) -$ + \end{equation*} Then we conclude that $\exists p. S$ is equivalent to $ProjectSet(S,​p)$ defined by 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 \} ​ProjectSet(S,​p) = \{ ProjectForm(F_1,​F_2,​p) \mid F_1,F_2 \in S \} -$ + \end{equation*} ==== Projection Proof Rules ==== ==== 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} \frac{F_1 \; \ F_2} ​{(subst(p \mapsto {\it false},F_1) \lor ​{(subst(p \mapsto {\it false},F_1) \lor (subst(p \mapsto {\it true},​F_2))} (subst(p \mapsto {\it true},​F_2))} -$ + \end{equation*} The soundness of projection rule follows from the fact that 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)$. 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" Applying the projection rule we obtain formulas with fewer and fewer variables. ​ We therefore also add the "​ground contradiction rule" - $+ \begin{equation*} \frac{F} \frac{F} {{\it false}} {{\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 ==== ==== 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^*$: 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_0(S) = S \\ ​P_{n+1}(S) = ProjectSet(P_n(S),​p_{n+1}) \\ ​P_{n+1}(S) = ProjectSet(P_n(S),​p_{n+1}) \\ ​P^*(S) = \bigcup_{n \geq 0} P_n(S) ​P^*(S) = \bigcup_{n \geq 0} P_n(S) - \end{array}$ + \end{array}\end{equation*} - + ==== Completeness of Projection Rules ==== ==== 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 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) 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 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) \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. 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 Instead of arbitrary formulas, use clauses as sets of literals. ​ The projection rule becomes - $+ \begin{equation*} \frac{C_1 \; \ C_2} \frac{C_1 \; \ C_2} ​{(subst(p \mapsto {\it false},C_1) \cup ​{(subst(p \mapsto {\it false},C_1) \cup (subst(p \mapsto {\it true},​C_2))} (subst(p \mapsto {\it true},​C_2))} -$ + \end{equation*} If $C$ is a clause, then If $C$ is a clause, then - $+ \begin{equation*} ​subst(\{p \mapsto {\it false}\},C) ​subst(\{p \mapsto {\it false}\},C) -$ + \end{equation*} ++++ ++++ is equivalent to is equivalent to | | - $+ \begin{equation*} \left\{\begin{array}{l} \left\{\begin{array}{l} C \setminus \{p\}, \ \ p \in C \\ C \setminus \{p\}, \ \ p \in C \\ Line 129: Line 126: C, \mbox{ otherwise} C, \mbox{ otherwise} \end{array}\right. \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. Therefore, for clauses, projection (with some elimination of redundant conclusions) is exactly the resolution proof rule. +