(c)
(d)
(A ∨ B) ⇒ (C ∧ D)
¬(A∨B)∨(C ∧D)
(¬A∧¬B)∨(C ∧D)
(¬A ∨ (C ∧ D)) ∧ (¬B ∨ (C ∧ D)) (¬A∨C)∧(¬A∨D)∧(¬B∨C)∧(¬B∨D) (distribute∧over∨)
The University of Melbourne
School of Computing and Information Systems COMP30026 Models of Computation
Sample Answers to Tutorial Exercises, Week 3
(push negation in) (distribute ∨ over ∧)
KE ETE thEY E (distribute ∨ over ∧)
19. (a)
The result is now in reduced CNF. (b)
Hok I HE b
¬(A ∧ ¬(B ∧ C))
¬A ∨ (B ∧ C)
(¬A ∨ B) ∧ (¬A ∨ C)
A ∨ (¬B ∧ (C ∨ (¬D ∧ ¬A)))
(A ∨ ¬B) ∧ (A ∨ C ∨ (¬D ∧ ¬A))
(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).
The result is in RCNF. We could have chosen different orders for the distributions.
BV THVB
A ∧ (B ⇒ (A ⇒ B))
A ∧ (¬B ∨ ¬A ∨ B) (unfold both occurrences of ⇒)
A (rightmost clause is tautological: remove it)
20. Let us follow the method given in a lecture, except we do the double-negation elimination
BVA B n BVAVB
aggressively, as soon as opportunity arises:
BHA ElBVAVB
¬((¬B ⇒ ¬A) ⇒ ((¬B ⇒ A) ⇒ B))
¬(¬(B ∨ ¬A) ∨ ¬(B ∨ A) ∨ B) (B ∨ ¬A) ∧ (B ∨ A) ∧ ¬B
This is RCNF without further reductions.
FAHDeMorgan KEEF PE
(unfold ⇒)
(de Morgan) (distribute ∨ over ∧)
(unfold ⇒ and eliminate double negation)
(de Morgan for outermost neg; elim double neg)
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}
{}
{A}
{}
21. Here is a refutation:
{¬B}
{A, ¬B}
{A, B, ¬C} {A, B, C} {A,B}
{¬A}
KLARA
HuttotxtEk
From this we conclude that (A ∨ B ∨ ¬C) ∧ ¬A ∧ (A ∨ B ∨ C) ∧ (A ∨ ¬B) is unsatisfiable.
Negation
22. (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. 7AVB
So:
A n nB
¬((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 the result into RCNF:
¬((¬P ⇒P)⇒P) (¬P ⇒ P ) ∧ ¬P (¬¬P ∨ P) ∧ ¬P (P ∨ P ) ∧ ¬P
formula, to get ¬((¬P ⇒ P) ⇒ P). Then turn
(shortcut from above) (unfold ⇒)
(eliminate double negation) (∨-absorption)
P ∧ ¬P
The resolution proof is immediate; we will leave it out.
Tmm
2
(c) ((P ⇒Q)⇒P)⇒P. Again,negatetheformula,toget¬(((P ⇒Q)⇒P)⇒P). Then turn the result into RCNF:
¬(((P ⇒Q)⇒P)⇒P) ((P ⇒Q)⇒P)∧¬P ((¬P ∨Q)⇒P)∧¬P (¬(¬P ∨Q)∨P)∧¬P ((¬¬P ∧¬Q)∨P)∧¬P ((P ∧¬Q)∨P)∧¬P
(P ∨P)∧(¬Q∨P)∧¬P P ∧(¬Q∨P)∧¬P
(shortcut, outermost ⇒) (unfold ⇒)
(unfold ⇒)
(de Morgan)
(double negation) (distribution) (absorption)
PVnP TQP 03
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
03
the resulting formula into RCNF:
P ⊕ ((P ⇒ Q) ⇒ P )
(P ∨((P ⇒Q)⇒P))∧(¬P ∨¬((P ⇒Q)⇒P)) (P ∨ ((P ⇒ Q) ⇒ P )) ∧ (¬P ∨ ((P ⇒ Q) ∧ ¬P )) (P ∨ (¬(¬P ∨ Q) ∨ P)) ∧ (¬P ∨ ((¬P ∨ Q) ∧ ¬P)) (P ∨(¬¬P ∧¬Q)∨P)∧(¬P ∨((¬P ∨Q)∧¬P)) (P ∨(P ∧¬Q)∨P)∧(¬P ∨((¬P ∨Q)∧¬P))
P ∧ (P ∨ ¬Q) ∧ (¬P ∨ ((¬P ∨ Q) ∧ ¬P ))
P ∧(P ∨¬Q)∧(¬P ∨Q)∧¬P
(eliminate ⊕)
(shortcut from above) (⇒-elimination)
(de Morgan)
(double negation) (∨-absorption, distribution) (∨-absorption, distribution)
23. (a)
Once again, now just resolve {P} against {¬P}.
{{A, B}, {¬A, ¬B}, {¬A, B}} stands for the formula (A ∨ B) ∧ (¬A ∨ ¬B) ∧ (¬A ∨ B).
This is satisfiable by {A → f,B → 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) Wehave{{A,B},{¬A,¬B},{B,C},{¬B,¬C},{A,C},{¬A,¬C}}. Thissetisnotsat- isfiable, as a proof by resolution shows:
{A, B} {¬B, ¬C} {A, ¬C}
{A}
{A, C}
{¬A, ¬B} {B, C} {¬A, ¬C} {¬A, C}
{¬A}
He4
King 4
{}
FATE
3
24. 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)
1s
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 neagate 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.)
25. Let us give names to the propositions:
• A: The commissioner apologises
• F : The commissioner can attend the function • 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).
(c) (T∧¬F)⇒C (d) K ⇒ S
4