Transform the following into clausal form: ∃x ∀y (∀z P(f(x),y,z)→(∃u Q(x,u) & ∃v R(y,v)))

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))}}