FOL and Conjuctive Normal Form Conversion

Question

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.

Answer 1

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))]$