% problem-set/puzzles/birds/bird4.ver1.in % created : 06/28/88 % revised : 08/11/88 % description: % % This is an input file for Chapter 9 problem 4, % 'A Question on Agreeable Birds'. % For all birds x and y, there exists a bird z that composes x with y for all % birds w. % Hypothesis: If C is agreeable then A is agreeable. % representation: % set(para_from). set(para_into). set(para_from_left). set(para_from_right). list(axioms). % 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))). end_of_list. list(sos). % Hypothesis: If C is agreeable then A is agreeable. % Finding clause: % -[ If FAx TEy (response(C,y) = response(x,y)), % then FAw TEv (response(A,v) = response(w,v)) ]. % -[ TEx FAy -(response(C,y) = response(x,y)) | % FAw TEv (response(A,v) = response(w,v)) ]. % FAx TEy (response(C,y) = response(x,y)) and % TEw FAv -(response(A,v) = response(w,v). % Letting common_bird(x) = y and odd_bird = w, % response(C,commom_bird(x)) = response(x,common_bird(x)) and % -(response(A,v) = response(odd_bird,v)). % Denial clause: EQUAL(response(C,common_bird(x)),response(x,common_bird(x))). -EQUAL(response(A,v),response(odd_bird,v)). % C composes A with B. % Clause: EQUAL(C,comp(A,B)). end_of_list.