Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:normal_forms_for_first-order_logic [2009/05/14 15:44] 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): | ||
| - | \[ | + | \begin{equation*} |
| \begin{array}{l@{}l} | \begin{array}{l@{}l} | ||
| \lnot \bigg( \big( & (\forall x. \exists y.\ R(x,y))\ \land \\ | \lnot \bigg( \big( & (\forall x. \exists y.\ R(x,y))\ \land \\ | ||
| Line 26: | Line 26: | ||
| & \rightarrow \forall x. \exists y.\ R(x,y) \land P(y) \bigg) | & \rightarrow \forall x. \exists y.\ R(x,y) \land P(y) \bigg) | ||
| \end{array} | \end{array} | ||
| - | \] | + | \end{equation*} |
| We will first consider a range of techniques that allow us to convert such formula to simpler normal forms. | We will first consider a range of techniques that allow us to convert such formula to simpler normal forms. | ||
| Line 83: | Line 83: | ||
| \end{array} | \end{array} | ||
| \] | \] | ||
| - | |||
| - | |||
| - | |||
| - | |||
| Line 127: | Line 123: | ||
| \[ | \[ | ||
| \begin{array}{l@{}l} | \begin{array}{l@{}l} | ||
| - | & (\forall x_1. R(x_1,g(x_1)))\ \land \\ | + | & (\forall x. R(x,g(x)))\ \land \\ |
| - | & (\forall z.\ \neg R(x_2,y_2) \lor R(a,f(b,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(c,y_4) \vee \neg P(y_4)) | + | & (\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 153: | Line 150: | ||
| === 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,y) \vee \neg P(y)$ |
| === Another Example: Irreflexive Dense Linear Orders === | === Another Example: Irreflexive Dense Linear Orders === | ||
| Line 179: | Line 175: | ||
| \end{array} | \end{array} | ||
| \] | \] | ||
| + | |||