• English only

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 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.
+