Introduction to AI: Tutorial
Foundation of Logic and Resolution-based Proof Procedures
Alessandra Russo
The aim of this tutorial is to enable you to practise more with fundamental logic-
based concepts, introduced in Unit 2, and to gain more practice with SLD and SLDNF
derivations from KB expressed using definite clauses and normal clauses.
Question 1
Convert the following first-order sentences into clausal representation:
i) ∀X∃Y friend(X, Y )→ ∃V happy(V )
ii) ∀Y (∃XP (X, Y )→ ¬ S(Y ))
iii) ∀X(philosopher(X)→ ∃Y (book(Y ) ∧ write(X, Y )))
Question 2
If possible unify the following pairs and give the unification φ, otherwise explain why
they do not unify:
1) p(f(X), g(Y )) and p(Z, g(f(a))) 2) p(Y, a, b, Y ) and p(c, F,G, F )
3) p(X,X) and p(E,E) 4) p(f(X)) and q(f(X))
5) p(V, g(X)) and p(f(X), V )
Question 3
Consider a knowledge base (KB) about the following sentences:
(a) Lucy is a professor.
(b) All professor are people.
(c) John is a dean.
(d) Deans are professors.
(e) All professor consider the dean a friend or they don’t know him.
1. Formalise each of the above sentence into first-order logic
2. Convert them into clausal form.
Introduction to AI: Tutorial 2
3. Let KB be the set of clauses that you have given in your answer to part (2)
above. Write KB in rule form.
4. Assume the only constants to be Lucy and John. Write in full the ground(KB)
(i.e. the grounding of KB).
5. Give the Herbrand base of KB.
6. Give the Least Herbrand model of KB, and an example of an Herbrand inter-
pretation that is not a model of KB.
7. Using resolution show that KB 6|= friendOf(lucy, john). Explain also seman-
tically why this is the case.
Question 4
Consider the following KB. Give the SLDNF tree of all derivations of the goal p(X)
from KB.
KB =
p(X)← not q(X), s(X, Y )
q(X)← not r(X).
r(a).
r(b).
s(a, b).
s(c, b).
Question 5
Consider the following KB, which formalises the notion that
A student passes the year in which he/she is enrolled if
he/she has not failures in any course. John in a student enrolled
in his first year, and Logic is a course.
KB =
passedY ear(X, Y )← year(Y ), enrolled(X, Y ), not failures(X,C)
year(firstY ear).
enrolled(john, firstY ear).
course(Logic).
1. Explain why there does not exist an SLDNF derivation of passedY ear(X, Y )
from KB.
2. Modify the KB so that it does accept a derivation of passedY ear(X, Y ) for
some unification of X and Y , and give an example of such an SLDNF derivation.
Alessandra Russo Tutorial: Foundation of Logic and Resolution-based Proof Procedures