Differences

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

--- sav08:deriving_propositional_resolution [2008/03/12 11:04]
vkuncak
+++ sav08:deriving_propositional_resolution [2008/03/12 12:58]
vkuncak
@@ Line 89: / Line 89: @@
     A = \bigcup_{i=1}^M P_i(S)
 \]
-By definition of $P_i$, we can show that the set $A$ contains the expansion of
+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)
 \]
-This expansion is a ground formula, so it evaluates to either //true// or //false//.  By assumption, $P^*(S)$ and therefore $A$ do not contain ground contradiction.  Therefore, $\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.
-==== Improvement: Simplification Rules ====
-Of course, we do not need to wait until we reach a ground contradiction.  Whenever we substitute variable with //true// or //false//, we can immediately simplify the formula using sound simplification rules.
-When we introduce simplifications we still manipulate equivalent formulas, so soundness and completeness remain the same.
 ==== Improvement: Subsumption Rules ====