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:41] vkuncak |
sav08:normal_forms_for_first-order_logic [2009/05/14 15:58] vkuncak |
||
---|---|---|---|
Line 83: | Line 83: | ||
\end{array} | \end{array} | ||
\] | \] | ||
- | |||
- | |||
- | |||
===== Skolem Normal Form ===== | ===== Skolem Normal Form ===== | ||
Line 125: | Line 122: | ||
\[ | \[ | ||
\begin{array}{l@{}l} | \begin{array}{l@{}l} | ||
- | & (\forall x_1. R(x_1,f_{y_1}(x_1)))\ \land \\ | + | & (\forall x. R(x,g(x)))\ \land \\ |
- | & (\exists x_2. \exists y_2.\ \forall z.\ \neg R(x_2,y_2) \lor R(x_2,f(y_2,z)))\ \land \\ | + | & (\forall x.\forall y. \forall z.\ \neg R(x,y) \lor R(x,f(y,z)))\ \land \\ |
- | & (\forall x_3.\ P(x_3) \lor P(f(x_3,a)))\ \land \\ | + | & (\forall x.\ P(x) \lor P(f(x,a)))\ \land \\ |
- | & (\forall y_4.\ \neg R(f_4,y_4) \vee \neg P(y_4)) | + | & (\forall x.\ \neg R(c,x) \vee \neg P(x)) |
\end{array} | \end{array} | ||
\] | \] | ||
Line 151: | Line 148: | ||
=== Clauses for Example === | === Clauses for Example === | ||
- | *$C_1=R(x_1,f_{y_1}(x_1))$ | + | *$C_1=R(x,g(x))$ |
- | *$C_2=\neg R(x_2,y_2) \lor R(x_2,f(y_2,z)))$ | + | *$C_2=\neg R(x,y) \lor R(x,f(y,z)))$ |
- | *$C_3=P(x_3) \lor P(f(x_3,a))$ | + | *$C_3=P(x) \lor P(f(x,a))$ |
- | *$C_4=\neg R(f_4,y_4) \vee \neg P(y_4)$ | + | *$C_4=\neg R(c,x) \vee \neg P(x)$ |
=== Another Example: Irreflexive Dense Linear Orders === | === Another Example: Irreflexive Dense Linear Orders === | ||
Line 177: | Line 173: | ||
\end{array} | \end{array} | ||
\] | \] | ||
+ |