• English only

# 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)
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*}