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.

  • $\begingroup$ 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)]] ? $\endgroup$ – 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))]$

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.