Department of Computer Science
CS 2209A — Applied Logic for Computer Science
Assignment 2
1. Convert the following First Order sentences to Conjunctive Normal Form. Show all intermediate conversion steps. Include steps that are required to incorporate the clauses into an
empty set ready to do resolution.
(a) ∃x∀yL(x, y)
(b) ∀x∃yL(y, x)
(c) ∀z{Q(z) ⇒ {¬∀x∃y[P(y) ⇒ P(g(z, x))]}}
2. With the clauses given by Γ show Γ ` ∃x¬B(x) using resolution.
Γ = n
¬B(x) ∨ C(x), ¬C(a) ∨ D(b), ¬C(c) ∨ E(d), ¬D(w) ∨ ¬E(y)
o
Use the following demonstration format:
1. clause Given
.
.
.
k. clause Given
k+1. clause line number, line number, unifier (+ standardize variables apart)
.
.
.
n. empty line number, line number, unifier (+ standardize variables apart)
3. Show using resolution that the following statement is valid.
∀xP(x) → ∃yP(y)
4. Show a bottom up derivation of Γ ` R(a1, a1) using the bottom up proof algorithm given the
definite clauses (written as head ← body) in set Γ.
Γ =
P(a2, a1)
P(a3, a2)
P(a4, a3)
P(a1, a4)
Q(x, y) ← P(x, y)
Q(x, y) ← Q(x, z) ∧ P(z, y)
R(x, y) ← Q(y, x)
5. Show a top down derivation of Γ ` R(a1, a1 using the top down proof algorithm given the
definite clauses (written as head ← body) in set Γ from the previous question.
