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 [2015/02/16 10:36] vkuncak |
sav08:normal_forms_for_first-order_logic [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 10: | Line 10: | ||
Consider this formula in ${\cal L}$: | Consider this formula in ${\cal L}$: | ||
- | \begin{equation} | + | \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} | + | \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*} |