%=============================================================
%
% THE "FULL" JOBS PUZZLE -- FULL FIRST-ORDER LOGIC
% version by Selmer Bringsjord
%
%     Intro to Logic Programming & AI
%     Spring 1998
%
% There are four people:  Roberta, Thelma, Steve, and Pete.
% Among them, they hold eight different jobs.  Each holds
% exactly two jobs.  The jobs are chef, guard, nurse, clerk,
% police officer (gender open), teacher, actor, and boxer.
% The husband of the chef is the clerk.  Roberta is not a boxer.
% Pete has no education poast the ninth grade.  Roberta, the
% chef, and the police officer went golfing together.
%
%=============================================================


set(auto).
assign(max_proofs,1).

formula_list(usable).


% ---- Gender of four people in puzzle:
Female(roberta).
Female(thelma).
Male(steve).
Male(pete).


% ---- The four people in the puzzle are distinct:
-Equalp(roberta,thelma).
-Equalp(roberta,steve).
-Equalp(roberta,pete).
-Equalp(thelma,steve).
-Equalp(thelma,pete).
-Equalp(pete,steve).


% ---- The two jobs a person holds are distinct:
all x -Equalj(job1(x),job2(x)).


% ---- Enforce reflexivity of equality predicates:
all x Equalp(x,x).
all x Equalj(x,x).
all x Equal(x,x).


% ---- Everyone is female or male, bot not both:
all x (Female(x) <-> -Male(x)).


% ---- Roberta is not the boxer:
-HasJob(roberta,boxer).


% ---- The job of nurse is held by a male:
all x (HasJob(x,nurse) -> Male(x)).


% ---- The job of actor is held by a male:
all x (HasJob(x,actor) -> Male(x)).


% ---- Every person has two jobs:
all x (HasJob(x,job1(x))).
all x (HasJob(x,job2(x))).


% ---- Every job is held by a person.
all x (HasJob(jobholder(x),x)).


% ---- The husband of the chef is the clerk:
all x (Husband(x,jobholder(chef)) -> HasJob(x,clerk)).
all x (HasJob(x,clerk) -> Husband(x,jobholder(chef))).
Female(jobholder(chef)).


% ---- Husbands are male and their wives are female:
all x all y (Husband(x,y) -> (Male(x) & Female(y))).


%=============================================================
% Education Level Info:
%
%---- Pete's education level isn't greater than 9th grade:
-Greater(ed-level(pete),9).

%---- Nurses have education beyond the 9th grade:
all x ( HasJob(x,nurse) -> Greater(ed-level(x),9)).

%---- Police Officers have education beyond the 9th grade:
all x ( HasJob(x,policeofficer) -> Greater(ed-level(x),9)).

%---- Teachers have education beyond the 9th grade:
all x ( HasJob(x,teacher) -> Greater(ed-level(x),9)).
%=============================================================


%=============================================================
% The Golfing Information
% (Note:  Some versions of the "full" jobs puzzle don't include
% the info that produces what humans infer from the English
% sentence in question (e.g., that Roberta cannot have the job
% of the chef).  In this version, these facts are deduced from
% more fundamental facts about golfing and common-sense.  
% On the other hand, even this version "cheats":  it assumes 
% that in the three-place predicate Golfed the second and
% third places are invariably filled by job names, not the
% names of people.)
%
% First, who golfed together:
Golfed(roberta,chef,policeofficer).
%
% 
% The implication that these are three distinct golfers:
all x all y all z ( (Golfed(x,y,z)) ->
      (-HasJob(x,y) & -HasJob(x,z))).
%
all x all y all z ( (Golfed(x,y,z)) ->
      (all z1 (HasJob(z1,y) -> -HasJob(z1,z)))).
%
all x all y all z ( (Golfed(x,y,z)) ->
      (all z1 (HasJob(z1,z) -> -HasJob(z1,y)))).
%=============================================================


% ---- If x holds job y and y isn't x's second job, then y is
% ---- is x's first job:
all x all y ( (HasJob(x,y) & -Equalj(y,job2(x))) ->
     Equalj(y,job1(x))).


% ---- If x and z are distinct people, and x holds job y, then
% ---- z cannot hold job y:
all x all y all z ( (-Equalp(x,z) & HasJob(x,y)) ->
     -HasJob(z,y)).


% ---- If the jobholder of x is female, and Roberta doesn't
% ---- have the job x, then Thelma does:
all x ( (Female(jobholder(x)) & -HasJob(roberta,x)) ->
     HasJob(thelma,x)).

% ---- If the jobholder of x is male, and Steve doesn't
% ---- have the job x, then Pete does:
all x ( (Male(jobholder(x)) & -HasJob(steve,x)) ->
     HasJob(pete,x)).



%=============================================================
% OUTPUT SECTION

%HasJob(roberta,boxer).
%HasJob(roberta,nurse).
%HasJob(roberta,actor).
%HasJob(roberta,chef).
%HasJob(roberta,policeofficer).
HasJob(roberta,clerk).

%-HasJob(roberta,clerk) -> $ANSWER(roberta,IS_NOT_THE,clerk).
%-HasJob(roberta,boxer) -> $ANSWER(roberta,IS_NOT_THE,boxer).

%all x (  (-HasJob(x,boxer) & -HasJob(x,nurse) &
%  -HasJob(x,actor) & -HasJob(x,chef) &
% -HasJob(x,policeofficer)
%  & -HasJob(x,clerk)) -> (HasJob(x,teacher) &
%    HasJob(x,guard))).

%all x (  (-HasJob(x,boxer) & -HasJob(x,nurse) &
%  -HasJob(x,actor) & -HasJob(x,chef) & -HasJob(x,policeofficer)) ->
%   (HasJob(x,teacher) & HasJob(x,guard))).

all x (  (-HasJob(x,boxer) & -HasJob(x,nurse) &
  -HasJob(x,actor) & -HasJob(x,chef) & -HasJob(x,policeofficer) &
  -HasJob(x,clerk)) ->
   (HasJob(x,teacher) & HasJob(x,guard))).

-HasJob(roberta,guard).




%-(all x (HasJob(x,chef) -> -HasJob(x,policeofficer))).
%-(all x (HasJob(x,chef) -> -HasJob(x,policeofficer))).

%-HasJob(roberta,actor) -> HasJob(roberta,teacher).
%-HasJob(roberta,teacher).




end_of_list.