/Users/billy/gits/moc-2021/tutes/week03.dvi
School of Computing and Information Systems
COMP30026 Models of Computation Tutorial Week 3
9–13 August 2021
Content: logical equivalence/consequence, resolution, translating into propositional logic
The exercises
T3.1 Discuss what it means for formulas, F and G, to be logically equivalent (i.e. F ≡ G), and
what it means for G to be a logical consequence of F (i.e. F � G). What can we conclude (if
anything) about formulas F,G,H in the following situations?
(i) F � f
(ii) F � t
(iii) f � F
(iv) t � F
(v) F � G and G � H
(vi) F � G and G � f
T3.2 Resolution works by producing resolvents of a set of clauses. These resolvents are logical
consequences of the original set, so if a resolvent is unsatisfiable, so is the original set of
clauses. Using resolution, show that the set {{A,B}, {A,¬B}, {C,¬A,¬D}, {¬C,¬D}, {D}}
of clauses is unsatisfiable.
T3.3 Consider these assumptions:
(a) If Jemima eats duck food then she is healthy
(b) If Jemima is healthy she will lay an egg
(c) Jemima eats duck food
Translate these formulas into propositional logic, and use them to prove that Jemima will lay
an egg, by showing that some set of clauses is unsatisfiable.
T3.4 We now have 3 different tools to reason about propositional formulas: truth tables/truth
assignments, conversion rules for equivalent formulas, and resolution. Discuss how we can use
these tools to do the following. Which is best in each situation?
(i) Prove F ≡ G
(ii) Refute F ≡ G
(iii) Prove F is unsatisfiable
(iv) Prove F is satisfiable
(v) Prove F is valid
(vi) Prove that F � G
(vii) Prove that F must hold, given premises
A,B,C, (that is, A ∧B ∧ C � F )
(viii) Refute A ∧B ∧ C � F
If you finish early: work on questions from Problem Set 3