COSC1127/1125 Artificial Intelligence
School of Computing Technologies Semester 2, 2021
Prof. ̃a
Tutorial No. 5 KR&R II – First Order Logic
For some of the questions below, you may want to check the great slides by (CSC 384 at University of Toronto) on Skolemization, Most General Unifiers, First-Order Resolution. It includes the Skolem- ization process to remove existential quantification, the algorithm for finding MGUs, and FOL resolution; all with great fully detailed examples!
Predicates
A term is either a variable or a name (sometimes called a constant).1
A formula (or first-order formula) is
• p(x1,…,xn) where x1,…,xn are terms. p is called a predicate, and p(x1,…,xn) is called an atom. • ¬P where P is a formula.
• P ∨Q,P ∧Q,P ⇒QandP ⇔QwhereP andQareformulae.
• ∀xP and ∃xP where P is a formula with free variable x. ∀ and ∃ are called quantifiers.
A literal is an atom or the negation of an atom. For example, p(1, 2) and ¬q(3) are both literals, but ∀x¬p(x) is not. We will say a formula is in literal form if all negations in the formula occur only in literals. For example, the formula ¬∀x p(x, x) is not in literal form, whereas ¬p(1, 2) is in literal form.
Note that all the previous logical equivalences (denoted ≡) are still true. The ones from last week and some specific to quantifiers are below.
P ∧(Q∨R)≡(P ∧Q)∨(P ∧R) P ∨(Q∧R)≡(P ∨Q)∧(P ∨R) ¬¬P ≡ P
¬(P ∧Q)≡(¬P)∨(¬Q)
¬(P ∨Q)≡(¬P)∧(¬Q) ∀x p(x) ≡ ∀y p(y) ∀x∀yP ≡∀y∀xP ¬∀xP ≡∃x¬P
∀x P(x) ⇒ Q(x) ≡ ∀x¬Q(x) ⇒ ¬P(x)
Distributive Law 1 Distributive Law 2
De Morgan Law 1 De Morgan Law 2 ∃x p(x) ≡ ∃y p(y) ∃x∃yP ≡∃y∃xP ¬∃xP ≡∀x¬P Contrapositive
Please remember that ≡ is NOT a logical symbol, so α ≡ β is NOT a formula in the FOL language. Instead, α ≡ β is a shorthand for the claim (at the English meta-level), that α |= β and β |= α, or what is the same, that for every FOL interpretation/models M, M |= α if and only if M |= β.
1Strictly speaking there are other kinds of terms as well, but we will not be concerned with them in this course. 1
COSC1127/1125 – AI Tutorial 5: KR&R II – First Order Logic Page 2 of 17
Using quantifiers and connectives
The choice of quantifiers and connectives has a very big impact on the ultimate meaning of a logical statement. For example, if X is an object in the universe of discourse (i.e., the set of objects being considered), the predicate zebra(X) means X is a zebra and the predicate striped(X) means X is striped, the statement
∀x zebra(x) ⇒ striped(x),
is read as all zebras are striped. Intuitively, you can think of logical implication as an if-then conditional statement, in which case this is read as for all x in the universe of discourse, if x is a zebra, then x is striped.
The meaning of this statement can be changed by changing the connective. For example, the statement
∀x zebra(x) ∧ striped(x),
is read as everything is a zebra and everything is striped, meaning everything in the universe of discourse is a striped zebra!
Similarly, changing the quantifier will also change the meaning. For example, the statement
∃x zebra(x) ∧ striped(x),
is read as there exists an x, where x is a zebra and x is striped, meaning that out of all of the objects in the universe
of discourse at least one is a striped zebra. Finally, the statement
∃x zebra(x) ⇒ striped(x),
is a bit more tricky and you will almost never see this combination of quantifier and connective. This statement is read as there exists an x, where if x is a zebra, then x is striped. The difference is a bit subtle, but the important thing to understand is that this statement only guarantees that x exists, it does not guarantee that x is a zebra or that it is striped!
As a general rule-of-thumb, the universal quantifier (∀x) is usually paired with the implication connective (⇒) and the existential quantifier (∃x) is usually paired with the conjunction connective (∧).
PART1: Predicatelogicformulas…………………………………………………………..
(a) Choose a vocabulary of predicates, constants and functions appropriate for representing the following information in First Order Logic, then represent each sentence in FOL.
i. “There is someone who is loved by everybody”
ii. “All cats are lazy”
iii. “Some students are clever”
iv. “No student is rich”
Solution:
(∃y)(∀x)loves(x, y)
Solution: (Note: this is a partial solution)
….(cat(x) ⇒ ….)
Solution:
(∃x)(student(x) ∧ clever(x))
Solution:
(¬∃x)(student(x) ∧ rich(x)) or
(∀x)(student(x) ⇒ ¬rich(x))
RMITAI2021(Semester2)-SebastianSardin ̃a Exercise1continuesonthenextpage…
COSC1127/1125 – AI Tutorial 5: KR&R II – First Order Logic Page 3 of 17
v. “Every man loves a woman” (represent both meanings)
Solution: Your turn!
vi. “Everything is bitter or sweet”
vii. “Everything is bitter or everything is sweet”
viii. “Martin has a new bicycle”
Solution: Your turn!
ix. “Lynn gets a present from John, but she doesn’t get anything from Peter”
(b) Do the same as for the previous question. i. Anyone who is rich is powerful.
ii. Anyone who is powerful is corrupt.
Solution: Your turn!
iii. Anyone who is meek and has a corrupt boss is unhappy.
iv. Not all students take both Computing-Theory and OO-Programming.
Solution: Your turn!
v. Only one student failed Computing-Theory.
Solution:
(∀x)(bitter(x) ∨ sweet(x))
Solution:
(∀x)bitter(x) ∨ ∀ysweet(y)
Solution:
(∃x)(present(x)∧gets(Lynn,x,John))∧ ((¬∃y)(present(y) ∧ gets(Lynn, y, P eter)) ∧ (x ̸= y)
Solution:
(∀x)(rich(x) ⇒ powerful(x))
Solution:
(∀x)(∃y)(meek(x) ∧ isBoss(y, x) ∧ corrupt(y) ⇒ unhappy(x))
Solution:
(∃x)student(x)∧fails(x,CT)∧(∀y)student(y)∧fails(y,CT) ⇒ x = y
In this example, an equality symbol is used to make a statment about the effect that two terms refer to the same object. For the above first sentence,
(∃x)student(x)∧fails(x,CT)∧(∀y)student(y)∧fails(y,CT)
would only assert that all instances of y and there is at least one x that failed CT, but nothing says that x and y are referring to the same object.
You can imagine that you run a loop going over all possible y values, and there is an x value where x = y is true. When this is the case, the implication stands.
Note that in a knowledge base, the existential quantifier is eliminated by replacing it with specific instances. Based on this assumption, the above sentence will refer to only one specific student who failed CT.
vi. Only one student failed both Computing-Theory and OO-Programming.
RMITAI2021(Semester2)-SebastianSardin ̃a Exercise1continuesonthenextpage…
COSC1127/1125 – AI Tutorial 5: KR&R II – First Order Logic Page 4 of 17
Solution: Your turn!
vii. The best score in Computing-Theory was better than the best score in OO-Programming.
viii. Every person who dislikes all donkeys is smart.
ix. There is a woman who likes all men who are not footballers.
Solution: Your turn!
x. There is a barber who shaves all men who do not shave themselves.
xi. No person likes a lecturer unless the lecturer is smart.
Solution: Your turn!
xii. Politicians can fool some of the people all of the time, and they can fool all of the people some of the
time, but they can’t fool all of the people all of the time.
(c) Consider the following story:
I married a widow (let’s call her w) who has a grown up daughter (d). My father (f ), who visited us quite often, fell in love with my step-daugher and married her. Hence my father became my son-in-law and my step-daughter became my mother. Some months later, my wife gave birth to a son (s1), who became the brother-in-law of my father, as well as my uncle. The wife of my father, that is, my step-daughter, also had a son (s2).
Using predicate calculus, create a set of expressions that represent the situation in the above story. Ex- tend the kinship relations to in-laws and uncle. Use generalised modus ponens to prove ‘I am my own grandfather’.
Solution:
(∃x)(score(x, CT ) ∧ ((∀y)score(y, OO) ⇒ better(x, y)))
Since there is no negation in front of the universal quantifier (and no scope clashes), it can be moved to the front of the formula without changing the expression.
(∃x)(∀y)(score(x, CT ) ∧ (score(y, OO) ⇒ better(x, y)))
Solution:
(∀x)person(x) ∧ ((∀y)donkey(y) ⇒ dislikes(x, y)) ⇒ smart(x)
Solution:
(∃x)barber(x) ∧ ((∀y)man(y) ∧ ¬shaves(y, y)) ⇒ shaves(x, y)
Solution:
(∀x)politician(x) ⇒ ((∃y)(∀t)person(y) ∧ f ools(x, y, t)) ∧ ((∃t)(∀y)person(y) ∧ f ools(x, y, t)) ∧ ¬((∀t)(∀y)person(y) ⇒ f ools(x, y, t))
Solution:
This works fine (with a little violation of the accepted semantics for family relationships).
Here is an example showing how we can prove this; we can have the following rules (among others):
(∀x)(∀y)child(x, y) ≡ parent(y, x) (1) (∀x)(∀y)(∃z)grandparent(x, y) ≡ parent(x, z) ∧ parent(z, y) (2)
From the given story we can get the following facts (once again, among others):
parent(F, I) (since F is my father), (3)
RMIT AI 2021 (Semester 2) – ̃a
COSC1127/1125 – AI Tutorial 5: KR&R II – First Order Logic Page 5 of 17
child(F, I) (since my father becomes my son-in-law). (4) Some of the other rules are: (parent(W,D),spouse(I,W),spouse(F,D), etc), but we don’t really
need them since we can already prove our conclusion.
From1and4(takey=F andx=I)wederivethat
parent(I,F) (5)
Finally, from 3 and 5 we derive (take x = I,y = I and z = F): grandparent(I, I)
Thus, “I am my own grandfather”!
PART 2: Representing family relationships…………………………………………………. You are given an enormous table of family information. This consists of a very large number of facts, which are organised into predicates as below.
Predicate
parent(x, y) male(x) female(x)
Meaning
x is a parent of y x is male
x is female
Use this information to define the relationships below by giving an appropriate formula based on the above three predicates.
Example: To capture he relation “x is the brother of y”, we can write: male(x) ∧ ∃z(parent(z, x) ∧ parent(z, y))
and so define the new relation brother(x, y) via the following formula (note the formula is an equivalence between the new predicate and the formula):
∀x, y[brother(x, y) ⇔ (male(x) ∧ ∃z(parent(z, x) ∧ parent(z, y))]
This formula is, basically, defining what the brother relation is in terms of the other two relations. Note the universal quantification at the outset of the whole equivalence formula: the relation between x and y holds for every pair of x and y.
(a) x is the sister of y.
(b) xistheuncleofy. Solution: Your turn!
(c) x is the grandmother of y.
Solution: female(x)∧∃zparent(z,x)∧parent(z,y)
and if we want to define a new relation to capture the sister notion we can write the following formula:
∀x, y[sister(x, y) ⇔ f emale(x) ∧ ∃z parent(z, x) ∧ parent(z, y)]
RMITAI2021(Semester2)-SebastianSardin ̃a Exercise2continuesonthenextpage…
COSC1127/1125 – AI
Tutorial 5: KR&R II – First Order Logic
Page 6 of 17
Solution: female(x)∧∃wparent(x,w)∧parent(w,y)
and if we want to define a new relation to capture the grandmother notion:
∀x, y[grandma(x, y) ⇔ f emale(x) ∧ ∃w parent(x, w) ∧ parent(w, y)]
(d) x is an orphan. Solution: Your turn!
(e) x is not an orphan.
Solution: ∃z parent(z, x)
If we had a predicate orphan(x) already we can state when exactly that predicate is false as follows:
∀x[¬orphan(x) ⇔ ∃z parent(z, x)]
While not necessary, on could use a different predicate to state that x is not an orphan, something like
this:
∀x[notOrphan(x) ⇔ ∃z parent(z, x)]
See that notOrphan(x) is just another predicate name. The fact that I use the English ”not” at the start does not imply it is the negation of anything. I could have named the new predicate hello(x) if I wanted. Now, if we had defined orphan(x) as in the previous question, one would be able to formally prove that the formula ∀x(¬orphan(x) ⇔ notOrphan(x)) is a indeed tautology!
(f) x is someone’s mother.
(g) x is someone’s son. Solution: Your turn!
(h) x is a first cousin of y, that is, x and y have a common grandparent.
(i) x is a first or second cousin of y.
Solution: female(x)∧∃z parent(x,z)
and if we want to capture it in a new predicate, we can use the following formula:
∀x[isM other(x) ⇔ f emale(x) ∧ ∃z parent(x, z)]
Solution: ∃z∃w∃vparent(w,x)∧parent(v,y)∧(w̸=v)∧parent(z,w)∧parent(z,v) and if we want to capture it in a new predicate, we can use the following formula:
∀x, y[cousin(x, y) ⇔ ∃z∃w∃v parent(w, x) ∧ parent(v, y) ∧ (w ̸= v) ∧ parent(z, w) ∧ parent(z, v)]
Solution:
(∃z∃w∃v parent(w, x) ∧ parent(v, y) ∧ (w ̸= v) ∧ parent(z, w) ∧ parent(z, v)) ∨ (∃z∃w∃v∃u∃t parent(w, x) ∧ parent(v, y) ∧ parent(u, w) ∧ parent(t, v) ∧
(u ̸= t) ∧ parent(z, u) ∧ parent(z, t))
RMITAI2021(Semester2)-SebastianSardin ̃a Exercise2continuesonthenextpage…
COSC1127/1125 – AI Tutorial 5: KR&R II – First Order Logic Page 7 of 17
and if we want to capture it in a new predicate, we can use the following formula:
∀x, y[f s cousin(x, y) ⇔
(∃z∃w∃v parent(w, x) ∧ parent(v, y) ∧ (w ̸= v) ∧ parent(z, w) ∧ parent(z, v)) ∨
(∃z∃w∃v∃u∃t parent(w, x) ∧ parent(v, y) ∧ parent(u, w) ∧ parent(t, v) ∧ (u ̸= t) ∧ parent(z, u) ∧ parent(z, t))]
(j) x is an ancestor of y.
(k) x is a descendant of y. Solution: Your turn!
(l) All of x’s grandchildren are male.
Solution: ∀y∀z(parent(x,y)∧parent(y,z))⇒male(z)
(m) x does not have any grandparents.
Solution: ¬∃y∃zparent(y,x)∧parent(z,y)
If you are keen, you can try executing some similar definitions using the language Prolog. Download and install a Prolog interpreter (a good one is SWI-Prolog), and load the file family.pl available here. The syntax may take a little getting used to, but in this file you will find various definitions like those in the previous question.
PART3: Unification……………………………………………………………………….
(a) Give the most general unifier (MGU) for the following pairs of expressions, or say why it does not exist. In all of these expressions variables are lower-case x, y, or z.
i. p(a,b,b),p(x,y,z). Solution:
Solution: This can only be done by defining the relationship “recursively”, i.e. in term of itself: ∀x, y[ancestor(x, y) ⇔ (parent(x, y) ∨ ∃z(parent(x, z) ∧ ancestor(z, y)))]
However, it is important to note that this formula would actually not work in predicate logic, that is, it will not correctly define the ancestor notion in terms of the parent one. This is because FOL/predicate logic is not expressive enough to capture Transitive Closure (but this is out of the scope of the course).
RMITAI2021(Semester2)-SebastianSardin ̃a Exercise3continuesonthenextpage…
COSC1127/1125 – AI Tutorial 5: KR&R II – First Order Logic Page 8 of 17
To find the MGU, we use the algorithm described here.
S0 ={p(a,b,b),p(x,y,z)} D0 = {a, x}
σ = {x/a}
S1 ={p(a,b,b),p(a,y,z)}
D1 = {b, y}
σ = {x/a, y/b}
S2 ={p(a,b,b),p(a,b,z)} D3 = {b, z}
σ = {x/a, y/b, z/b}
S3 = {p(a, b, b), p(a, b, b)}
[first disagreement set]
[second disagreement set]
[third disagreement set]
No disagreement, MGU found! σ = {x/a, y/b, z/b}.
Observe that σ′ = {x/a,y/b,z/y} is not an MGU because it is not even a unification of both structures. In fact, p(x, y, z)σ = p(a, b, b) ̸= p(x, y, z)σ′ = p(a, b, y).
ii. q(y,g(a,b)),q(g(x,x),y).
Solution:
S0 ={q(y,g(a,b)),q(g(x,x),y)} D0 = {y, g(x, x)}
σ = {y/g(x, x)}
S1 ={q(g(x,x),g(a,b)),q(g(x,x),g(x,x))}
D1 = {g(a, b), g(x, x)}
No unifier (x cannot bind to both a and b).
[first disagreement set]
[second disagreement set]
iii. older(father(y),y),older(father(x),john).
iv. knows(father(x),y),knows(x,x).
v. r(f(a),b,g(f(a))),r(x,y,z). Solution: Your turn!
vi. older(father(y),y),older(father(y),john).
Solution: Your turn!
If you still need additional guidance, please check this video. However, note that if you needed to rely on the video, then there was probably insufficient learning. The best & expected case would be that you use the video to verify your approach.
Solution:
No unifier, because the occurs-check prevents unification of x with father(x)
S0 ={knows(father(x),y),knows(x,x)}
D0 = {f ather(x), x)} [first disagreement set]
RMITAI2021(Semester2)-SebastianSardin ̃a Exercise3continuesonthenextpage…
COSC1127/1125 – AI Tutorial 5: KR&R II – First Order Logic Page 9 of 17
Solution:
S0 = {older(father(y),y),older(father(y),john)} D0 = {y, john}
σ = {y/john}
S1 = {older(father(john),john),older(father(john),john)}
No disagreement, MGU found! σ = {y/john}.
[first disagreement set]
vii. f(g(a,h(b)),g(x,y)),f(g(z,y),g(y,y)). Solution: Your turn!
(b) Somemore(y,w,z,v,uareallvariables): i. p(f(y),w,g(z)),p(v,u,v).
ii. p(f(y),w,g(z)),p(v,u,x). Solution: Your turn!
iii. p(a,x,f(g(y))),p(z,h(w),f(w)).
iv. p(z,h(w),g(z)),p(v,u,v). Solution: Your turn!
v. p(a,h(w),f(g(y))),p(z,x,f(w)).
PART 4: Representation and reasoning……………………………………………………..
(a) Write down logical representations for the following sentences, suitable for use with generalised modus ponens. Pay special attention to implications and quantification.
i. Horses, cows and pigs are mammals.
ii. An offspring of a horse is a horse.
iii. Bluebeard is a horse.
iv. Bluebeard is Charlie’s parent.
Solution:
Impossible as v has to match both f(y) and g(z) and f and g are different symbols.
Solution:
{z/a, x/h(w), w/g(y)}
Solution:
{z/a, x/h(w), w/g(y)}
Solution:
∀x[Horse(x) ⇒ Mammal(x)] ∀x[Cow(x) ⇒ Mammal(x)] ∀x[Pig(x) ⇒ Mammal(x)]
Solution:
∀x, y[Offspring(x, y) ∧ Horse(y) ⇒ Horse(x)]
Solution:
Horse(bluebeard)
RMITAI2021(Semester2)-SebastianSardin ̃a Exercise4continuesonthenextpage…
COSC1127/1125 – AI Tutorial 5: KR&R II – First Order Logic Page 10 of 17
Solution: Your turn!
v. Offspring and parent are inverse relations.
vi. Every mammal has a parent.
Solution: Your turn!
(b) Using the logical expressions from the previous question do the following:
i. Draw the proof tree using backward chaining (that is, starting from your query) for the query “there
exists a horse” – (∃x)Horse(x).
Solution:
The proof tree is shown below. The branch with Of f spring(bluebeard, y) and P arent(y, bluebeard) repeats indefinitely, so the rest of the proof is never reached.
ii. Repeat the proof using forward chaining (that is, start with the facts and derive further conclusions). Do you get the the same results as before?
Solution: Your turn!
iii. How many solutions for H are there?
(c) A popular children’s riddle is “Brothers and sisters I have none, but that man’s father is my father’s son”. Use the rules of the kinship domain to work out who that man is.
(d) For the following Wumpus world:
Solution:
∀x, y[Of f spring(x, y) ⇒ P arent(y, x)] ∀x, y[P arent(x, y) ⇒ Of f spring(y, x)
Solution:
Both bluebeard and charlie are horses.
Solution:
The son (of the man speaking).
RMITAI2021(Semester2)-SebastianSardin ̃a Exercise4continuesonthenextpage…
COSC1127/1125 – AI Tutorial 5: KR&R II – First Order Logic Page 11 of 17
i. Develop a notation capturing the important aspects of this domain in first order logic.
ii. How would you express in a first order logic sentence:
α) If a square has no smell then the Wumpus is not in this square or any of the adjacent squares?
β) If there is stench in a square there must be a Wumpus in this square or in one of the adjacent squares?
iii. Suppose the agent has traversed the path (1, 1) ⇒ (1, 2) ⇒ (2, 2) ⇒ (1, 2). How can the agent deduce that the Wumpus is in square [1,3] using the laws of inference of first order logic?
PART5: Resolutionproofs………………………………………………………………… As with propositional logic, applying resolution to first-order logic formulas requires that they be first converted to conjunctive normal form. This is a bit more complicated when dealing with predicates however, because of the existential and universal quantifiers. We need to find a certain kind of reduction from first-order logic to propositional logic, in order to use the principles of resolution to prove our statements, and Herbrand’s theorem provides us with such a reduction. However, this theorem applies to the domain closure of a set of formulas with no quantifier, so in order to apply it, we need a way to remove quantifiers from first-order logic forumulas.
Basically, a first-order clause (disjunction of literals) is always assumed to be universally quantified. So, if a clause like (P (x) ∨ ¬Q(x, y) ∨ R(y)) stands for the sentence ∀x, y.(P (x) ∨ ¬Q(x, y) ∨ R(y)). So, when
Solution: (Note: this is a partial solution)
Similar to previous tutorial for propositional logic but now stated using first order.
Solution:
∀x[¬Smell(x) ⇒ ∀y((Adjacent(x, y) ∨ x = y) ⇒ ¬W umpusAt(y))].
Solution:
∀x[Smell(x) ⇒ ∃y((Adjacent(x, y) ∨ x = y) ∧ W umpusAt(y))].
Solution: It follows from (β) above and the fact that the knowledge base includes or entails:
Adjacent((1, 3), (1, 2))
Smell((1, 2))
¬W umpusAt((1, 1))
¬Smell((2, 2))(or directly ¬W umpusAt((2, 2)))
RMITAI2021(Semester2)-SebastianSardin ̃a Exercise5continuesonthenextpage…
COSC1127/1125 – AI Tutorial 5: KR&R II – First Order Logic Page 12 of 17 the only quantifiers we have are universal, this is easy: if we have a sentence ∀x.P(x) ∨ Q(y), its clausal
representation is just (P (x) ∨ Q(y)). Similarly, ∀x.P (x) ⇒ Q(x) can be written in CNF as (¬P (x) ∨ Q(x)).
Where it becomes more complicated is when we are using the existential quantifier. If we have a formula ∃x.P(x), we cannot just write clause P(x), sa that clause stands for ∀x.P(x). This is where the idea of Skolemisation comes in. As ∃x.P (x) ∨ Q(x) says that “there exists some value of x“ for which P (x) ∨ Q(x) is true, we can assume a “witness” value representing such value, and hence use a constant A, so-called the Skolem constant for such x, for this value and write P (A) ∨ Q(A).
Now, what happens with a formula like ∀x, ∃y.(P (x) ∧ Q(y))? The fact is that the value of y that makes the formula true, will depend on each specific x. So, when dealing with formulas that mix quantifiers, we need to use a so-called Skolem function, to indicate that the element we are claiming to exist depend on the value of the previously universally quantified variables. A Skolem function is an n-place function, where n is the number of universal quantifiers that appear before the existentially quantified variable.
For example:
[∀x.P (x) ⇒ ∃y.Q(y) ∧ R(x, y)] ≡[P (x) ⇒ Q(f (x)) ∧ R(x, f (x))] [∀x∀y.P (x, y) ⇒ ∃z.Q(z) ∧ R(x, z)] ≡[P (x, y) ⇒ Q(f (x, y)) ∧ R(x, f (x, y))]
[∀x.P (x) ⇒ ∃y∀z.(Q(y) ∧ R(y, z))] ≡[P (x) ⇒ (Q(f (x)) ∧ R(f (x), z))] [∃x∀y∀z.P (x) ∧ (Q(y) ⇒ R(x, z))] ≡[P (A) ∧ (Q(y) ⇒ R(A, z))]
In this last example, we use the Skolem constant A, as there is no universal quantifier that occurs before the existential quantifier. Of course, these examples are only used to demonstrate how to remove the quantifiers from these formulas; in order to apply resolution, we must also convert them into CNF.
When doing KRR below, we take information given in English and represent such information in first-order logic. We then suitably convert the resulting formulas so we can perform resolution, by transforming the formulas to CNF + Skolemization. Finally, we construct a resolution proof for the query of concern. There are fully work examples in the book (Section 9.5 – Resolution).
(a) Consider the following sentences: 1. Marcus was a man.
2. Marcus was a Roman.
3. All men are people.
4. Caesar was a ruler.
5. All Romans were either loyal to Caesar or hated him (or both). 6. Everyone is loyal to someone.
7. People only try to assassinate rulers they are not loyal to.
8. Marcus tried to assassinate Caesar. Carry out the following tasks:
i. Converteachofthesesentencesintofirst-orderlogicandthenconverteachformulaintoclausalform. Indicate any Skolem functions or constants used in the conversion.
Solution:
First-order sentences:
1. Man(marcus)
2. Roman(marcus)
3. ∀x.Man(x) ⇒ Person(x).
4. Ruler(caesar).
5. ∀x.Roman(x)⇒Loyal(x,caesar)∨Hate(x,caesar). 6. ∀x.∃y.Loyal(x,y)
7. TryKill(x,y)⇒Ruler(y)∧¬Loyal(x,y)
8. TryKill(marcus,caesar).
RMITAI2021(Semester2)-SebastianSardin ̃a Exercise5continuesonthenextpage…
COSC1127/1125 – AI Tutorial 5: KR&R II – First Order Logic Page 13 of 17 ii. Convert the negation of the question “Who hated Caesar?” into causal form (with an answer literal)
Solution:
Conversions to CNF:
1. Man(marcus)
2. Roman(marcus)
3. ¬Man(x)∨Person(x).
4. Ruler(caesar).
5. ¬Roman(x)∨Loyal(x,caesar)∨Hate(x,caesar).
6. Loyal(x,f(x))
(as the existential quantifier ∃y is within the scope of the universal quantifier ∀x, a Skolem function f (x) must be substituted for the variable y in order to remove the existential quanti- fier)
7. (¬TryKill(x,y)∨Ruler(y))and(¬TryKill(x,y)∨¬Loyal(x,y)).
8. TryKill(marcus,caesar).
iii. Derive the answer to this question using first-order resolution. Give the answer in English. In the proof use the notation developed in lectorials.
Solution: (Note: this is a partial solution)
Query: ∃z.Hate(z, caesar).
Query with answer predicate: ∃z.[Hate(z, caesar) ∧ ¬A(z)]. Negation of query with answer predicate: ¬Hate(z, caesar) ∨ A(z)
The resolution follows easily until we get a clause A(marcus): Marcus hated Caesar.
1. {M an(marcus)}
2. {Roman(marcus)}
3. {¬M an(x), P erson(x)}
4. {Ruler(ceasar)}
5. {¬Roman(x), Loyal(x, caesar), Hate(x, caesar)}
6. {Loyal(x, f (x))}
7. {¬T ryKill(x, y), Ruler(y)}
8. {¬T ryKill(x, y), ¬Loyal(x, y)}
9. {T ryKill(marcus, caesar)}
10. {¬Hate(z, caesar), A(z)}
11. {Loyal(marcus, caesar), Hate(marcus, caesar)}
12. {¬Loyal(marcus, caesar)}
13. ….
14. ….
Now, represent this resolution proof as a resolution graph!
clause from KB
clause from KB
clause from KB
clause from KB
clause from KB
clause from KB
clause from KB
clause from KB
clause from KB
negated query with answer predicate
resolve 2,5 with σ = {x/marcus}
resolve 8,9 with σ = {x/marcus, y/caesar} resolve ….
resolve ….
(b) Determine whether the following sentence is valid (i.e., a tautology) using FOL Resolution:
∃x∀y∀z((P (y) ⇒ Q(z)) ⇒ (P (x) ⇒ Q(x))).
Solution:
Please check this video that explains this solution in more detail.
Because the existential quantifier is outside the scope of both universal quantifiers, we don’t need to use a Skolem function, just a Skolem constant. Here we will use the constant A, and the substitution x/A.
RMITAI2021(Semester2)-SebastianSardin ̃a Exercise5continuesonthenextpage…
COSC1127/1125 – AI Tutorial 5: KR&R II – First Order Logic Page 14 of 17
∀y∀z[(P (y) ⇒ Q(z)) ⇒ (P (A) ⇒ Q(A))]
We have an over-all implication of (P (y) ⇒ Q(z)) ⇒ (P (A) ⇒ Q(A)), where (P (y) ⇒ Q(z)) is the
antecedent and (P (A) ⇒ Q(A)) is the consequent (what we’re trying to prove). Putting the antecedent into CNF gives:
¬P (y) ∨ Q(z)
Putting the the consequent into CNF gives:
¬P (A) ∨ Q(A)
As we are trying to prove the consequent by refutation, we must negate it: P (A) ∧ ¬Q(A)
Which gives us the clauses:
1. {¬P(y),Q(z)}
2. {P(A)}
3. {¬Q(A)}
Finally, we can solve this by resolution:
4. {Q(z)} [1,2]
5. {} [3,4]
As we have derived the empty set using resolution, it must be a tautology.
(c) (From [Brachman and Levesque 2005]) Victor has been murdered, and Arthur, Bertram, and Carleton are the only suspects (meaning exactly one of them is the murderer). Arthur says that Bertram was the victim’s friend, but that Carleton hated the victim. Bertram says that he was out of town the day of the murder, and besides, he didn’t even know the guy. Carleton says that he saw Arthur and Bertram with the victim just before the murder. You may assume that everyone—except possibly for the murderer—is telling the truth.
You are also given the following general facts:
• anyone who was with Victor on the day of the murder, must have been in town;
• a person who is with someone, must also know them; • a friend knows the person who they call a friend;
• a person who hates someone must also know them.
You should use the following set of predicates when expressing the general facts and statements made by the suspects:
• I(x): means x is innocent;
• F(x,y): means x is a friend of y; • H(x, y): means x hates y;
• T(x):meansxisintown;
• K(x, y): means x knows y; and
• W(x,y): means x is with y.
i. Use Resolution to find the murderer. In other words, formalize the facts as a set of clauses, prove that there is a murderer (here, we assume that there is only one murderer), and extract their identity from
RMITAI2021(Semester2)-SebastianSardin ̃a Exercise5continuesonthenextpage…
COSC1127/1125 – AI Tutorial 5: KR&R II – First Order Logic Page 15 of 17 the derivation.
Solution: (Note: this is a partial solution)
If we assume that if someone is innocent, then they are telling the truth, we can derive the following formulas from the statements given:
i. I(Arthur)⇒F(Bertram,Victor)∧H(Carleton,Victor) ii. I(Bertram)⇒¬T(Bertram)∧¬K(Bertram,Victor)
iii. I(Carleton)⇒W(Arthur,Victor)∧W(Bertram,Victor)
Converting these to CNF and putting into set form we have:
i. {¬I(Arthur),F(Bertram,Victor)},{¬I(Arthur),H(Carleton,Victor)}
ii. {¬I(Bertram),¬T(Bertram)},{¬I(Bertram),¬K(Bertram,Victor)} iii. …………
From the four general facts we are given, we can obtain the formulas: iv. ∀x.W(x,Victor)⇒T(x)
v. ∀x∀y.W(x,y)⇒K(x,y) vi. …………
vii. …………
Converting these to CNF and putting into set form we have: iv. {¬W(x,Victor),T(x)}
v. {¬W(x,y),K(x,y)} vi. {¬F(x,y),K(x,y)} vii. {¬H(x,y),K(x,y)}
Finally, we assume that there is one and only one murderer, and it must be one of Arthur, Bertram or Carleton, which we can express as:
viii. ∀x.¬I(x) ⇒ x = Arthur ∨ x = Bertram ∨ x = Carleton ix. ∀x∀y.¬I(x) ∧ ¬I(y) ⇒ x = y
x. ¬I(Arthur)∨¬I(Bertram)∨¬I(Carleton)
Converting these to CNF and putting into set form we have: viii. …………
ix. {I(x),I(y),x=y}
x. {¬I(Arthur),¬I(Bertram),¬I(Carleton)}
We also need to assert that Arthur, Bertram, Carleton, and V ictor are all different people! This gives rise to the following unit clauses:
xi. {¬(Arthur = Bertram)}, {¬(Arthur = Carleton)}, {¬(Arthur = V ictor)}, . . .
All the above formulas (i) to (xi) compromise the knowledgebase representing what is known about the case.
Finally, we want to find whether someone is guilty and who that person is (Victor is dead, after all!). So, our query is:
∃x.¬I (x)
The negated query is then ∀x.I(x) (everyone is innocent!), which with the answer predicate in- cluded, yields the following clause to be considered:
{I (x), A(x)}
Remember to complete the missing . . . parts above first!
Next, let’s do the resolution proof (yellow highlighted formulas come from the knowledgebase (i)- (xi); yellow highlighted represents the clause coming from the query):
RMITAI2021(Semester2)-SebastianSardin ̃a Exercise5continuesonthenextpage…
COSC1127/1125 – AI Tutorial 5: KR&R II – First Order Logic Page 16 of 17
With time, my proof has been partly faded out… can you fill the gaps?
One can also do a so-called model-theoretic proof, by analysing what would need to be true in any model of the knowledgebase, that, any interpretation that makes formulas (i) to (xi) true.
Suppose that M is a model of all formulas (i)-(xi), and suppose further that M |= I(Bertram), that is Bertram is innocent in interpretation M.
Then, due to (ii), we know that M |= ¬T(Bertram) This together with (iv) implies that M |= ¬W (Bertram, V ictor). Due to (ii), we derive then that M |= ¬I(Carleton).
Also due to (ii) and the fact that M |= I(Bertram), we conclude that …………. This together with (vi) implies that …………. Due to (i), we conclude M |= ¬I(Arthur).
So, we have M |= ¬I(Arthur) ∧ ¬I(Carleton), that is, both Arthur and Carleton are guilty! Using formula (ix), ………… But that is not the case, as we know from formula (xi) that M |= ¬(Arthur = Carleton)!
So, we reach a contradiction and hence it cannot be the case that ………… Thus, any model M oftheknowledgeable(i)-(xi)mustbesuchthat …………,andBertramisthereforeguilty!
(Note that, using (ix) and (xi), we can derive that M |= I(Arthur) and M |= I(Carleton).
ii. Suppose we discover that we were wrong—we cannot assume that there was only a single murderer (there may have been a conspiracy). Show that in this case the facts do not support anyone’s guilt. In other words, for each suspect, present a logical interpretation that supports all the facts, but where that suspect is innocent (and maybe the other two are guilty!).
Solution:
Here, we no-longer know that there was only one murderer: there could be more than one. So, we drop constraint formula (ix.) above.
Under the new formalization (i.e., previous formalization except formula ix.), we are to show that there is no-one who is definitively guilty. Technically, for each individual suspect, we construct an interpretation, a ”possible world”, that is compatible with all the information at hand, but under
RMITAI2021(Semester2)-SebastianSardin ̃a Exercise5continuesonthenextpage…
COSC1127/1125 – AI Tutorial 5: KR&R II – First Order Logic Page 17 of 17
which the suspect is indeed innocent.
So, let’s prove that, in the new formalization, Bertram can indeed be innocent. Take any interpre- tation M such that:
• I(Bertram) is true, but I(Arthur) and I(Carleton) are false in M. That is, Bertram is innocent and the other two are guilty! Observe this is now possible because we don’t have to satisfy formula ix. anymore: a conspiracy is possible!
• T(Bertram),W(Bertram,Victor),F(Bertram,Victor)andH(Bertram,Victor)are false in M.
The truth value of the remaining predicate instances can chosen arbitrary to finish interpretation M , for example, everything else can be false in M. On can then verify that M indeed satisfies all the formulas of the formalization (except for ix. which is left out in this exercise). Thus, unlike in the previous part, we now cannot conclude with certainty that Bertram was the murderer, as we have just showed a possible way things could turn out to be where Bertram is innocent.
Now your turn to show the other two cases, that is, one interpretation under which Arthur is innocent, and one in which Carleton is innocent!
Question: could there have been a conspiracy if Arthur is innocent?
RMIT AI 2021 (Semester 2) – ̃a
End of tutorial worksheet