Convert to clause form:
Convert the following statement to clause form:
?x[B(x)? ( ?y [ Q(x,y) ? ? P(y) ]
? ? ?y [ Q(x,y) ? Q(y,x) ]
? ?y [ ? B(y) ? ? E(x,y)] ) ]
1- Eliminate the implication (?)
E1 ? E2 = ?E1 ? E2
?x[? B(x) ? ( ?y [ Q(x,y) ? ? P(y) ]
? ? ?y [ Q(x,y) ? Q(y,x) ]
? ?y [ ? ( ? B(y)) ? ? E(x,y)] ) ]
2- Move the negation down to the atomic formulas (by using the following rules)
• ? (P?Q) ? ? P ? ? Q
• ? (P?Q) ? ? P ? ? Q
• ? ( ? ( P ) ) ? P
• ? ?x ( P (x) ) ? ?x (? P (x) )
• ? ?x ( P (x) ) ? ?x (? P (x) )
?x[? B(x) ? ( ?y [ Q(x,y) ? ? P(y) ]
? ?y [ ? Q(x,y) ? ? Q(y,x) ]
? ?y [ B(y) ? ? E(x,y)] ) ]
3- Purge existential quantifiers
The function that is eliminate the existential are called “ Skolem function”
?x[? B(x) ? ( [ Q(x , f (x)) ? ? P(f (x)) ]
? ?y [ ? Q(x,y) ? ? Q(y,x) ]
? ?y [ B(y) ? ? E(x,y)] ) ]
4- Rename variables, as necessary, so that no two variables are the same.
?x[? B(x) ? ( [ Q(x , f (x)) ? ? P(f (x)) ]
? ?y [ ? Q(x,y) ? ? Q(y,x) ]
? ?z [ B(z) ? ? E(x,z)] ) ]
5- Move the Universal quantifiers to the left of the statement.
?x ?y ?z [? B(x) ? ( [ Q(x , f (x)) ? ? P(f (x)) ]
? [ ? Q(x,y) ? ? Q(y,x) ]
? [ B(z) ? ? E(x,z)] ) ]
6- Move the disjunction down to the literals, using distributive laws
E1 ? (E2 ? E3 ? E4 ?…) ? (E1 ? E2) ? (E1?E3) ? ….
E1 ? (E2 ? E3 ? E4?…) ? (E1 ? E2) ? (E1?E3) ? ….
?x ?y ?z [ ( ? B(x) ? ( Q(x , f (x)) ? ? P(f (x) ) ) )
? [ ? B(x) ? ? Q(x,y) ? ? Q(y,x) ]
? [? B(x) ? B(z) ? ? E(x,z)] ]
?x ?y ?z [ ( ? B(x) ? ( Q(x , f (x))
? ( ? B(x) ? ? P(f (x) ) )
? ( ? B(x) ? ? Q(x,y) ? ? Q(y,x) )
? (? B(x) ? B(z) ? ? E(x,z) ) ]
7- Eliminate the conjunctions
?x [ ? B(x) ? ( Q(x , f (x) ]
?x [? B(x) ? ? P(f (x) ) ]
?x ?y [ ? B(x) ? ? Q(x,y) ? ? Q(y,x) ]
?x ?z [? B(x) ? B(z) ? ? E(x,z) ]
8- Rename all the variables, as necessary, so that no two variables are the same.
?x [ ? B(x) ? ( Q(x , f (x) ]
?w [? B(w) ? ? P(f (w) ) ]
?u ?y [? B(u) ? ? Q(u,y) ? ? Q(y,u) ]
?a ?z [? B(a) ? B(z) ? ? E(a,z) ]
9- Purg the universal quntifiers.
? B(x) ? ( Q(x , f (x)
? B(w) ? ? P(f (w) )
? B(u) ? ? Q(u,y) ? ? Q(y,u)
? B(a) ? B(z) ? ? E(a,z) )