TDDC36 (L OGIC ): E XAM
Solutions to Exercises
E XERCISE 1
1. Prove the following propositional formula
[P (Q R)] [(P Q) R]
(a) (2 points) using tableaux
(b) (2 points) using Gentzen system (as provided in the book or during lectures
- up to your choice).
2. Prove the following formula of predicate logic, where a, b are constants:
xyz[R(x, y, z) S(x) T (y)] x[R(x, a, b) T (a)]
(a) (3 points) using tableaux
(b) (3 points) using resolution.
S OLUTION TO 1( A )
We first negate the formula:
h
i
[P (Q R)] [(P Q) R]
[P (Q R)] [(P Q) R]
P (Q R) (P Q) R
P (Q R) P Q R.
Next, we construct a tableau for the negated formula:
P (Q R) P Q R
(-rule)
P, (Q R) P Q R
(-rule)
P, (Q R), P Q R
(-rule)
P, (Q R), P, Q, R
|
{z
}
closed
2(9)
TDDC36 (Logic) Exam: Solutions to Exercises
S OLUTION TO 1( B )
A possible proof:
( l)
[P (Q R)] [(P Q) R]
P (Q R) (P Q) R
(l)
P, (Q R) (P Q) R
(r)
P, (Q R) (P Q), R
(r)
P, (Q R), (P Q) R
(l)
P, (Q R), P, Q R
(l)
P, (Q R), Q R, P
|
{z
}
axiom
S OLUTION TO 2( A )
We first negate the formula:
h
i
xyz[R(x, y, z) S(x) T (y)] x[R(x, a, b) T (a)]
xyz[R(x, y, z) S(x) T (y)] x[R(x, a, b) T (a)]
xyz[R(x, y, z) S(x) T (y)] x[R(x, a, b) T (a)]
xyz[R(x, y, z) S(x) T (y)] x[R(x, a, b) T (a)].
Next, we construct a tableau for the negated formula:
xyz[R(x, y, z) S(x) T (y)] x[R(x, a, b) T (a)]
(-rule)
yz[R(c, y, z) S(c) T (y)] x[R(x, a, b) T (a)]
(-rule)
yz[R(c, y, z) S(c) T (y)] [R(c, a, b) T (a)]
(-rule)
z[R(c, a, z) S(c) T (a)] [R(c, a, b) T (a)]
(-rule)
[R(c, a, b) S(c) T (a)] [R(c, a, b) T (a)]
(-rule)
R(c, a, b), S(c) T (a) [R(c, a, b) T (a)]
(-rule)
R(c, a, b), S(c), T (a) [R(c, a, b) T (a)]
(-rule)
R(c, a, b), S(c), T (a), [R(c, a, b) T (a)]
.
& (-rule)
R(c, a, b), S(c), T (a), R(c, a, b)
R(c, a, b), S(c), T (a), T (a)
|
{z
}
|
{z
}
closed
closed
I DA
U NIVERSITY OF L INK OPING
3(9)
TDDC36 (Logic) Exam: Solutions to Exercises
S OLUTION TO 2(B)
We first negate the formula and obtain (see the solution for 2(a)):
xyz[R(x, y, z) S(x) T (y)] x[R(x, a, b) T (a)].
Now Skolemiztion for x results in:
yz[R(c, y, z) S(c) T (y)] x[R(x, a, b) T (a)],
so we have clauses:
(1) R(c, y, z)
(2) S(c)
(3) T (y)
(4) R(x, a, b) T (a)
A possible proof by resolution:
(5) R(x, a, b) (res) applied to (3), (4) with unification y = a
(6) FALSE
(res) applied to (1), (5) with unification
x = c, y = a, z = b.
I DA
U NIVERSITY OF L INK OPING
4(9)
TDDC36 (Logic) Exam: Solutions to Exercises
E XERCISE 2
1. (4 points) Translate the following sentences into a set of propositional formulas:
Boxes are small or medium.
Each box is red, green or blue.
Small boxes are blue or red.
Medium boxes are green or blue.
For shipment robots do chose red boxes.
For activities other than shipment robots chose neither blue nor green
boxes.
2. (2 points) Assuming that exactly one box is to be chosen hypothesize what
choice (size and color) can be made and explain your reasoning informally.
3. (4 points) Prove your claim formally using a proof system of your choice
(tableaux, Gentzen system or resolution). Please do not use truth table method,
as this will give no points).
S OLUTION TO 2.1
A possible translation:
small medium
red green blue
small (blue red)
medium (green blue)
shipment red
shipment (blue green).
(1)
S OLUTION TO 2.2
Observe that for shipment red boxes are chosen. For non-shipment neither blue nor
green boxes are chosen, so only red boxes remain. Therefore no matter whether for
shipment or not, red boxes are chosen.
We have only small or medium boxes. The chosen boxes are red, which excludes
medium boxes, (if a box is red then it is neither blue nor green). So one can chose only
boxes being both small and red.
S OLUTION TO 2.3
We use resolution. We first show that the set of formulas (1) implies red. We first
transform (1) into a set of clauses:
(1) small medium
(2) red green blue
(3) small blue red
(4) medium green blue
(5) shipment red
(6) shipment blue
(7) shipment green.
I DA
U NIVERSITY OF L INK OPING
5(9)
TDDC36 (Logic) Exam: Solutions to Exercises
Now we negate formula
[(1) (2) (3) (4) (5) (6) (7)] red
and obtain:
[(1) (2) (3) (4) (5) (6) (7)] red.
Therefore, we consider clauses (1) (7) together with
(8) red
A possible proof by resolution:
(9) shipment
(10) blue
(11) green
(12) green blue
(13) green
(14) FALSE
(res) applied to (5), (8)
(res) applied to (6), (9)
(res) applied to (7), (9)
(res) applied to (2), (8)
(res) applied to (10), (12)
(res) applied to (11), (13).
To prove that the chosen box is small we need formulas:1
red green
red blue
green blue
green red
blue green
blue red.
We could add all of them, but it suffices to take the first two. We also add the conclusion
red which is already proved to be the consequence of the initial set of clauses. Since
we want to prove that small is implied by our clauses, we also add its negation to the
set of clauses. The new clauses are:
(15) red
(16) red green
(17) red blue
(18) small.
A possible proof that the set of clauses leads to contradiction:
(19) green
(20) blue
(21) medium
(22) green blue
(23) blue
(24) FALSE
(res) applied to (15), (16)
(res) applied to (15), (17)
(res) applied to (1), (18)
(res) applied to (4), (21)
(res) applied to (19), (22)
(res) applied to (20), (24),
which completes the proof.
1
We assume that each box has one color, so a choice of a given box excludes boxes having a different
color.
I DA
U NIVERSITY OF L INK OPING
6(9)
TDDC36 (Logic) Exam: Solutions to Exercises
E XERCISE 3
Consider a set of persons and a relation R of being a relative of. Let
(a) the relation relative has the property that whenever person A is a relative of both
B and C then also B is a relative of C.
Consider the relation the same family member, denoted by F . We assume that
(b) whenever a person A is a relative of a person B then they are in the same family,
i.e., F (A, B) holds;
(c) everybody is in his/her family, i.e., for any person A we have F (A, A).
Using the provided information
(1) (3 points) express in predicate logic the properties (a), (b), (c)
(2) (2 points) provide informal arguments that R (as understood in real life) is
transitive and express in predicate logic the transitivity of R
(3) (5 points) using resolution, facts from points (1), (2) and the property:
h
i
xy R(x, y) z[R(x, z) R(z, y)]
prove that xy[F (x, y)].
S OLUTION TO 3(1)
(a) xyz[(R(x, y) R(x, z)) R(y, z)]
(b) xy[R(x, y) F (x, y)]
(c) x[F (x, x)]
S OLUTION TO 3(2)
The transitivity of R is expressed by:
xyz[(R(x, y) R(y, z)) R(x, z)].
The informal argument can be as follows. A relative is a person related by blood or
marriage. So, if x, y are relatives, there is a chain of persons x1 x2 . . . xk such
that:
x is related by blood or marriage to x1 ,
x1 related by blood or marriage to x2 ,
...
xk1 is related by blood or marriage to xk ,
xk is related by blood or marriage to y.
I DA
U NIVERSITY OF L INK OPING
7(9)
TDDC36 (Logic) Exam: Solutions to Exercises
If y and z are relatives then If y and z are relatives then there is a similar chain between
y and z. Therefore, there is a chain of persons relating x and z (the chain from x to y
plus the chain from y to z), i.e., x and z are relatives, too.
S OLUTION TO 3(3)
We have to show that the conjunction of formulas:
xyz[(R(x, y) R(x, z)) R(y, z)]
xy[R(x, y) F (x, y)]
x[F (x, x)]
xyz[(R(x,
y) R(y, z)) R(x, z)]
h
i
xy R(x, y) z[R(x, z) R(z, y)]
implies xy[F (x, y)].
To apply resolution we negate the conclusion, translate formulas into clauses and
try to derive the empty clause (FALSE). Below clauses (5), (6) are obtained from
xy[R(x, y) z[R(x, z) R(z, y)]] by Skolemizing this formula and transforming
into clauses. The clause (7) is a Skolemized negation of the conclusion, i.e., Skolemized xy[F (x, y)].
(1) R(x, y) R(x, z) R(y, z)
(2) R(x, y) F (x, y)
(3) F (x, x)
(4) R(x, y) R(y, z) R(x, z)
(5) R(x, y) R(x, f (x, y))
(6) R(x, y) R(f (x, y), y)
(7) F (a, b).
A possible proof by resolution:
(8) R(a, b)
(9) R(a, f (a, b))
(10) R(f (a, b), b)
(11) R(f (a, b), z) R(a, z)
(12) R(a, b)
(13) FALSE
(res) applied to (2), (7) with x = a, y
(res) applied to (5), (8) with x = a, y
(res) applied to (6), (8) with x = a, y
(res) applied to (4), (9) with x = a, y
(res) applied to (10), (11) with z = b
(res) applied to (8), (12),
=b
=b
=b
= f (a, b)
which completes the proof.
I DA
U NIVERSITY OF L INK OPING
8(9)
TDDC36 (Logic) Exam: Solutions to Exercises
E XERCISE 4
1. (2 points) Design a Datalog database for storing information about streets in
a town. Each street is characterized by its name, width and length. In addition,
for each street s the database contains information whether s is closed for traffic
as well as information about all streets intersecting s.
2. (1 point) Express in predicate calculus the constraint:
the relation of road intersection is symmetric
3. (1 point) Provide another exemplary integrity constraint concerning the relation
of road intersection.
4. Formulate in logic queries selecting:
(a) (2 point) all streets longer than 7km and wider than 3m, intersecting the
street named Kungsgatan;
(b) (4 points) all streets accessible by car from a given street, assuming that it
is impossible to drive through closed streets.
S OLUTION TO 4.1
The database contain relations:
street(id, name, width, length, closed), where id is a (unique) identifier for a
street, name String is its name, width, length N umbers are its width
and length, closed {true, f alse} indicates whether a given street i closed for
traffic,
intersects(id1, id2), where id1, id2 are street identifiers.
Example:
street(21,0 HanburySt.0 , 5, 300, F alse) a street which is not closed
for traffic
street(46,0 N obleSt.0 , 7, 200, T rue) a street which is closed for traffic
intersects(21, 46) streets 21 and 46 intersect each other.
S OLUTION TO 4.2
The relation of road intersection is symmetric:
xy[intersects(x, y) intersect(y, x)].
S OLUTION TO 4.3
Another exemplary integrity constraint concerning the relation of road intersection:
x[intersects(x, x)].
I DA
U NIVERSITY OF L INK OPING
9(9)
TDDC36 (Logic) Exam: Solutions to Exercises
S OLUTION TO 4.4( A )
Select all streets longer than 7km and wider than 3m, intersecting the street named
Kungsgatan (recall that is an anonymous dont care variable):
answer(id) : street(id, , W, L, ), W > 3, L > 7000,
street(id1, Kungsgatan, , , ), intersects(id, id1).
Now answer(X) provides all required streets.
S OLUTION TO 4.4( B )
Select streets accessible by car from a given street, assuming that it is impossible to
drive through closed streets. We first define:
accessible(id1, id2) : street(id1, , , , C1), C1 6= T rue,
street(id2, , , , C2), C2 6= T rue,
intersects(id1, id2).
accessible(id1, id2) : street(id1, , , , C1), C1 6= T rue,
street(id2, , , , C2), C2 6= T rue,
intersects(id1, id3), accessible(id3, id2).
Now, given a street, say Stone St., we can formulate the required query (assuming
that we are interested in street names, not identifiers):
answer(N ) : street(id, StoneSt., , , ),
street(id1, N, , , ), accessible(id, id1).
I DA
U NIVERSITY OF L INK OPING
