CS计算机代考程序代写 /Users/billy/gits/moc-2021/tutes/week03.dvi

/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