Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
sav08:deriving_propositional_resolution [2008/03/19 17:18] tatjana |
sav08:deriving_propositional_resolution [2012/05/01 12:26] vkuncak |
||
---|---|---|---|
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 ==== | ||
- | Th justified the use of $ProjectForm(F_1,F_2,p)$ as an inference rule. We write such rule: | + | Above we justified the use of $ProjectForm(F_1,F_2,p)$ as an inference rule. We write such rule: |
\[ | \[ | ||
\frac{F_1 \; \ F_2} | \frac{F_1 \; \ F_2} | ||
Line 62: | Line 61: | ||
{{\it false}} | {{\it false}} | ||
\] | \] | ||
- | 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: we can never |
+ | have a model of a ground formula that evaluates to false. | ||
==== Iterating Rule Application ==== | ==== Iterating Rule Application ==== | ||
Line 73: | Line 72: | ||
P^*(S) = \bigcup_{n \geq 0} P_n(S) | P^*(S) = \bigcup_{n \geq 0} P_n(S) | ||
\end{array}\] | \end{array}\] | ||
- | |||
- | |||
==== Completeness of Projection Rules ==== | ==== Completeness of Projection Rules ==== | ||
Line 138: | Line 135: | ||
Therefore, for clauses, projection (with some elimination of redundant conclusions) is exactly the resolution proof rule. | Therefore, for clauses, projection (with some elimination of redundant conclusions) is exactly the resolution proof rule. | ||
+ |