42. (a)
The University of Melbourne
School of Computing and Information Systems COMP30026 Models of Computation
Selected Tutorial Solutions, Week 6
The two statements
S1: “No politician is honest.” become F1 : ∀x (¬P (x) ∨ ¬H(x))
S2: “Some politicians are not honest.” F2 : ∃x (P (x) ∧ ¬H(x)) (b) F1 ⇒ F2 is satisfiable. First let us simplify the formula. Normally it would be a good
idea to rename the bound variables, but in this case, it will be preferable to keep the x.
F1 ⇒ F2
≡ ∀x (¬P(x) ∨ ¬H(x)) ⇒ ∃x (P(x) ∧ ¬H(x))
≡ ¬∀x (¬P (x) ∨ ¬H(x)) ∨ ∃x (P (x) ∧ ¬H(x))
≡ ∃x (P(x) ∧ H(x)) ∨ ∃x (P(x) ∧ ¬H(x))
≡ ∃x ((P (x) ∧ H(x)) ∨ (P (x) ∧ ¬H(x)))
≡ ∃x (P (x) ∧ (H(x) ∨ ¬H(x)))
≡ ∃xP(x)
spell out
eliminate implication
push negation in
∃ distributes over ∨
factor out P(x)
eliminate trivially true conjunct
For this formula we can clearly find an interpretation that makes it true. For example,
take the domain {alf,bill,charlie} and let P and H hold for all elements. Or, take the domain Z, let P stand for “is a prime” and let H stand for “is zero”. Itstruthonlydepend n
(c) F1 ⇒ F2 is not valid. It is easy to find an interpretation that makes ∃x P (x) false. For go example,takethedomain{alf,bill,charlie}andletP holdfornoneoftheelements(H His can be given any interpretation). Or, take the domain Z, let P stand for “is an even irrelevant prime greater than 2” and let H stand for “is zero”.
(d) The statements
can be expressed
S3: S4:
“No Australian politician is honest.” “All honest politicians are Australian.”
S3: ∀x((A(x)∧P(x))⇒¬H(x)) S4: ∀y((P(y)∧H(y))⇒A(y))
Each of these formulas corresponds to exactly one clause. The clausal forms are:
{{¬A(x), ¬H (x), ¬P (x)}} {{A(y), ¬H(y), ¬P (y)}}
(e) We can show that S1 is a logical consequence of S3 and S4 by refuting S3∧S4∧¬S1. So let us write ¬S1 in clausal form (note that we must apply the negation before “clausifying”; the other way round generally gives an incorrect result):
¬∀x (¬P (x) ∨ ¬H (x))
∃x (P (x) ∧ H (x)) push negation in P (a) ∧ H (a) Skolemize
Or, written as a set of sets: {{P(a)},{H(a)}}. Added to the other clauses, these allow us to complete the proof by resolution:
mm
¬A(x), ¬P (x), ¬H(x) A(y), ¬P (y), ¬H(y) ¬P (x), ¬H (x)
¬H (a)
⊥
P (a) H(a)
43.
(f) The statement “S2 is a logical consequence of S3 and S4” is false. We can show this by constructing an interpretation which makes S3 and S4 true, while making S2 false. Any interpretation with domain D, in which P is false for all elements of D, will do.
(We should rename clauses apart, but in this case, no confusion arises, so we omit that.) We can construct the refutation in 5 resolution steps, that is, the refutation tree has only 5 internal nodes:
Px ¬Px,¬Qy Qx,¬Ry Rx,Sa Rb,¬Sx ¬Qy
¬Ry
Sa
⊥
Here is another way (5 steps), in which the depth of the refutation tree is somewhat smaller:
Px ¬Px,¬Qy Rx,Sa Qx,¬Ry Rb,¬Sx
Rb
¬Qy
Qx, Sa Qx, ¬Sz
Qx NB: variable renamed
With factoring, we can do it in 4 resolution steps, plus one factoring step:
Px ¬Px,¬Qy Qx,¬Ry Rx,Sa Rb,¬Sx ¬Qy Rb
⊥
Qx
Rx, Rb factored
44.
(a) ∀x (F(x,a) ⇒ E(a,x)) (b) ∀x(E(x,e)⇒¬F(e,x))
⊥
2
(c)
We capture “Eve is no more fortunate than Adam” as ¬F(e,a). To show that this is a logical consequence of the other two statements, we need to show that every model of ∀x (F(x,a) ⇒ E(a,x)) ∧ ∀x (E(x,e) ⇒ ¬F(e,x)) makes F(e,a) false. Assume (for contradiction) that there is a model in which F (e, a) is true. Then, by the left conjunct, E(a, e) is also true in this model. But then, by the right conjunct, ¬F (e, a) is also true, that is, F(e,a) is false. But this is a contradiction, so F(e,a) must be false. Indeed a proof by resolution is easy:
¬F(x,a),E(a,x) ¬E(x′,e),¬F(e,x′) F(e,a) ¬F (e, a)
A
45. (a) i. ii. iii. iv. v.
∀x∀y(P (x, y) ⇔ C(y, x))
b e t oA l l I f a n do n l yi f should applied f
⊥
Eoy z 131
GexNRK vGGlHnCNN
∀x(G(x)⊕R(x))
∀x(G(x) ⇔ ∃y(P(y,x) ∧ G(y))) i 7 5 I big ∀x(G(x) ⇒ S(x))
∀x(∀y[C(y, x) ⇒ S(y)] ⇒ H(x)) Happy Fifa
EVI
Pushing negation in:
∀x(¬G(x) ∨ ∃y(P (y, x) ∧ G(y)) ∧ (G(x) ∨ ∀y(¬P (y, x) ∨ ¬G(y))))
We see that the existentially quantified y needs to be Skolemized. Let us use the function symbol p, so that p(x) reads “parent of x”.
Similarly, let us simplify the fifth formula. Replacing the implication symbols, we get ∀x[¬∀y[¬C(y, x) ∨ S(y)] ∨ H(x)]. Pushing the negations in, we then get
∀x[∃y[C(y, x) ∧ ¬S(y)] ∨ H(x)]
Again, the existentially quantified y needs to be Skolemized, and we must use a fresh
function symbol—let us choose c, so that c(x) reads “child of x”. We can now list the clauses:
i. Two clauses: {¬P(x,y),C(y,x)} and {P(x,y),¬C(y,x)} ii. Two clauses: {G(x), R(x)} and {¬G(x), ¬R(x)}
iii. Three clauses: {¬G(x), P (p(x), x)}, {¬G(x), G(p(x))}, and {G(x), ¬P (y, x), ¬G(y)} iv. One clause: {¬G(x), S(x)}
v. Two clauses: {C(c(x), x), H(x)} and {¬S(c(x)), H(x)}
(c) The statement to prove is ∀x(G(x) ⇒ H(x)). Negating this statement, we have ∃x(G(x) ∧ ¬H(x)). In clausal form this is G(a) and ¬H(a) (two clauses). Altogether we now have 12 clauses, but fortunately a refutation can be found that uses just seven:
(b) Before we generate clauses, let us simplify the third formula. Replacing ⇔, we get ∀x(¬G(x) ∨ ∃y(P (y, x) ∧ G(y)) ∧ (G(x) ∨ ¬∃y(P (y, x) ∧ G(y))))
3
IQ
¬G(u), S(u)
¬S(c(v)), H(v) ¬S(c(a))
¬G(c(a))
⊥
46. If you haven’t used Haskell to solve this problem, it is not too late!
(a) We can hope to prove an existential claim by brute force, by using Haskell to enumerate candidate witnesses. If a witness appears in a reasonable time we are done. There is no obvious way to refute an existential claim that way, nor to prove a universal claim.
(b) The conjecture is false. The easiest way to get to that conclusion is to write the con- jecture as a Haskell expression
conjecture k = elem (product (take k primes) + 1) primes
(assuming we have defined primes) and then check, say: map conjecture [1..10] and
see what happens. We find that it fails for k = 6.
(c) Easy, if we let Haskell do the work:
(3,5), (5,7), (11,13), (17,19), (29,31), (41,43), (59,61), (71,73), (101,103), (107,109), (137,139), (149,151), (179,181), (191,193), (197,199), (227,229), (239,241), (269,271), (281,283), (311,313), (347,349), (419,421), (431,433), (461,463), (521,523), (569,571), (599,601), (617,619), (641,643), (659,661), (809,811), (821,823), (827,829), (857,859), (881,883), (1019,1021), (1031,1033), (1049,1051), (1061,1063), (1091,1093), (1151,1153), (1229,1231), (1277,1279), (1289,1291), (1301,1303), (1319,1321), (1427,1429), (1451,1453), (1481,1483), (1487,1489).
(d) Haskell generates the triple (3,5,7) and then stalls.
(e) … and for good reason, as there are no other prime triples. However, we can’t hope to use Haskell to prove that! Instead we have to think.
Here is why there cannot be any prime triples other than (3, 5, 7). Assume that p > 3. Out of p, p+2, and p+4, one must be divisible by 3, and so it is not a prime. The following table shows all the possible remainders of the three numbers, after division by 3:
In all cases, one of the three is divisible by 3.
Notice that this proof is not by brute force. Its critical step is to identify an essential property of prime triples and use that, rather than simply enumerate-and-test.
¬H(a) C(c(a), a)
P (a, c(a)) G(c(a)), ¬G(a) G(c(a))
C(c(w), w), H(w)
P (x, y), ¬C(y, x)
G(x′), ¬P (y′, x′), ¬G(y′) G(a)
p p+2 p+4
012 201 120
4
guy
U
u gcx
48
X
u ferv u
47
Tcu
yzD
vU IiE
μgtca.gr fu guy
y Y
n gyu
y2D
gcx
U
gca
gu 112,32
fca y z
fcga y 442,27
gta
guy fly yea
su fi.si
gcx
fEIiIi
x
LEE Vx.yGBCDVSLy.ylvnscx.LI
Bex
EE
49 V x.ge 3CX VnGscy y vscx y
Sly.y 751kg
BCD
Buy
BCD
0