Convert the following First Order sentences to Conjunctive Normal Form. Show all inter-mediate conversion steps. Include steps that are required to incorporate the clauses into an empty set ready to do resolution.
9x8yL(x; y)
8x9yL(y; x)
8zfQ(z) ) f:8x9y[P (y) ) P (g(z; x))]gg
2. With the clauses given by show ‘ 9x:B(x) using resolution.
n o
:B(x) _ C(x); :C(a) _ D(b); :C(c) _ E(d); :D(w) _ :E(y)
Use the following demonstration format:
1. clause Given
...
k. clause Given
k+1. clause line number, line number, uni er (+ standardize variables apart)
...
n. empty line number, line number, uni er (+ standardize variables apart)
Show using resolution that the following statement is valid. 8xP (x) ! 9yP (y)
Show a bottom up derivation of de nite clauses (written as head
‘ R(a1; a1) using the bottom up proof algorithm given the body) in set
8
P (a3; a2)
9
P (a2; a1)
P (a4; a3)
<
=
P (a1; a4)
Q(x; y)
Q(x; z) P (z; y)
Q(x; y)
P (x; y)
^
R(x; y)
Q(y; x)
:
;
Show a top down derivation of de nite clauses (written as head
‘ R(a1; a1 using the top down proof algorithm given the body) in set from the previous question.
