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:normal_forms_for_first-order_logic [2009/05/14 16:02] vkuncak |
sav08:normal_forms_for_first-order_logic [2015/02/16 10:36] vkuncak |
||
|---|---|---|---|
| Line 10: | Line 10: | ||
| Consider this formula in ${\cal L}$: | Consider this formula in ${\cal L}$: | ||
| - | \[ | + | \begin{equation} |
| \begin{array}{l@{}l} | \begin{array}{l@{}l} | ||
| & (\forall x. \exists y.\ R(x,y))\ \land \\ | & (\forall x. \exists y.\ R(x,y))\ \land \\ | ||
| Line 17: | Line 17: | ||
| & \rightarrow \forall x. \exists y.\ R(x,y) \land P(y) | & \rightarrow \forall x. \exists y.\ R(x,y) \land P(y) | ||
| \end{array} | \end{array} | ||
| - | \] | + | \end{equation} |
| We are interested in checking the //validity// of this formula (is it true in all interpretations). We will check the //satisfiability// of the negation of this formula (does it have a model): | We are interested in checking the //validity// of this formula (is it true in all interpretations). We will check the //satisfiability// of the negation of this formula (does it have a model): | ||
| \[ | \[ | ||