Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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*}
  
 
sav08/normal_forms_for_first-order_logic.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice