/Users/billy/gits/moc-2021/tutes/week06.dvi
School of Computing and Information Systems
COMP30026 Models of Computation Tutorial Week 6
30 August–3 September 2021
Content: resolution for predicate logic, clausal form, skolemization, unification.
Notice
Doing the problem sets is critical. These contain questions which are less suited to live discussion,
but are nevertheless important for you to achieve the expected learning outcomes for this subject.
The exercises
T6.1 Recall the definition of satisfiability of a predicate logic formula, and explain why these two
formulas are equisatisfiable (one is satisfiable iff the other is).
∀x∀y(¬L(x, y) ∨ ∃z(L(x, z) ∧ L(z, y))) (1)
¬L(x, y) ∨ (L(x, f(x, y)) ∧ L(f(x, y), y)) (2)
T6.2 Perform the unification algorithm to determine if the terms h(v, g(v), f(u, a)) and h(g(x), y, x)
are unifiable, and if so, write down a most general unifier.
T6.3 Use resolution to show that the following set of clauses is unsatisfiable.
{Q(f(u), g(x)), P (x)}, {¬P (b)}, {¬Q(z, y), R(z, z)}, {¬R(w, f(u))}
T6.4 Turn the closed formula ∃z∀x ∃y
[
∃u ∀v
(
P (x, y) ∨Q(z, u, v)
)
⇒∀u
(
¬R(f(x), u, y)
)]
into
clausal form.
T6.5 For this question use the following predicates:
• G(x) for “x is a green dragon”
• R(x) for “x is a red dragon”
• H(x) for “x is a happy dragon”
• S(x) for “x is a dragon capable of spit-
ting fire”
• P (x, y) for “x is a parent of y”
• C(x, y) for “x is a child of y”
(a) Express the following statements as formulas in first-order predicate logic:
i. x is a parent of y if and only if y is a child of x.
ii. A dragon is either green or red; not both.
iii. A dragon is green if and only if at least one of its parents is green.
iv. Green dragons can spit fire.
v. A dragon is happy if all of its children can spit fire.
(b) Translate each of the five formulas to clausal form.
(c) Prove, using resolution, that all green dragons are happy.
After you finish: Work on Problem Set 6.