LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
sav08:normal_forms_for_first-order_logic [2015/02/16 10:36]
vkuncak
sav08:normal_forms_for_first-order_logic [2015/02/16 10:36]
vkuncak
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.