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:13] tatjana |
sav08:deriving_propositional_resolution [2008/03/19 17:15] tatjana |
||
|---|---|---|---|
| Line 63: | Line 63: | ||
| \] | \] | ||
| 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. | ||
| + | |||
| ==== Iterating Rule Application ==== | ==== Iterating Rule Application ==== | ||
| Line 69: | Line 70: | ||
| \[\begin{array}{l} | \[\begin{array}{l} | ||
| P_0(S) = S \\ | P_0(S) = S \\ | ||
| - | P_{n+1}(S) = Proj(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}\] | ||