% % Who killed Aunt Agatha puzzle % % % % Used predicates : % % lives(X) : X lives in Dreadbury Mansion % killed(X, Y) : X hates Y % richer(X, Y) : X is richer than Y % hates(X, Y) : X hates Y % % % % Rem : X = Y is equivalent to the predicate equal(X, Y) % X != Y is equivalent to ~equal(X, Y) % equal(X, Y) is a predefined predicate !!! % % If the equal predicate wasn't defined, we could use % somes axioms to have the same behaviour. % % Axioms for equality : % % premise{ ![X] : equal(X, X) } % premise{ ![X,Y,Z] : (equal(X,Y) => ((lives(X) <=> lives(Y)) & % (killed(X,Z) <=> killed(Y,Z)) & % (killed(Z,X) <=> killed(Z,Y)) & % (richer(X,Z) <=> richer(Y,Z)) & % (richer(Z,X) <=> richer(Z,Y)) & % (hates(X,Z) <=> hates(Y,Z)) & % (hates(Z,X) <=> hates(Z,Y)))) } % % Someone who lives in Dreadbury Mansion killed Aunt Agatha. premise{ ?[X] : (lives(X) & killed(X, agatha)) } % Agatha, the butler, and Charles live in Dreadbury Mansion, premise{ lives(agatha) } premise{ lives(butler) } premise{ lives(charles) } % and are the only people who live therein. premise{ ![X] : (lives(X) => (X = agatha | X = butler | X = charles)) } % A killer always hates his victim, premise{ ![X,Y] : (killed(X, Y) => hates(X, Y)) } % and is never richer than his victim. premise{ ![X,Y] : (killed(X, Y) => ~richer(X, Y)) } % Charles hates no one that Aunt Agatha hates. premise{ ![X] : (hates(agatha, X) => ~hates(charles, X)) } % Agatha hates everyone except the butler. premise{ ![X] : ((X != butler) => hates(agatha, X)) } % The butler hates everyone not richer than Aunt Agatha. premise{ ![X] : (~richer(X, agatha) => hates(butler, X)) } % The butler hates everyone Aunt Agatha hates. premise{ ![X] : (hates(agatha, X) => hates(butler, X)) } % No one hates everyone. premise{ ![X] : ?[Y] : ~hates(X, Y) } % Agatha is not the butler. premise{ agatha != butler } % Therefore : Agatha killed herself. conclusion{ killed(agatha, agatha) }