%%%
%%% This is Lei Qian's solution to the Logic Puzzle assignment
%%% P515, Spring 2001
%%%
%%%
th_Ha: THEORY
 BEGIN

  domain: TYPE = {A, B, C, D}

  range: TYPE = {X, Y, W, Z}

  f: VAR [domain -> range]

  oneone(f): bool = (FORALL (d1, d2: domain): f(d1) = f(d2) => d1 = d2)

  onto(f): bool = (FORALL (r: range): (EXISTS (d: domain): f(d) = r))

  corresp(f): bool = oneone(f) AND onto(f)

  solves_the_puzzle(f): bool =
      (f(A) /= X => f(C) /= Y) AND
       (f(B) = Y OR f(B) = Z => f(A) = X) AND
        (f(C) /= W => f(B) = Z) AND
         (f(D) = Y => f(B) /= X) AND (f(D) /= X => f(B) = X)

  puzzle_1: THEOREM NOT (EXISTS f: (corresp(f) AND solves_the_puzzle(f)))


  th1: THEOREM FORALL f: corresp(f) AND solves_the_puzzle(f) implies f(B)=X

  th2: THEOREM FORALL f: corresp(f) AND solves_the_puzzle(f) implies f(C)=W

  th3: THEOREM FORALL f: corresp(f) AND solves_the_puzzle(f) implies (f(A)=Y AND f(D)=Z)


 END th_Ha



%%%
% The next puzzle is
% REQUIRED for P515 
% OPTIONAL EXTRA CREDIT for P415 (strongly recommended: you try it, at least).
%%%

th_Hb: THEORY
BEGIN
%%%
%
% Example #1 of the Dell Book of Logic Problems No. 6,
% E.L. Rothstein (ed.), Dell Publishing, New York 1996
% ISBN: 0-440-50738-3
% 
% A young woman attending a party was introduced to four men in rather
% rapid succession and, as usual at such gatherings, there respective
% types of work wer mentioned rather early in the conversation.
% Unfortunately, she was afflicted with a somewhat faulty memory.
% Half an hour later, she could remember only that she had met a
% Mr. Brown, a Mr. White, a Mr. Black, and a Mr. Green.  She recalled that
% among them were a photographer, a grocer, a banker and a singer,
% but she could not recall which was which.  Her hostess, a fun-loving
% friend, refused to refresh her memory, but offered four clues.  Happlily,
% the young woman's logic was better than her memory, and she quickly
% paired each man with his profession.  Can you? Here are the clues:
% 
% 1. Mr. White approached the banker for a loan.
% 2. Mr. Brown had met the photographer when he hired him to take pictures of
%    his wedding
% 3. The singer and Mr. White are friends but they have never had business
%    dealings. 
% 4. Neither Mr. Black nor the singer had ever met Mr. Green before that
%    evening.
%
% The book describes a solution process of filling in a matrix with
% Xs (indicating a contradiction) and +s (indicating a solution) to
% accumulate an answer.  This is done by evaluating the clues repeatedly
% as information is accumulated.  In this example the result after two
% iterations is:
%
%            Black   Brown   Green   White
%    banker    X2      X1              X1  
%    grocer    X2      X1      X2      +2  
%    photog    +2      X1      X2      X2  
%    singer    X1      +1      X1      X1  
%
%%%

people: TYPE = {Brown, White, Black, Green} 
p,q,r: VAR people

professions: TYPE = {photographer, grocer, banker, singer}

%
% The statement of the clues, as I have translated them, also involves a
% relation "knows". 
%
job: VAR [people -> professions]
oneone(job):bool = (FORALL p,q: job(p) = job(q) => p = q)
onto(job):bool = (FORALL (j:professions): (EXISTS p: job(p)= j)) 
corresp(job):bool = oneone(job) and onto(job)

knows: VAR [people,people -> bool]
reflexive(knows):bool = (FORALL p: knows(p,p))
symetric(knows):bool = FORALL p,q: knows(p,q) IFF knows(q,p)

%
% Feel free to alter, modify, or improve this translation of the clues.
%
solves_the_puzzle(job, knows):bool =
%
% 1. Mr. White approached the banker for a loan.
%
       NOT job(White) = banker
   AND (FORALL p: job(p) = banker IMPLIES knows(White,p))
%
% 2. Mr. Brown had met the photographer when he hired him to take pictures of
%    his wedding
%
   AND (NOT job(Brown) = photographer)
   AND (FORALL p: job(p) = photographer IMPLIES knows(Brown,p))
%
% 3. The singer and Mr. White are friends but they have never had business
%    dealings [hence, White can't be the photographer, this inference might
%    be criticized as solving being part of the puzzle, but I didn't want
%    do introduce another relation for "has_had_business_dealings_with"].
%
   AND (NOT job(White) = singer)
   AND (FORALL p: singer?(job(p)) IFF knows(p, White))
   AND (FORALL p: (job(Brown) = singer AND knows(Brown,p))
         IMPLIES (NOT (p = White AND job(p) = photographer)))
%
% 4. Neither Mr. Black nor the singer had ever met Mr. Green before that
%    evening.
%
   AND NOT singer?(job(Black))
   AND NOT singer?(job(Green))
   AND (FORALL p,q: ((p = Black OR job(p) = singer) AND knows(p,q))
                IMPLIES (NOT q = Green))


%%%
%
% Again, the CONJECTURE is stated in the negative:
%   "There is no solution to the problem"
% Failure to prove this conjecture should lead to a counterexample that
% solves the problem.
%
% The commands in my .prf file include: PROP, LEMMA, GRIND, CASE, REVEAL,
% INST, SKOLEM!, ASSERT, and SPLIT, and nothing else.
%
% Hints:  Try using the "onto" property and remember together with the
%          "Professions_inclusive" axiom, which states:
%
%         FORALL (Professions_var: Professions):
%               photographer?(Professions_var) OR
%                grocer?(Professions_var) OR
%                  banker?(Professions_var) OR
%                     singer?(Professions_var);
%
%         Also, I suspect that it would be more efficient to collect the
%         FORALL quantifiers outside the conjunction.
%%%

puzzle_2: CONJECTURE 
  NOT EXISTS (job, knows):
        oneone(job) AND  onto(job)
   AND  reflexive(knows) AND  symetric(knows)
   AND solves_the_puzzle(job, knows)

Result2: THEOREM FORALL job, knows: oneone(job) AND onto(job) AND reflexive(knows)
	AND symetric(knows) AND solves_the_puzzle(job, knows) IMPLIES
	  (job(Black)=photographer AND job(Brown)=singer AND 
		job(Green)=banker AND job(White)=grocer)
END th_Hb