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:normal_forms_for_first-order_logic [2009/05/14 15:59] 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): | ||
\[ | \[ | ||
Line 130: | Line 130: | ||
\] | \] | ||
Note: it is better to do PNF and SNF //for each conjunct independently//. | Note: it is better to do PNF and SNF //for each conjunct independently//. | ||
+ | |||
===== CNF and Sets of Clauses ===== | ===== CNF and Sets of Clauses ===== | ||
Line 152: | Line 153: | ||
*$C_2=\neg R(x,y) \lor R(x,f(y,z)))$ | *$C_2=\neg R(x,y) \lor R(x,f(y,z)))$ | ||
*$C_3=P(x) \lor P(f(x,a))$ | *$C_3=P(x) \lor P(f(x,a))$ | ||
- | *$C_4=\neg R(c,x) \vee \neg P(x)$ | + | *$C_4=\neg R(c,y) \vee \neg P(y)$ |
=== Another Example: Irreflexive Dense Linear Orders === | === Another Example: Irreflexive Dense Linear Orders === |