% problem-set/puzzles/truth_lies/tandl42.ver1.clauses % created : 07/14/88 % revised : 07/14/88 % description: % % This run solves "Truthtellers and Liars Puzzle #42" using hyper- % resolution. % % Truthtellers and Liars Puzzle #42 % % There is an island with exactly three types of people-- % truthtellers who always tell the truth, and liars who always % lie, and normals who sometimes tell the truth and sometimes % lie. Liars are said to be of the lowest rank , % normals are middle rank, and truthtellers of the highest rank % of the highest rank. Two people A and B on the island make the % following statements. % A: I am of lower rank than B % B: Thats not true! % What are the ranks of A and B, and which of the two statements % are true? % representation: % % declare_predicate(3,P). % declare_predicate(1,TRUE). % declare_functions(1,[atr,liar,norm,nnorm]). % declare_functions(2,[Said,lower,nlower]). % declare_variables([x,y,z]). % declare_constants([a,b,c]). % A person can be one of : truthteller, liar and normal TRUE(atr(x)) | TRUE(liar(x)) | TRUE(norm(x)). -TRUE(atr(x)) | -TRUE(norm(x)). -TRUE(atr(x)) | -TRUE(liar(x)). -TRUE(liar(x)) | -TRUE(norm(x)). % A truthteller always tells the truth and a liar always lies -TRUE(atr(x)) | -TRUE(Said(x,y)) | TRUE(y) . -TRUE(liar(x)) | -TRUE(Said(x,y)) | -TRUE(y) . -TRUE(x) | -TRUE(Said(y,x)) | TRUE(atr(y)) | TRUE(norm(y)). TRUE(x) | -TRUE(Said(y,x)) | TRUE(liar(y)) | TRUE(norm(y)). % Definition of "lower than" and "not lower than" TRUE(nlower(x,x)). -TRUE(nlower(x,y)) | -TRUE(lower(x,y)). TRUE(nlower(x,y)) | TRUE(lower(x,y)). -TRUE(lower(x,y)) | -TRUE(liar(x)) | TRUE(norm(y)) | TRUE(atr(y)). -TRUE(lower(x,y)) | -TRUE(norm(x)) | TRUE(atr(y)). -TRUE(lower(x,y)) | -TRUE(atr(x)). -TRUE(lower(x,y)) | -TRUE(atr(y)) | TRUE(norm(x)) | TRUE(liar(x)). -TRUE(lower(x,y)) | -TRUE(norm(y)) | TRUE(liar(x)). -TRUE(lower(x,y)) | -TRUE(liar(y)). -TRUE(nlower(x,y)) | -TRUE(atr(x)) | TRUE(atr(y)) | TRUE(lower(y,x)). -TRUE(nlower(x,y)) | -TRUE(liar(x)) | TRUE(liar(y)) | TRUE(lower(y,x)). -TRUE(nlower(x,y)) | -TRUE(norm(x)) | TRUE(norm(y)) | TRUE(lower(y,x)). % Statements made by A and B TRUE(Said(a,lower(a,b))). TRUE(Said(b,nlower(a,b))).