Convert the following propositional logic start into CNF.

A $\rightarrow$ (B $\Leftrightarrow$ C)

Solution:

Step 1: Eliminate implication.

$\alpha \rightarrow B \therefore \ \neg \ \alpha \vee B$

$\Rightarrow \ \neg \ A \vee ( B \Leftrightarrow C)$

Step 2: Eliminate bi-directional implication.

$\alpha \Leftrightarrow B \therefore (\alpha \rightarrow B)$

$\ \neg \ A \vee (B \rightarrow C) \wedge (C \rightarrow B)$

$\neg \ A \vee (\ \neg \ B \vee C) \wedge (\ \neg \ C \vee B))$

Step 3: Apply distribute law.

$(\ \neg \ A \vee \ \neg \ B \vee C) \wedge (\ \neg \ A \vee \ \neg \ C \vee B)$

$(A \Leftrightarrow B) \rightarrow C$

Solution: Eliminate $\alpha \Leftrightarrow$ B with $(\alpha \rightarrow B) \wedge (B \rightarrow \alpha)$

$((A \rightarrow B) \wedge (B \rightarrow A)) \rightarrow C$

Some students took French in spring 2001

$ \exists_x$ students (x) $\wedge$ fakes (X, F Spring 2001).

Every student who takes French passed it.

$\forall$, X, S student(x) $\wedge$ fakes (x, f, s) $\Rightarrow$ passes (x, f, s).

$\therefore$ only one student took Greek in spring 2001.

$\exists_x$ student (x) n Fakes (X, G, Spring 2001) $\wedge \vee$ $\forall$ Y $\neg$ X

$\Rightarrow \ \neg$ Fakes (Y, G, Spring 2001).

Every gardener likes sun.

$\forall_x$ gardenercies $\rightarrow$ likes (x, sun).

No purple. Mushroom is poisonous.

$\forall$x mushroom (x) $\wedge$ purple (x) $\rightarrow$ $\neg$ poisonous (x)

$\ \neg \ \exists_x$ purple (x) $\wedge$ mushroom (x) $\wedge$ poisonous (x)

Deb is not tall

$\neg$ tall (Deb)

• You can fool some of the people of all the time.

$\exists_x$ person (x) $\wedge $ $\forall$ t time (t) $\rightarrow$ can – fool (x, t)

• You can fool all of the people some of time

$\forall$x person (x) $\rightarrow$ $\exists_t$ time (t) $\wedge$ can fool (x, t)

Resolution.

• CNF First order logic.

• Everyone who loves all animals is loved by someone.

$\forall_x [ \forall_y \ Animal \ (y) \ \Rightarrow \ Loves \ (x,y)] \Rightarrow [\exists_y \ Love \ (y,x)]$

Steps.

1] Eliminate implication.

$\forall_x [ \ \neg \ \forall_y \ \neg \ Animal \ (y) \vee \ Loves \ (x,y)] \vee [\exists_y \ Loves \ (y,x)]$

2] Move $\neg$ inwards.

$\neg \forall_x \ p \ becomes \ \exists_x \ \neg \ P$

$\neg \ \exists \ x \ p \ becomes \ \forall_x \ \neg \ p$

$\therefore \ \forall_x [ \exists y \ \neg \ (\neg \ Animal \ (y) \vee Loves (x,y))] \vee [\exists_y \ Loves \ (y,x)]$

$\forall_x [\exists_y \ \neg \ \neg \ Animal \ (y) \vee \ \neg \ Loves (x,y)] \vee [\exists_y \ Loves \ (y,x)]$

$\forall_x [\exists_y Animal \ (]) \vee \neg \ Loves \ (x,y)] \vee [\exists_y \ Loves \ (y,x)]$

3] Standardize variables.

$\forall_x [\exists_y \ Animal \ (y) \wedge \ \neg \ Loves (x,y)] \vee [\exists_z \ Loves \ (z,y)]$

4] Solemnize – remaining existential quantifier.

$\exists x \ p(x) \Rightarrow p(A) -$ A is constant.

$\forall$x $[Animal (A) \wedge \ \neg \ Loves \ (x, A)] \vee \ Loves \ (B, x)$

Skolem entities to depend on x.

$\forall_x [Animal \ (F(x)) \wedge \ \neg \ \ Loves \ (x, F(x))] \vee \ Loves \ (G(x), x)$

F, G are skolem functions.

5] Drop universal quantifier.

$[Animal \ (F (x)) \wedge \ \neg \ Loves \ (x, f(x))] \vee Loves \ (G(x), x)$

6] Distribute $\wedge \ over \ \vee$

$[Animal \ (f (x)) \vee Loves \ (G (x), x)] \wedge$

$[ \ \neg \ Loves (x, f(x)) \vee Loves \ (G (x), x,)]$