/Users/billy/gits/moc-2021/tutes/sol03.dvi
The University of Melbourne
School of Computing and Information Systems
COMP30026 Models of Computation
Sample Answers to Tutorial Exercises, Week 3
T3.1 F and G are logically equivalent if every truth-assignment assigns the same value to F and
G. G is a logical consequence of F if every truth-assignment which makes F true, also makes
G true. Alternatively, G is a logical consequence of F if no truth-assignment makes F true
and G false.
(i) F � f tells you that F is unsatisfiable
(ii) F � t tells you nothing about F , since t is a logical consequence of any formula (think
about the definition of logical consequence)
(iii) f � F tells you nothing about F , since any formula is a logical consequence of f (think
about the definition of logical consequence)
(iv) t � F tells you F is valid
(v) F � G and G � H tells you that F � H, since any truth assignment that makes F true
must make G true (because F � G), and therefore must make H true (because G � H).
(vi) F � G and G � f tells you F and G are both unsatisfiable, using part (v) and part (i)
T3.2 Here is a refutation:
{A,B} {A,¬B} {C,¬A,¬D} {¬C,¬D} {D}
{A} {¬A,¬D}
{¬A}
⊥
From this we conclude that (A∨B)∧(A∨¬B)∧(C∨¬A∨¬D)∧(¬C∨¬D)∧D is unsatisfiable.
T3.3 We can translate these as follows, using F for “Jemima eats duck food”, H for “Jemima is
healthy”, and E for “Jemima will lay an egg”.
(i) F ⇒H
(ii) H ⇒ E
(iii) F
We want to show that in every scenario where these assumptions are true, E must also be
true. In other words, we want to show (F ⇒H) ∧ (H ⇒ E) ∧ F � E. This is equivalent to
showing that the formula (F ⇒ H) ∧ (H ⇒ E) ∧ F ∧ ¬E is unsatisfiable. This formula is
equivalent to (¬F ∨ H) ∧ (¬H ∨ E) ∧ F ∧ ¬E, which is in conjunctive normal form. This
corresponds to the set of clauses {{¬F,H}, {¬H,E}, {F}, {¬E}}, which we can show is
unsatisfiable with the resolution proof below.
{¬F,H} {¬H,E} {F} {¬E}
{¬F,E}
{E}
⊥
T3.4 If we only need to know about one row of the truth table to demonstrate something, then
exhibiting that truth assignment is the cleanest and easiest way to do so. Otherwise we can
choose between writing out the truth table or using resolution. If the formula/s are small
enough, then it’s often easiest to just draw up the truth-table/s, but resolution is a lot easier
when the formulas become larger.
The important piece of information for each of this situations that use resolution is how you
reduce the problem to showing some set of clauses is unsatisfiable.
(i) A chain of conversion formulas can demonstrate F ≡ G if the formulas are similar
enough. If they are too different it might take a while to turn one formula into the
other. If the formulas are small enough we can just draw the truth tables, and compare
their main columns. Otherwise we can show that ¬(F⇔G) is unsatisfiable via resolution,
since ¬(F ⇔G) is unsatisfiable iff F ≡ G.
(ii) We can refute F ≡ G (show they are not logically equivalent), by exhibiting a truth
assignment which makes one true and the other false. For example, A⇒ B 6≡ B ⇒ A,
since the truth assignment that makes A true and B false makes A⇒B false and B⇒A
true.
(iii) We can show F is unsatisfiable by drawing its truth table if it’s small enough, otherwise
we can just convert F to CNF and apply resolution until we reach the empty clause.
(iv) We can show F is satisfiable by exhibiting a truth assignment that makes it true. For
example, A ∨ B is satisfiable, because the truth assignment that makes A true and B
false, makes it true. You might be tempted to apply resolution, then fail to produce
the empty clause, and therefore conclude it must be satisfiable because you couldn’t
show it to be unsatisfiable. While this can be done correctly, you would need to prove
that whatever algorithm you’re using to produce resolvents will always find the empty
clause in a finite number of steps, whenever the formula is unsatisfiable, and will fail
and terminate otherwise. That’s so much more effort than just exhibiting a truth-
assignment that makes the formula true. However, using resolution on a satisfiable set
of clauses can still give you logical consequences, which can help you construct the truth
assignment which satisfies all of the original clauses.
(v) We can show F is valid by showing ¬F is unsatisfiable (or just look at the truth table
if it is small enough to write out).
(vi) We can show F � G by showing F ∧ ¬G is unsatisfiable.
(vii) We can show A ∧B ∧ C � F by showing A ∧B ∧ C ∧ ¬F is unsatisfiable.
(viii) We can refute A∧B ∧C � F by exhibiting a truth-assignment which makes A∧B ∧C
true and F false.
2