top of page

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


450 views0 comments

Comments


bottom of page