/Users/billy/gits/moc-2021/problem-sets/solps03.dvi
The University of Melbourne
School of Computing and Information Systems
COMP30026 Models of Computation
Solutions for Problem Set 3
P3.1 (a)
¬(A ∧ ¬(B ∧ C))
¬A ∨ (B ∧ C) (push negation in)
(¬A ∨B) ∧ (¬A ∨ C) (distribute ∨ over ∧)
The result is now in reduced CNF.
(b)
A ∨ (¬B ∧ (C ∨ (¬D ∧ ¬A)))
(A ∨ ¬B) ∧ (A ∨ C ∨ (¬D ∧ ¬A)) (distribute ∨ over ∧)
(A ∨ ¬B) ∧ (A ∨ C ∨ ¬D) ∧ (A ∨ C ∨ ¬A) (distribute ∨ over ∧)
The result is in CNF but not RCNF. To get RCNF we need to eliminate the last clause
which is a tautology, and we end up with (A ∨ ¬B) ∧ (A ∨ C ∨ ¬D).
(c)
(A ∨B)⇒ (C ∧D)
¬(A ∨B) ∨ (C ∧D) (unfold ⇒)
(¬A ∧ ¬B) ∨ (C ∧D) (de Morgan)
(¬A ∨ (C ∧D)) ∧ (¬B ∨ (C ∧D)) (distribute ∨ over ∧)
(¬A ∨ C) ∧ (¬A ∨D) ∧ (¬B ∨ C) ∧ (¬B ∨D) (distribute ∧ over ∨)
The result is in RCNF. We could have chosen different orders for the distributions.
(d)
A ∧ (B ⇒ (A⇒B))
A ∧ (¬B ∨ ¬A ∨B) (unfold both occurrences of ⇒)
A (rightmost clause is tautological: remove it)
P3.2 Let us follow the method given in a lecture, except we do the double-negation elimination
aggressively, as soon as opportunity arises:
¬((¬B ⇒¬A)⇒ ((¬B ⇒A)⇒B))
¬(¬(B ∨ ¬A) ∨ ¬(B ∨A) ∨B) (unfold ⇒ and eliminate double negation)
(B ∨ ¬A) ∧ (B ∨A) ∧ ¬B (de Morgan for outermost neg; elim double neg)
This is RCNF without further reductions.
We could also have used other transformations—sometimes this can shorten the process. For
example, we could have rewritten the sub-expression ¬B⇒¬A as A⇒B (the contraposition
principle). You may want to check that this does not change the result.
The resulting formula, written as a set of sets of literals:
{{¬A,B}, {A,B}, {¬B}}
We can now construct the refutation:
{¬A,B} {A,B} {¬B}
{B}
{ }
P3.3 (a) (P ∨Q)⇒ (Q∨P ). First negate the formula (why?), to get ¬((P ∨Q)⇒ (Q∨P )). Then
we can use the usual techniques to convert the negated proposition to RCNF. Here is a
useful shortcut, combining ⇒-elimination with one of de Morgan’s laws:
¬(A⇒B) ≡ A ∧ ¬B.
So:
¬((P ∨Q)⇒ (Q ∨ P ))
(P ∨Q) ∧ ¬(Q ∨ P ) (shortcut)
(P ∨Q) ∧ ¬Q ∧ ¬P (de Morgan)
The result allows for a straight-forward refutation:
{P,Q} {¬Q} {¬P}
{P}
{ }
(b) (¬P ⇒ P )⇒ P . Again, first negate the formula, to get ¬((¬P ⇒ P )⇒ P ). Then turn
the result into RCNF:
¬((¬P ⇒ P )⇒ P )
(¬P ⇒ P ) ∧ ¬P (shortcut from above)
(¬¬P ∨ P ) ∧ ¬P (unfold ⇒)
(P ∨ P ) ∧ ¬P (eliminate double negation)
P ∧ ¬P (∨-absorption)
The resolution proof is immediate; we will leave it out.
(c) ((P ⇒Q)⇒ P )⇒ P . Again, negate the formula, to get ¬(((P ⇒Q)⇒ P )⇒ P ). Then
turn the result into RCNF:
¬(((P ⇒Q)⇒ P )⇒ P )
((P ⇒Q)⇒ P ) ∧ ¬P (shortcut, outermost ⇒)
((¬P ∨Q)⇒ P ) ∧ ¬P (unfold ⇒)
(¬(¬P ∨Q) ∨ P ) ∧ ¬P (unfold ⇒)
((¬¬P ∧ ¬Q) ∨ P ) ∧ ¬P (de Morgan)
((P ∧ ¬Q) ∨ P ) ∧ ¬P (double negation)
(P ∨ P ) ∧ (¬Q ∨ P ) ∧ ¬P (distribution)
P ∧ (¬Q ∨ P ) ∧ ¬P (absorption)
Again this gives an immediate refutation: just resolve {P} against {¬P}.
(d) P ⇔ ((P ⇒ Q)⇒ P ). Negating the formula, we get P ⊕ ((P ⇒ Q)⇒ P ). Let us turn
the resulting formula into RCNF:
P ⊕ ((P ⇒Q)⇒ P )
(P ∨ ((P ⇒Q)⇒ P )) ∧ (¬P ∨ ¬((P ⇒Q)⇒ P )) (eliminate ⊕)
(P ∨ ((P ⇒Q)⇒ P )) ∧ (¬P ∨ ((P ⇒Q) ∧ ¬P )) (shortcut from above)
(P ∨ (¬(¬P ∨Q) ∨ P )) ∧ (¬P ∨ ((¬P ∨Q) ∧ ¬P )) (⇒-elimination)
(P ∨ (¬¬P ∧ ¬Q) ∨ P ) ∧ (¬P ∨ ((¬P ∨Q) ∧ ¬P )) (de Morgan)
(P ∨ (P ∧ ¬Q) ∨ P ) ∧ (¬P ∨ ((¬P ∨Q) ∧ ¬P )) (double negation)
P ∧ (P ∨ ¬Q) ∧ (¬P ∨ ((¬P ∨Q) ∧ ¬P )) (∨-absorption, distribution)
P ∧ (P ∨ ¬Q) ∧ (¬P ∨Q) ∧ ¬P (∨-absorption, distribution)
Once again, now just resolve {P} against {¬P}.
2
P3.4 (a) {{A,B}, {¬A,¬B}, {¬A,B}} stands for the formula (A ∨B) ∧ (¬A ∨ ¬B) ∧ (¬A ∨B).
This is satisfiable by {A 7→ f , B 7→ t}.
(b) {{A,¬B}, {¬A}, {B}} stands for (A ∨ ¬B) ∧ ¬A ∧B. A refutation is easy:
{A,¬B} {¬A} {¬B}
{¬B}
{ }
(c) {{A}, ∅} stands for A ∧ f , which is clearly not satisfiable.
(d) We have {{A,B}, {¬A,¬B}, {B,C}, {¬B,¬C}, {A,C}, {¬A,¬C}}. This set is not sat-
isfiable, as a proof by resolution shows:
{A,B} {¬B,¬C} {A,C} {¬A,¬B} {B,C} {¬A,¬C}
{A,¬C} {¬A,C}
{A} {¬A}
{ }
P3.5 Let us give names to the propositions:
• C: Ann clears 2 meters
• F : Ann gets the flu
• K: The selectors are sympathetic
• S: Ann is selected
• T : Ann trains hard
The four assumptions then become:
(a) C ⇒ S
(b) T ⇒ (F ⇒K)
(c) (T ∧ ¬F )⇒ C
(d) K ⇒ S
It is easy to see that S is not a logical consequence of these, as we can give all five variables
the value false, and all the assumptions will thereby be true.
To see that T ⇒ S is a logical consequence of the assumptions, we can negate it, obtaining
T ∧ ¬S. Then, translating everything to clausal form, we can use resolution to derive an
empty clause.
Alternatively, note that T ⇒ (F ⇒K) is equivalent to (T ∧ F )⇒K. Since also K ⇒ S, we
have (T ∧ F )⇒ S. Similarly, (T ∧ ¬F )⇒ C together with C ⇒ S gives us (T ∧ ¬F )⇒ S.
But from (T ∧ F )⇒ S and (T ∧ ¬F )⇒ S we get T ⇒ S. (You may want to check that by
massaging the conjunction of the two formulas.)
P3.6 Let us give names to the propositions:
• A: The commissioner apologises
• F : The commissioner can attend the function
3
• R: The commissioner resigns
The four statements then become
(a) F ⇒ (A ∧R)
(b) (R ∧A)⇒ F
(c) R⇒ F
(d) F ⇒A
The first translation may not be obvious. But to say “X does not happen unless Y happens”
is the same as saying “it is not possible to have X happen and at the same time Y does not
happen.” That is, ¬(X ∧ ¬Y ), which is equivalent to X ⇒ Y . Note that (a) entails (d) and
(c) entails (b).
4