% problem-set/puzzles/birds/bird4.ver2.clauses
% created : 06/28/88
% revised : 08/11/88

% description:
%
% This is an input file for Chapter 9 problem 4,
% 'A Question on Agreeable Birds'.

% representation:
%

% x is equal to x.
% Clause:

EQUAL(x,x).

% For all birds x and y, there exists a bird z that composes 
% x with y for all birds w.
% Finding clause:
%    FAx FAy TEz FAw [response(z,w) = response(x,response(y,w))].
%    Letting comp(x,y) = z,j
%    response(comp(x,y),w) = response(x,response(y,w)).
% Clause:

EQUAL(response(comp(x,y),w),response(x,response(y,w))).

% Definition of agreeable: A bird x is agreeable if and only if
% for all birds y there exists a bird z such that xz = yz.
% Finding clause:
%   1) If agreeable(x) then FAy TEz [response(x,z) = response(y,z)] and
%   2) if TEx FAy TEz [response(x,z) = response(y,z)] then agreeable(x).
%   1) Letting commom_bird(y) = z,
%      -agreeable(x) | 
%         response(x,common_bird(y)) = response(y,common_bird(y)).
%   2) FAx TEy FAz -[response(x,z) = response(y,z)] | agreeable(x).
%      Letting compatible(x) = y,
%      -[response(x,z) = response(compatible(x),z)] | agreeable(x).
% Clause 1:

-agreeable(x) |
EQUAL(response(x,common_bird(y)),response(y,common_bird(y))).

% Clause 2:

-EQUAL(response(x,z),response(compatible(x),z)) | agreeable(x).
 

% Hypothesis: If C is agreeable then A is agreeable.
% Finding clause:
%    - [ If agreeable(C) then agreeable(A) ].
%    - [ -agreeable(C) | agreeable(A) ].
%    agreeable(C) and -agreeable(A).
% Denial clause:

agreeable(C).
-agreeable(A).

% C composes A with B.
% Clause:

EQUAL(C,comp(A,B)).