Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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