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/12 12:58] vkuncak |
sav08:deriving_propositional_resolution [2008/03/18 02:00] 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 \} |