% problem-set/puzzles/truth.lies/knightknave.in
% created : 08/08/88
% revised : 08/17/89

% description :
%
% The husband & wife problem : if he's a knight, so is she.

% representation :
%
% g(x) means that x is good, i.e. x is a knight
% b(x) means that x is bad, i.e. x is a knave
% s(x,y) means that x makes the statement y
% p(x) means that x is a person
% S(x) refers to the statement made by x

set(ur_res).
set(para_from).
set(para_into).
assign(max_literals,5).
set(free_all_mem).
set(unit_deletion).

list(axioms).

%  everyone's either a knight or a knave; statements are true or false.
-p(x) | g(x) | b(x).
-p(x) | -g(x) | -b(x).
-s(x,y) | true(y) | -true(y).

%  rules about statements:
-s(x,y) | -eq(x,y).
-s(x,y) | eq(y,S(x)).
-p(x) | -eq(x,S(y)).
-p(x) | -true(S(x)) | g(x).
-p(x) | true(S(x)) | b(x).

%  rules about equalities:
eq(x,x).
-eq(x,y) | eq(y,x).
-eq(x,y) | -eq(y,z) | eq(x,z).
-eq(x,y) | -g(x) | g(y).
-eq(x,y) | -b(x) | b(y).
-eq(x,y) | -p(x) | p(y).
-eq(x,y) | -s(x,z) | s(y,z).
-eq(x,y) | -s(z,x) | s(z,y).
-eq(x,y) | -true(x) | true(y).

%  what knights say is true, what knaves say is false:
-g(x) | -s(x,y) | true(y).
-b(x) | -s(x,y) | -true(y).

end_of_list.


list(sos).

%  this is for the husband & wife problem; if he's a knight, then she is.
p(h).
p(j).
-eq(h,j).
s(h,S(h)).
-true(S(h)) | -g(h) | g(j).
true(S(h)) | -g(h).
true(S(h)) | g(j).
-g(j) | true(S(h)).
-g(h).

end_of_list.

