/Users/billy/gits/moc-2021/problem-sets/solps06.dvi
The University of Melbourne
School of Computing and Information Systems
COMP30026 Models of Computation
Sample Answers to Tutorial Exercises, Week 6
P6.1 (i) The pair of terms (h(f(x), g(y, f(x)), y), h(f(u), g(v, v), u)) is not unifiable. Applying
rule 1 (decomposition) to {h(f(x), g(y, f(x)), y) = h(f(u), g(v, v), u)}, we get
f(x) = f(u)
g(y, f(x)) = g(v, v)
y = u
Applying rule 1 (decomposition) again, to each of the first two equations, yields
x = u
y = v
f(x) = v
y = u
Applying rule 6 (substitution) with the first equation, we get
x = u
y = v
f(u) = v
y = u
Applying rule 4 (reorientation) to the third equation, followed by rule 6 to the result
yields
x = u
y = f(u)
v = f(u)
y = u
Applying rule 6 (substitution) with the last equation yields
x = u
u = f(u)
v = f(u)
y = u
Now the occur check applied to the second equation yields failure.
(ii) The pair of terms (h(f(g(x, y)), y, g(y, y)), h(f(u), g(a, v), u)) is unifiable. Applying
rule 1 (decomposition) to {h(f(g(x, y)), y, g(y, y)) = h(f(u), g(a, v), u)}, we get
f(g(x, y)) = f(u)
y = g(a, v)
g(y, y) = u
and a second application yields
g(x, y) = u
y = g(a, v)
g(y, y) = u
Applying rule 4 (reorientation) to the first and the third equation, we have
u = g(x, y)
y = g(a, v)
u = g(y, y)
Applying rule 6 (to the first equation) we then get
u = g(x, y)
y = g(a, v)
g(x, y) = g(y, y)
which, after an application of rule 1 gives
u = g(x, y)
y = g(a, v)
x = y
y = y
The last equation is dropped, by rule 3, and then rule 6 applied to the third equation
gives
u = g(y, y)
y = g(a, v)
x = y
Finally, rule 6 applied to the second equation gives
u = g(g(a, v), g(a, v))
y = g(a, v)
x = g(a, v)
This is a normal form and {u 7→ g(g(a, v), g(a, v)), y 7→ g(a, v), x 7→ g(a, v)} is the most
general unifier.
(iii) The pair of terms (h(g(x, x), g(y, z), g(y, f(z))), h(g(u, v), g(v, u), v)) is not unifiable.
Applying rule 1 (decomposition) to {h(g(x, x), g(y, z), g(y, f(z))) = h(g(u, v), g(v, u), v)},
we get
g(x, x) = g(u, v)
g(y, z) = g(v, u)
g(y, f(z)) = v
Applying rule 1 (decomposition) again, to each of the first two equations, yields
x = u
x = v
y = v
z = u
g(y, f(z)) = v
2
Applying rule 4 (reorientation) to the last equation, followed by rule 6 applied to v
yields
x = u
x = g(y, f(z))
y = g(y, f(z))
z = u
v = g(y, f(z))
Now the occur check (rule 5) applied to the third equation yields failure.
(iv) The pair of terms (h(v, g(v), f(u, a)), h(g(x), y, x)) is unifiable. Applying rule 1 (decom-
position) to {h(v, g(v), f(u, a)) = h(g(x), y, x)}, we get
v = g(x)
g(v) = y
f(u, a)) = x
Reorienting the last two equations:
v = g(x)
y = g(v)
x = f(u, a))
Now replacing x (rule 6):
v = g(f(u, a))
y = g(v)
x = f(u, a))
Finally replacing v (rule 6):
v = g(f(u, a))
y = g(g(f(u, a)))
x = f(u, a))
we have a normal form and {v 7→ g(f(u, a)), x 7→ f(u, a), y 7→ g(g(f(u, a)))} is the most
general unifier.
(v) The pair of terms (h(f(x, x), y, y, x), h(v, v, f(a, b), a)) is not unifiable. Applying rule 1
(decomposition) to {h(f(x, x), y, y, x) = h(v, v, f(a, b), a)}, we get
f(x, x) = v
y = v
y = f(a, b)
x = a
Reorienting the first equation yields
v = f(x, x)
y = v
y = f(a, b)
x = a
3
Now applying rule 6 to x and then to v, we get
v = f(a, a)
y = f(a, a)
y = f(a, b)
x = a
Now apply rule 6 to, say, the second equation and get
v = f(a, a)
y = f(a, a)
f(a, a) = f(a, b)
x = a
Decomposition (rule 1) then yields
v = f(a, a)
y = f(a, a)
a = a
a = b
x = a
Now the second-last equation gives match failure (rule 2 applies), and so the original
pair of terms were not unifiable.
P6.2 (a) The two statements
S1: “No politician is honest.”
S2: “Some politicians are not honest.”
become
F1 : ∀x (¬P (x) ∨ ¬H(x))
F2 : ∃x (P (x) ∧ ¬H(x))
(b) F1 ⇒ F2 is satisfiable. First let us simplify the formula. Normally it would be a good
idea to rename the bound variables, but in this case, it will be preferable to keep the x.
F1 ⇒ F2
≡ ∀x (¬P (x) ∨ ¬H(x))⇒∃x (P (x) ∧ ¬H(x)) spell out
≡ ¬∀x (¬P (x) ∨ ¬H(x)) ∨ ∃x (P (x) ∧ ¬H(x)) eliminate implication
≡ ∃x (P (x) ∧H(x)) ∨ ∃x (P (x) ∧ ¬H(x)) push negation in
≡ ∃x ((P (x) ∧H(x)) ∨ (P (x) ∧ ¬H(x))) ∃ distributes over ∨
≡ ∃x (P (x) ∧ (H(x) ∨ ¬H(x))) factor out P (x)
≡ ∃x P (x) eliminate trivially true conjunct
For this formula we can clearly find an interpretation that makes it true. For example,
take the domain {alf , bill , charlie} and let P and H hold for all elements. Or, take the
domain Z, let P stand for “is a prime” and let H stand for “is zero”.
(c) F1 ⇒ F2 is not valid. It is easy to find an interpretation that makes ∃x P (x) false. For
example, take the domain {alf , bill , charlie} and let P hold for none of the elements (H
can be given any interpretation). Or, take the domain Z, let P stand for “is an even
prime greater than 2” and let H stand for “is zero”.
4
(d) The statements
S3: “No Australian politician is honest.”
S4: “All honest politicians are Australian.”
can be expressed
S3: ∀x ((A(x) ∧ P (x))⇒¬H(x))
S4: ∀y ((P (y) ∧H(y))⇒A(y))
Each of these formulas corresponds to exactly one clause. The clausal forms are:
{{¬A(x),¬H(x),¬P (x)}}
{{A(y),¬H(y),¬P (y)}}
(e) We can show that S1 is a logical consequence of S3 and S4 by refuting S3∧S4∧¬S1. So let
us write ¬S1 in clausal form (note that we must apply the negation before “clausifying”;
the other way round generally gives an incorrect result):
¬∀x (¬P (x) ∨ ¬H(x))
∃x (P (x) ∧H(x)) push negation in
P (a) ∧H(a) Skolemize
Or, written as a set of sets: {{P (a)}, {H(a)}}. Added to the other clauses, these allow
us to complete the proof by resolution:
¬A(x),¬P (x),¬H(x) A(y),¬P (y),¬H(y) P (a) H(a)
¬P (x),¬H(x)
¬H(a)
⊥
(f) The statement “S2 is a logical consequence of S3 and S4” is false. We can show this by
constructing an interpretation which makes S3 and S4 true, while making S2 false. Any
interpretation with domain D, in which P is false for all elements of D, will do.
P6.3 (We should rename clauses apart, but in this case, no confusion arises, so we omit that.)
We can construct the refutation in 5 resolution steps, that is, the refutation tree has only 5
internal nodes:
Px ¬Px,¬Qy Qx,¬Ry Rx, Sa Rb,¬Sx
¬Qy
¬Ry
Sa
Rb
⊥
5
Here is another way (5 steps), in which the depth of the refutation tree is somewhat smaller:
Px ¬Px,¬Qy Rx, Sa Qx,¬Ry Rb,¬Sx
¬Qy Qx, Sa Qx,¬Sz
Qx
⊥
NB: variable renamed
With factoring, we can do it in 4 resolution steps, plus one factoring step:
Px ¬Px,¬Qy Qx,¬Ry Rx, Sa Rb,¬Sx
¬Qy Rb
Qx
⊥
Rx,Rb factored
P6.4 (a) ∀x (F (x, a)⇒ E(a, x))
(b) ∀x (E(x, e)⇒¬F (e, x))
(c) We capture “Eve is no more fortunate than Adam” as ¬F (e, a). To show that this is
a logical consequence of the other two statements, we need to show that every model
of ∀x (F (x, a) ⇒ E(a, x)) ∧ ∀x (E(x, e) ⇒ ¬F (e, x)) makes F (e, a) false. Assume (for
contradiction) that there is a model in which F (e, a) is true. Then, by the left conjunct,
E(a, e) is also true in this model. But then, by the right conjunct, ¬F (e, a) is also true,
that is, F (e, a) is false. But this is a contradiction, so F (e, a) must be false. Indeed a
proof by resolution is easy:
¬F (x, a), E(a, x) ¬E(x′, e),¬F (e, x′) F (e, a)
¬F (e, a)
⊥
6
P6.8 If you haven’t used Haskell to solve this problem, it is not too late!
(a) We can hope to prove an existential claim by brute force, by using Haskell to enumerate
candidate witnesses. If a witness appears in a reasonable time we are done. There is no
obvious way to refute an existential claim that way, nor to prove a universal claim.
(b) The conjecture is false. The easiest way to get to that conclusion is to write the con-
jecture as a Haskell expression
conjecture k = elem (product (take k primes) + 1) primes
(assuming we have defined primes) and then check, say: map conjecture [1..10] and
see what happens. We find that it fails for k = 6.
(c) Easy, if we let Haskell do the work:
(3,5), (5,7), (11,13), (17,19), (29,31), (41,43), (59,61), (71,73), (101,103), (107,109),
(137,139), (149,151), (179,181), (191,193), (197,199), (227,229), (239,241), (269,271),
(281,283), (311,313), (347,349), (419,421), (431,433), (461,463), (521,523), (569,571),
(599,601), (617,619), (641,643), (659,661), (809,811), (821,823), (827,829), (857,859),
(881,883), (1019,1021), (1031,1033), (1049,1051), (1061,1063), (1091,1093), (1151,1153),
(1229,1231), (1277,1279), (1289,1291), (1301,1303), (1319,1321), (1427,1429), (1451,1453),
(1481,1483), (1487,1489).
(d) Haskell generates the triple (3,5,7) and then stalls.
(e) … and for good reason, as there are no other prime triples. However, we can’t hope to
use Haskell to prove that! Instead we have to think.
Here is why there cannot be any prime triples other than (3, 5, 7). Assume that p > 3.
Out of p, p + 2, and p + 4, one must be divisible by 3, and so it is not a prime. The
following table shows all the possible remainders of the three numbers, after division
by 3:
p 0 1 2
p+ 2 2 0 1
p+ 4 1 2 0
In all cases, one of the three is divisible by 3.
Notice that this proof is not by brute force. Its critical step is to identify an essential
property of prime triples and use that, rather than simply enumerate-and-test.
7