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

% description:
%
% This is an input file for Chapter 9 problem 1, 
% 'The Significance of the Mockingbird'.

% representation:
%
% There exists a mocking bird (Mock).
% Finding clause:
%    TEx FAy [response(x,y) = response(y,y)].
%    Letting Mock = x,
%    response(Mock,y) = response(y,y).
% Clause:

EQUAL(response(Mock,y),response(y,y)).

% 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,
%    response(comp(x,y),w) = response(x,response(y,w)).
% Clause:

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

% Hypothesis: Every bird is fond of at least one other bird.        
% Finding clause:
%    -FAx TEy [response(x,y) = y].
%    TEx FAy -[response(x,y) = y].
%    Letting A = x,
%    -[response(A,y) = y]. 
% Denial clause:

-EQUAL(response(A,y),y).