# Differences

This shows you the differences between two versions of the page.

 sav08:normal_forms_for_first-order_logic [2015/02/16 10:36]vkuncak sav08:normal_forms_for_first-order_logic [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2015/02/16 10:36 vkuncak 2015/02/16 10:36 vkuncak 2009/05/14 16:02 vkuncak 2009/05/14 15:59 vkuncak 2009/05/14 15:58 vkuncak 2009/05/14 15:44 vkuncak 2009/05/14 15:43 vkuncak 2009/05/14 15:41 vkuncak 2009/05/14 15:37 vkuncak 2009/05/14 15:32 vkuncak 2009/05/14 15:30 vkuncak 2009/05/14 13:34 vkuncak 2008/04/01 16:55 giuliano 2008/04/01 16:54 giuliano 2008/04/01 16:40 giuliano 2008/04/01 16:10 giuliano 2008/04/01 16:09 giuliano 2008/04/01 12:04 vkuncak 2008/04/01 12:04 vkuncak 2008/04/01 12:02 vkuncak 2008/04/01 12:00 vkuncak 2008/04/01 11:30 vkuncak 2008/03/28 16:28 giuliano 2008/03/28 16:05 giuliano 2008/03/28 15:54 giuliano 2008/03/28 15:48 giuliano 2008/03/20 10:29 vkuncak Next revision Previous revision 2015/02/16 10:36 vkuncak 2015/02/16 10:36 vkuncak 2009/05/14 16:02 vkuncak 2009/05/14 15:59 vkuncak 2009/05/14 15:58 vkuncak 2009/05/14 15:44 vkuncak 2009/05/14 15:43 vkuncak 2009/05/14 15:41 vkuncak 2009/05/14 15:37 vkuncak 2009/05/14 15:32 vkuncak 2009/05/14 15:30 vkuncak 2009/05/14 13:34 vkuncak 2008/04/01 16:55 giuliano 2008/04/01 16:54 giuliano 2008/04/01 16:40 giuliano 2008/04/01 16:10 giuliano 2008/04/01 16:09 giuliano 2008/04/01 12:04 vkuncak 2008/04/01 12:04 vkuncak 2008/04/01 12:02 vkuncak 2008/04/01 12:00 vkuncak 2008/04/01 11:30 vkuncak 2008/03/28 16:28 giuliano 2008/03/28 16:05 giuliano 2008/03/28 15:54 giuliano 2008/03/28 15:48 giuliano 2008/03/20 10:29 vkuncak 2008/03/20 10:28 vkuncak 2008/03/20 10:20 vkuncak 2008/03/19 22:12 vkuncak 2008/03/19 21:19 vkuncak 2008/03/19 21:17 vkuncak 2008/03/19 21:15 vkuncak 2008/03/19 21:14 vkuncak 2008/03/19 18:25 vkuncak 2008/03/19 18:22 vkuncak 2008/03/19 18:19 vkuncak 2008/03/19 10:11 vkuncak 2008/03/19 10:10 vkuncak 2008/03/19 10:08 vkuncak 2008/03/19 10:06 vkuncak 2008/03/19 10:05 vkuncak 2008/03/19 10:05 vkuncak 2008/03/19 10:04 vkuncak 2008/03/18 18:40 vkuncak created 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 47: Line 47: === NNF of Example === === NNF of Example === - $+ \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 54: Line 54: & (\exists x. \forall y.\ \neg R(x,y) \vee \neg P(y)) & (\exists x. \forall y.\ \neg R(x,y) \vee \neg P(y)) \end{array} \end{array} -$ + \end{equation*} Line 62: Line 62: Prenex normal form (PNF) is a formula of the form Prenex normal form (PNF) is a formula of the form - $+ \begin{equation*} Q_1 x_1. Q_2 x_2. \ldots Q_n x_n. G Q_1 x_1. Q_2 x_2. \ldots Q_n x_n. G -$ + \end{equation*} where $Q_i \in \{\forall, \exists\}$ and $G$ has no quantifiers. where $Q_i \in \{\forall, \exists\}$ and $G$ has no quantifiers. Line 75: Line 75: === PNF of Example === === PNF of Example === - $+ \begin{equation*} \begin{array}{l@{}l} \begin{array}{l@{}l} & (\forall x_1. \exists y_1.\ R(x_1,​y_1))\ \land \\ & (\forall x_1. \exists y_1.\ R(x_1,​y_1))\ \land \\ Line 82: Line 82: & (\exists x_4. \forall y_4.\ \neg R(x_4,y_4) \vee \neg P(y_4)) & (\exists x_4. \forall y_4.\ \neg R(x_4,y_4) \vee \neg P(y_4)) \end{array} \end{array} -$ + \end{equation*} Line 90: Line 90: Note that Note that - $+ \begin{equation*} \exists x. \forall y. P(y,x) \to \forall u. \exists v. P(u,v) \exists x. \forall y. P(y,x) \to \forall u. \exists v. P(u,v) -$ + \end{equation*} but converse implication does not hold (take as $P$ relation $\le$ or $>$ on natural numbers). but converse implication does not hold (take as $P$ relation $\le$ or $>$ on natural numbers). In general, we have this theorem: In general, we have this theorem: - $+ \begin{equation*} ​\forall u. \exists v. P(u,v) \leftrightarrow \exists g. \forall u. P(u,g(u)) ​\forall u. \exists v. P(u,v) \leftrightarrow \exists g. \forall u. P(u,g(u)) -$ + \end{equation*} where $g : D \to D$ is a function. where $g : D \to D$ is a function. Line 112: Line 112: **Definition:​** Skolemization is the result of applying this transformation ​ **Definition:​** Skolemization is the result of applying this transformation ​ - $+ \begin{equation*} \forall x_1,​\ldots,​x_n. \exists y. F \ \leadsto ​ \forall x_1,​\ldots,​x_n. \exists y. F \ \leadsto ​ \forall x_1,​\ldots,​x_n. subst(\{y \mapsto g(x_1,​\ldots,​x_n)\})(F) \forall x_1,​\ldots,​x_n. subst(\{y \mapsto g(x_1,​\ldots,​x_n)\})(F) -$ + \end{equation*} to the entire PNF formula to eliminate all existential quantifiers. ​ Above, $g$ is a fresh function symbol. ​ Denote $snf(F)$ the result of applying skolemization to formula $F$. to the entire PNF formula to eliminate all existential quantifiers. ​ Above, $g$ is a fresh function symbol. ​ Denote $snf(F)$ the result of applying skolemization to formula $F$. Line 121: Line 121: === SNF for Example === === SNF for Example === - $+ \begin{equation*} \begin{array}{l@{}l} \begin{array}{l@{}l} & (\forall x. R(x,g(x)))\ \land \\ & (\forall x. R(x,g(x)))\ \land \\ Line 128: Line 128: & (\forall y.\ \neg R(c,y) \vee \neg P(y)) & (\forall y.\ \neg R(c,y) \vee \neg P(y)) \end{array} \end{array} -$ + \end{equation*} 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//​. Line 135: Line 135: Let $snf(F)$ be $\forall x_1,​\ldots,​x_n. F$.  Convert $F$ to conjunctive normal form $C_1 \land \ldots \land C_m$.  Then $snf(F)$ is equivalent to Let $snf(F)$ be $\forall x_1,​\ldots,​x_n. F$.  Convert $F$ to conjunctive normal form $C_1 \land \ldots \land C_m$.  Then $snf(F)$ is equivalent to - $+ \begin{equation*} (\forall x_1,​\ldots,​x_n. C_1) \land \ldots \land (\forall x_1,​\ldots,​x_n. C_m) (\forall x_1,​\ldots,​x_n. C_1) \land \ldots \land (\forall x_1,​\ldots,​x_n. C_m) -$ + \end{equation*} where each $C_i$ is a disjunction of first-order literals. ​ We call $C_i$ //​(first-order) clause//​. ​ For a given formula $F$, denote the set of such clauses in conjunctive normal form of $snf(pnf(F))$ by $clauses(F)$. where each $C_i$ is a disjunction of first-order literals. ​ We call $C_i$ //​(first-order) clause//​. ​ For a given formula $F$, denote the set of such clauses in conjunctive normal form of $snf(pnf(F))$ by $clauses(F)$. Line 143: Line 143: **Theorem:​** The set $S$ is satisfiable iff the set **Theorem:​** The set $S$ is satisfiable iff the set - $+ \begin{equation*} \bigcup_{F \in S} clauses(F) \bigcup_{F \in S} clauses(F) -$ + \end{equation*} is satisfiable. is satisfiable. Line 158: Line 158: Let ${\cal L} = \{ less \}$ be binary relation ("​strictly less"​). ​ We consider the following axioms for irreflexive partial order that is total and dense: Let ${\cal L} = \{ less \}$ be binary relation ("​strictly less"​). ​ We consider the following axioms for irreflexive partial order that is total and dense: - $\begin{array}{rcl} + \begin{equation*}\begin{array}{rcl} IRef & \equiv & \forall x.\ \lnot less(x,x) \\ IRef & \equiv & \forall x.\ \lnot less(x,x) \\ Tra & \equiv & \forall x.\ \forall y.\ \forall z.\ less(x,y) \land less(y,z) \rightarrow less(x,z) \\ Tra & \equiv & \forall x.\ \forall y.\ \forall z.\ less(x,y) \land less(y,z) \rightarrow less(x,z) \\ Line 164: Line 164: Dense & \equiv & \forall x. \forall y.\ less(x,y) \rightarrow \exists z.\ less(x,z) \land less(z,y) Dense & \equiv & \forall x. \forall y.\ less(x,y) \rightarrow \exists z.\ less(x,z) \land less(z,y) \end{array} \end{array} -$ + \end{equation*} Let us find clauses for these axioms : Let us find clauses for these axioms : - $\begin{array}{lcr} + \begin{equation*}\begin{array}{lcr} \lnot less(x_1,​x_1) \\ \lnot less(x_1,​x_1) \\ \lnot less(x_2,​y_2) \lor \lnot less(y_2,​z_2) \lor less(x_2,​z_2) \\ \lnot less(x_2,​y_2) \lor \lnot less(y_2,​z_2) \lor less(x_2,​z_2) \\ Line 174: Line 174: \lnot less(x_4,​y_4) \lor \ less(f(x_4, y_4),y_4) \lnot less(x_4,​y_4) \lor \ less(f(x_4, y_4),y_4) \end{array} \end{array} -$ + \end{equation*}