Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:deriving_propositional_resolution [2008/03/19 17:12] tatjana |
sav08:deriving_propositional_resolution [2008/03/19 17:13] tatjana |
||
|---|---|---|---|
| Line 44: | Line 44: | ||
| 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 \} | ||
| \] | \] | ||
| + | |||
| ==== Projection Proof Rules ==== | ==== Projection Proof Rules ==== | ||
| Line 54: | Line 55: | ||
| \] | \] | ||
| 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 Proj(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" | ||