== The following puzzle is due to L. Schubert
==
== A mysterious death at Dreadbury Mansion ...
==
== 1: Someone who lives at Dreadbury Mansion killed Aunt Agatha.
== 2: Only Agatha, the butler and Charles has lived at Dreadbury Mansion.
== 3: A killer always hates their victim.
== 4: A killer is never richer than their victim.
== 5: Charles hates no-one that Aunt Agatha hates.
== 6: Aunt Agatha hates everyone but the butler.
== 7: The butler hates everyone who is not richer than Aunt Agatha.
== 8: The butler hates everyone Aunt Agatha hates.
== 9: No-one hates everyone.
== 10: Aunt Agatha is not identical with the butler, of course.
==
== Question: Who killed Aunt Agatha?
==
environ reserve x1,x2,z,u,v,w for Person;
given Agatha, butler, Charles being Person;
1: ex x1 st LivesatDBM[x1] & Killed[x1,Agatha];
2: for x1 st LivesatDBM[x1] holds x1=Agatha or x1=butler or x1=Charles;
3: for x1,x2 st Killed[x1,x2] holds Hates[x1,x2];
4: for x1,x2 st Killed[x1,x2] holds not Richer[x1,x2];
5: for x1 st Hates[Agatha,x1] holds not Hates[Charles,x1];
6: for x1 st x1<>butler holds Hates[Agatha,x1];
7: for x1 st not Richer[x1,Agatha] holds Hates[butler,x1];
8: for x1 st Hates[Agatha,x1] holds Hates[butler,x1];
9: for x1 ex x2 st not Hates[x1,x2];
10: Agatha<>butler
begin
Killed[Agatha, Agatha]
proof
11: for x1 st x1<>butler holds Hates[butler,x1] proof
let u be Person;
assume 11a: u<>butler;
thus Hates[butler,u] proof
11b: Hates[Agatha,u] by 11a,6;
thus thesis by 8,11b;
end;
end;
12: ex x2 st not Hates[butler,x2] by 9;
consider u such that
13: not Hates[butler,u] by 12;
14: u=butler proof
assume 14a: u<>butler;
14b: Hates[butler,u] by 11,14a;
thus contradiction by 13,14b;
end;
15: not Hates[butler,butler] by 13,14;
16: Richer[butler,Agatha] by 7,15;
17: not Killed[butler,Agatha] by 4,16;
18: Hates[Agatha,Agatha] by 6,10;
19: not Hates[Charles,Agatha] by 5,18;
20: not Killed[Charles,Agatha] by 3,19;
consider u such that
21: LivesatDBM[u] & Killed[u,Agatha] by 1;
22: u=Agatha or u=butler or u=Charles by 2,21;
23: u<>butler & u<>Charles by 17,20,21;
24: u=Agatha by 22,23;
thus thesis by 21,24;
end
environ
== The following example is due to L. Schubert.
==
== Wolves, foxes, birds, caterpillars, and snails are animals, and there
== are some of each of them.
reserve x, y, w, f, b, c, s for animal;
A: ex w, f, b, c, s st
wolf[w] & fox[f] & bird[b] & caterpillar[c] & snail[s];
== Also, there are some grains, and grains are plants.
reserve p, g for plants;
P: ex g st grain[g];
== Every animal either likes to eat all plants or all animals much smaller
== than itself that like to eat some plants.
1LIKES: for x holds
(for p holds likes[x,p])
or
(for y st smaller[y,x] &
(ex p st likes[y,p])
holds likes[x,y]);
== Caterpillars and snails are much smaller than birds, which are much smaller
== than foxes, which in turn are much smaller than wolves.
1SMALLER: for x, y st (caterpillar[x] or snail[x]) & bird[y]
holds smaller[x,y];
2SMALLER: for x, y st bird[x] & fox[y] holds smaller[x,y];
3SMALLER: for x, y st fox[x] & wolf[y] holds smaller[x,y];
== Wolves do not like to eat foxes or grains, while birds like to eat
== caterpillars but not snails.
2LIKES: for x, y, p st wolf[x] & fox[y] & grain[p]
holds not likes[x,y] & not likes[x,p];
3LIKES: for x, y st bird[x]
holds (caterpillar[y] implies likes[x,y]) &
(snail[y] implies not likes[x,y]);
== Caterpillars and snails like to eat some plants.
4LIKES: for x st caterpillar[x] or snail[x]
ex p st likes[x,p]
== Therefore there is an animal that likes to eat a grain-eating animal.
begin
ex x, y, p st likes[x,y] & likes[y,p] & grain[p]
proof
consider w, f, b, c, s such that
WFBCS: wolf[w] & fox[f] & bird[b] & caterpillar[c] & snail[s] by A;
consider g such that G: grain[g] by P;
0: not likes[b,s] & (ex p st likes[s,p]) & smaller[s,b]
by 3LIKES, 4LIKES, 1SMALLER, WFBCS;
1: likes[b,g] by 0, 1LIKES;
2: smaller[f,w] & not likes[w,f] & not likes[w,g]
by 3SMALLER, 2LIKES, G, WFBCS;
3: not likes[f,g] by 2, 1LIKES;
4: smaller[b,f] by 2SMALLER, WFBCS;
5: likes[f,b] by 1, 3, 4, 1LIKES;
thus thesis by G, 1, 5
end;
== A bit shorter, but messier.
ex x, y, p st likes[x,y] & likes[y,p] & grain[p]
proof
consider w, f, b, c, s such that
WFBCS: wolf[w] & fox[f] & bird[b] & caterpillar[c] & snail[s] by A;
consider g such that G: grain[g] by P;
1: not likes[b,s] & (ex p st likes[s,p]) & smaller[s,b] &
smaller[f,w] & not likes[w,f] & not likes[w,g] & smaller[b,f]
by 1SMALLER, 2SMALLER, 3SMALLER, 2LIKES,
3LIKES, 4LIKES, G, WFBCS;
2: likes[b,g] & not likes[f,g] by 1, 1LIKES;
3: likes[b,g] & likes[f,b] by 1, 2, 1LIKES;
thus thesis by G, 3
end
== Who will make it any shorter?