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/18 02:00]
tatjana
@@ Line 3: / Line 3: @@
 We next consider proof rules for checking [[Satisfiability of Sets of Formulas]].
-We 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
 \[
     subst(\sigma,S) = \{ subst(\sigma,F) \mid F \in S \}
@@ 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 ====