Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:deriving_propositional_resolution [2008/03/12 12:58] vkuncak |
sav08:deriving_propositional_resolution [2008/03/19 17:12] tatjana |
||
|---|---|---|---|
| Line 3: | Line 3: | ||
| We next consider proof rules for checking [[Satisfiability of Sets of Formulas]]. | 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 \} | subst(\sigma,S) = \{ subst(\sigma,F) \mid F \in S \} | ||
| 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 \} |
| \] | \] | ||