/Users/billy/gits/moc-2021/problem-sets/ps06.dvi
School of Computing and Information Systems
COMP30026 Models of Computation Problem Set 6
30–27 August 2021
Content: resolution for predicate logic, clausal form, skolemization, unification.
P6.1 For each of the following pairs of terms, determine whether the pair is unifiable. If it is, give
the most general unifier.
(i) h(f(x), g(y, f(x)), y) and h(f(u), g(v, v), u)
(ii) h(f(g(x, y)), y, g(y, y)) and h(f(u), g(a, v), u)
(iii) h(g(x, x), g(y, z), g(y, f(z))) and h(g(u, v), g(v, u), v)
(iv) h(v, g(v), f(u, a)) and h(g(x), y, x)
(v) h(f(x, x), y, y, x) and h(v, v, f(a, b), a)
(Don’t forget our agreed convention: for constants we use letters from the beginning of the
alphabet, here a and b, whereas for variables we use letters from the end of the alphabet.)
P6.2 Consider these statements:
S1: “No politician is honest.”
S2: “Some politicians are not honest.”
(a) Using the predicate symbols P andH for being a politician and being honest, respectively,
express the two statements as first order predicate formulas F1 and F2.
(b) Is F1 ⇒ F2 satisfiable?
(c) Is F1 ⇒ F2 valid?
(d) Consider these statements:
S3: “No Australian politician is honest.”
S4: “All honest politicians are Australian.”
Using the predicate symbol A for “is Australian”, express S3 and S4 in clausal form.
(e) Using resolution, show that S1 is a logical consequence of S3 and S4.
(f) Prove or disprove the statement “S2 is a logical consequence of S3 and S4.”
P6.3 Consider the following unsatisfiable set of clauses:
{{P (x)}, {¬P (x),¬Q(y)}, {Q(x),¬R(y)}, {R(x), S(a)}, {R(b),¬S(x)}}
What is the simplest refutation proof, if “simplest” means “the refutation tree has minimal
depth”? What is the simplest refutation proof, if “simplest” means “the refutation tree has
fewest nodes”?
P6.4 Consider the following predicates:
• E(x, y), which stands for “x envies y”
• F (x, y), which stands for “x is more fortunate than y”
(a) Using ‘a’ for Adam, express, in first-order predicate logic, the sentence “Adam envies
everyone more fortunate than him.”
(b) Using ‘e’ for Eve, express, in first-order predicate logic, the sentence “Eve is no more
fortunate than any who envy her.”
(c) Formalise an argument for the conclusion that “Eve is no more fortunate than Adam.”
That is, express this statement in first-order predicate logic and show that it is a logical
consequence of the other two.
P6.5 Using the unification algorithm, determine whether Q(f(g(x), y, f(y, z, z)), g(f(a, y, z))) and
Q(f(u, g(a), v), u) are unifiable. If they are, give a most general unifier. (As usual, we use
letters from the end of the alphabet for variables, and letters from the beginning of the
alphabet for constants.)
P6.6 Determine whether P (f(g(x), f(g(x), g(a))), x) and P (f(u, f(v, v)), u) are unifiable. If they
are, give a most general unifier.
P6.7 Here is an example of a refutation proof where factoring will be needed. Let us try to capture
Bertrand Russell’s ”barber paradox” as a formula in first order predicate logic. Let B(x)
mean “x is a barber” and let S(u, v) mean “u shaves v”. We want to express that barbers
shave people who do not shave themselves, and also, no barber shaves someone who shaves
themself. That is:
∀x, y
(
B(x)⇒ (S(y, y)⊕ S(x, y))
)
(1)
Turn this formula into clausal form. Then use resolution (with factoring) to show that there
are no barbers! That is, show that ¬∃v B(v) is a logical consequence of the formula (1).
P6.8 Let pi be the ith prime number and consider this conjecture: p1p2 · · · pk + 1 is always prime,
that is, when we add 1 to the product of the first k prime numbers, we get a new prime
number. This statement is really a universally quantified statement; it says “for all k, 1 + the
product of the first k primes is prime.”
If the conjecture is wrong, we can hope to use Haskell to show this, by finding a counter-
example. In general, we may be able to use Haskell to refute “universal” claims, or, equiva-
lently, to prove “existential” claims.
(a) Can we program our way out of proving “universal” claims with the same ease?
(b) Does the conjecture hold?
A prime pair is a pair (p, p+ 2) where both p and p+ 2 are prime.
(c) (Optional.) Use Haskell to find the first 50 prime pairs.
While we know that there are infinitely many primes, it is not known whether there are
infinitely many prime pairs.
A prime triple is a triple (p, p+ 2, p+ 4) with p, p+ 2, and p+ 4 all prime. Here is a Haskell
definition of the list of all prime triples, assuming we have already defined primes, the list of
all primes:
primeTriples :: [(Integer,Integer,Integer)]
primeTriples
= triple primes
where
triple (x:y:z:xyzs)
| x+2 == y && y+2 == z = (x,y,z) : triple (y:z:xyzs)
| otherwise = triple (y:z:xyzs)
(d) What happens when you evaluate primeTriples?
(e) Prove that there exists one and only one prime triple.
P6.9 (Optional, a bonus exercise for people who love algebra.) Work through the following more
substantial resolution example in your own time and make sure that you understand each
step. It is optional, but feel free to discuss the problem in a tutorial or the LMS Discussion
Forum if there are steps you don’t understand.
Dowsing, Rayward-Smith and Walter (see Readings Online on the LMS) give the following
example of a non-trivial proof using resolution. It is concerned with group theory. A group is
a set endowed with a binary operation ◦. If we use P (x, y, z) to mean x ◦ y = z then we can
write the so-called group axioms as follows:
∀x∀y∃z(P (x, y, z)) (closure)
∀x, y, z, u, v, w ([P (x, y, u) ∧ P (y, z, v)]⇒ [P (x, v, w)⇔ P (u, z, w)]) (associativity)
∃x∀y(P (x, y, y) ∧ ∃z(P (z, y, x))) (left identity
and left inverse)
Notice that the associativity axiom says that if x ◦ y = u and y ◦ z = v then x ◦ v = u ◦ z. In
other words, x ◦ (y ◦ z) = (x ◦ y) ◦ z. The last axiom says that there is some special element x
in the set, with the property that x ◦ y = y for all y (that is, this element is a neutral element
for ◦). Moreover, for each y there is a z such that z ◦ y yields that special element (in other
words, each element has a left inverse). For an example of a group, consider the set Z of
integers, endowed with the operation +.
We can translate the group axioms to clausal form. The first axiom (closure) becomes
{P (x, y, f(x, y))}
The second axiom (associativity) produces two clauses:
{¬P (x, y, u),¬P (y, z, v),¬P (x, v, w), P (u, z, w)}
{¬P (x, y, u),¬P (y, z, v),¬P (u, z, w), P (x, v, w)}
The last axiom (left identity and left inverse) also produces two clauses:
{P (a, y, y)}
{P (g(y), y, a)}
Suppose we want to prove that every element of a group also has a right inverse. That is, we
want to prove
∃x∀y∃z(P (y, z, x))
from the axioms. To do this we first negate our formula, obtaining:
∀x∃y∀z(¬P (y, z, x))
In clausal form this becomes {¬P (h(x), z, x)}.
Below is the proof by resolution. It is a mechanical proof of a non-trivial theorem. When
there is ambiguity, I have used underlining to show which atom takes part in the resolution
step.
Make sure you understand each resolution step. Did the refutation make use of all the axioms?
If you try to do the proof on your own without looking at the proof above, you will find that
there are many blind alleys (most of them will end in failure due to the occur check). So you
will most likely take a long time, and do lots of back-tracking. With a computer of course we
find the refutation in a flash.
Notice how clauses have had their variables renamed to avoid name clashes. Try to track how
the variables x′ and z′ from the original query get bound during this proof.
¬P (x, y, u),¬P (y, z, v),¬P (x, v, w), P (u, z, w) ¬P (h(x′), z′, x′)
¬P (x, y, h(x′)),¬P (y, z′, v),¬P (x, v, x′) P (g(u), u, a)
¬P (g(u), y, h(a)),¬P (y, z′, u) P (a, u′, u′)
¬P (x2, y2, u2),¬P (y2, z2, v2),¬P (u2, z2, w2), P (x2, v2, w2) ¬P (g(u
′), a, h(a)
¬P (g(u′), y2, u2),¬P (y2, z2, a),¬P (u2, z2, h(a)) P (a, v′, v′)
¬P (g(u′), y2, a),¬P (y2, h(a), a) P (g(u3), u3, a)
¬P (u3, h(a), a) P (g(u4), u4, a)
⊥
u = h(x′)
w = x′
z = z′
x = g(u)
v = u
x′ = a
y = a
z′ = u′
u = u′
x2 = g(u
′)
v2 = a
w2 = h(a)
u2 = a
v′ = h(a)
z2 = h(a)
u′ = u3
y2 = u3
u3 = g(h(a))
u4 = h(a)