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/18 02:00] tatjana |
sav08:deriving_propositional_resolution [2008/03/19 17:12] tatjana |
||
---|---|---|---|
Line 12: | Line 12: | ||
We first derive a more abstract proof system and that show that resolution is a special case of it. | We first derive a more abstract proof system and that show that resolution is a special case of it. | ||
+ | |||
==== Key Idea ==== | ==== Key Idea ==== | ||
Line 41: | Line 42: | ||
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 | ||
\[ | \[ | ||
- | Proj(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 \} |
\] | \] | ||