% problem-set/puzzles/truth_lies/tandl.ver1.in
% created : 07/09/86
% revised : 07/13/88
 
% description:
%
% This run solves the "Truthtellers and the Liars" puzzle using
% hyper-resolution.
%
%               Truthtellers and the Liars
%
% On a certain island the  inhabitants  are  partitioned  into
% those who always tell the truth and those who always lie.  I
% landed on the island and met three inhabitants A, B, and  C.
% I  asked  A, "Are you a truth-teller or a liar?"  He mumbled
% something which I couldn't make out.  I asked B what  A  had
% said.   B  replied,  "A  said  he was a liar." C then volun-
% teered, "Don't believe B, he's lying!"  What  can  you  tell
% about A, B, and C?

% representation:
%
% declare_predicate(1,P).
% declare_functions(1,[t,l]).
% declare_function(2,says).
% declare_variables([x,y]).
% declare_constants([a,b,c,notknown]).
% 
% P(x) means "x is true".
% T(x) means "x is a truthteller".
% L(x) means "x is a liar".
% Says(x,y) = x makes a statement y.  

set(hyper_res).


list(axioms).

P(T(x)) | P(L(x)).
-P(T(x)) | -P(L(x)).
-P(T(x)) | -P(Says(x,y)) | P(y).
-P(y) | -P(Says(x,y)) | P(T(x)).
% if P(L(x)) & P(Says(x,y)) then -P(y). (dependent axiom)
% if -P(y) & P(Says(x,y)) then P(L(x)). (dependent axiom)

end_of_list.


list(sos).

P(Says(A,Unknown)).
P(Says(B,Says(A,L(A)))).
P(Says(C,L(B))).

end_of_list.
