We have to transform the following sentence into clausal form:

∃x ∀y (∀z P(f(x),y,z)→(∃u Q(x,u) & ∃v R(y,v)))

Now, there are four steps to do this.

**Step 1: Remove biconditional statements**

A↔B = (A→B)∧(B→A)

**Step 2: Remove implicative sentences.**

(A→B) = ¬A∨B

**Step 3: Move negation inwards**

¬(A∧B) = ¬(A) ∨ ¬(B)

¬(A∨B) = ¬(A) ∧ ¬(B)

¬(¬A) = A

**Step 4: Skolemization**

We remove the existential quantifiers by introducing Skolem functions. We will talk about this later.

So, let us start by **removing implication.**

The implication is given as,

∀z P(f(x),y,z)→(∃u Q(x,u) & ∃v R(y,v))

= ¬∀z P(f(x),y,z)∨(∃u Q(x,u) & ∃v R(y,v))

Now, let us replace this in the original equation.

∃x ∀y (¬(∀z P(f(x),y,z))∨(∃u Q(x,u) & ∃v R(y,v)))

Next, we **move the negation inside the bracket**. We use the following formula:

¬∀x A(x) = ∃x ¬A(x)

So, we get,

∃x ∀y (∃z ¬P(f(x),y,z)∨(∃u Q(x,u) & ∃v R(y,v)))

Now, let's talk about **skolemization**. In artificial intelligence and logic programming, Skolemization is a process used to eliminate existential quantifiers (∃) from logical formulas. Let's introduce a Skolem constant *c* for *x*, a Skolem function *g*(*y*) for *z*, a Skolem function *h*(*y*) for *u*, and a Skolem function *k*(*y*) for *v*:

The equation thus becomes:

∀y (¬P(f(c),y,g(y))∨(Q(x,h(y)) & ∃v R(y,k(y))))

Now we have to convert this equation to **conjunctive normal form**.

∀y((¬P(f(c),y,g(y))∨Q(c,h(y)))∧(¬P(f(c),y,g(y))∨R(y,k(y))))

In clausal form, each clause is a disjunction of literals, and the formula is a conjunction of these clauses:

{¬P(f(c),y,g(y)),Q(c,h(y))}

{¬P(f(c),y,g(y)),R(y,k(y))}

Thus, the clausal form of the original formula is:

{¬P(f(c),y,g(y)),Q(c,h(y))}∧{¬P(f(c),y,g(y)),R(y,k(y))}

Expressed as a set of clauses, the clausal form is:

{{¬P(f(c),y,g(y)),Q(c,h(y))},{¬P(f(c),y,g(y)),R(y,k(y))}}

## Comments