# FOL and Conjuctive Normal Form Conversion

I see the CNF from following firs order logic:

$\forall x [ \forall y [ \neg A(y) \vee B(x,y) \Rightarrow [ \neg \forall y B(y,x) ] ]$

is equivalent to :

$(A(f(x)) \vee \neg B(g(x),x)) \wedge (\neg B (x,f(x)) \vee \neg B(g(x),x))$

How this CNF is calculated? i.e: how convert above the FOL sentence to above CNF?

Thanks to all.

• There is a typo in the formula, due to a right parentheses missing... Is it : (i) ∀x[∀y[(¬A(y)∨B(x,y))⇒[¬∀yB(y,x)]]] or (ii) ∀x[∀y[(¬A(y)∨B(x,y))]⇒[¬∀yB(y,x)]] ? – Mauro ALLEGRANZA Oct 22 '14 at 14:37

Assuming that the correct formula is :

$∀x[∀y[¬A(y)∨B(x,y)]⇒[¬∀yB(y,x)]]$ --- (*)

we have that $p \Rightarrow q$ is equivalent to $\lnot p \lor q$; thus (*) is :

$∀x[\lnot ∀y[¬A(y)∨B(x,y)] \lor [¬∀yB(y,x)]]$

i.e. :

$∀x[\exists y \lnot (¬A(y)∨B(x,y)) \lor \exists z (\lnot B(z,x))]$

i.e. to :

$\forall x \exists y \exists z [\lnot (¬A(y)∨B(x,y)) \lor \lnot B(z,x)]$.

Now we apply De Morgan to the left disjunct to get :

$\forall x \exists y \exists z [(A(y) \land \lnot B(x,y)) \lor \lnot B(z,x)]$

and ditribute the right disjunct :

$\forall x \exists y \exists z [(A(y) \lor \lnot B(z,x)) \land (\lnot B(x,y) \lor \lnot B(z,x))]$ ---(§).

The final step is to introduce skolem functions to get rid of existential quantifiers, i.e. remove every existential quantifier in the prefix replacing the corresponding variable with a new $n$-ary function symbol (the so-called "skolem function") where $n$ is the number of universal quantifiers preceding the existential one to be removed.

In the prefix of (§) we have the first existential quantifier : $\exists y$ and the second one : $\exists z$; both are preceded by a single universal quantifier : $\forall x$.

Thus, we need two unary skolem functions $f(x)$ and $g(x)$; they will replace variables $y$ and $z$ respectively, now free after the removal of the leading existential quantifiers, getting :

$\forall x [(A(f(x)) \lor \lnot B(g(x),x)) \land (\lnot B(x,f(x)) \lor \lnot B(g(x),x))]$

• Would u please describe about latest step? – Mouna Mokhiab Oct 22 '14 at 20:39
• @MounaMokhiab - see in Conjunctive normal form Step 3 : Skolemize the statement of Converting from first-order logic. – Mauro ALLEGRANZA Oct 23 '14 at 18:23
• I need It to tutor me... – Mouna Mokhiab Oct 23 '14 at 19:09
• first A(y) should be F(x) – Mouna Mokhiab Oct 24 '14 at 16:33