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:58] vkuncak |
sav08:normal_forms_for_first-order_logic [2009/05/14 16:02] vkuncak |
||
|---|---|---|---|
| Line 83: | Line 83: | ||
| \end{array} | \end{array} | ||
| \] | \] | ||
| + | |||
| ===== Skolem Normal Form ===== | ===== Skolem Normal Form ===== | ||
| Line 125: | Line 126: | ||
| & (\forall x.\forall y. \forall z.\ \neg R(x,y) \lor R(x,f(y,z)))\ \land \\ | & (\forall x.\forall y. \forall z.\ \neg R(x,y) \lor R(x,f(y,z)))\ \land \\ | ||
| & (\forall x.\ P(x) \lor P(f(x,a)))\ \land \\ | & (\forall x.\ P(x) \lor P(f(x,a)))\ \land \\ | ||
| - | & (\forall x.\ \neg R(c,x) \vee \neg P(x)) | + | & (\forall y.\ \neg R(c,y) \vee \neg P(y)) |
| \end{array} | \end{array} | ||
| \] | \] | ||
| 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 151: | 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 === | ||