% problem-set/puzzles/birds/bird7.ver1.in % created : 06/28/88 % revised : 08/11/88 % description: % % This is an input file for Chapter 9 problem 7, % 'Happy Birds'. % First part of denial clause: there exists a bird which is fond of some other % bird. Hypothesis: Any bird that is fond of at least one bird must be happy. % representation: % set(UR_res). 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). % First part of denial clause: there exists a bird which is fond % of some other bird. EQUAL(response(A,B),B). end_of_list. list(sos). % Hypothesis: Any bird that is fond of at least one bird must be happy. % Finding clause: % - FAx [If TEy (xy = y) then TEz TEw (xz = w) and (xw = z)]. % TEx -[- TEy (xy = y) | TEz TEw ((xz = w) and (xw = z))]. % TEx [ TEy (xy = y) and - TEz TEw ((xz = w) and (xw = z)) ]. % TEx [ TEy (xy = y) and FAz FAw -((xz = w) and (xw = z)) ]. % Letting A = x, % TEy (Ay = y) and FAz FAw -[(Az = w) and (Aw = z)]. % Letting B = y, % (AB = B) and [-(Az = w) | -(Aw = z)]. % Denial clause: % Placing (AB = B) in the list of axiom, we have: -EQUAL(response(A,z),w) | -EQUAL(response(A,w),z). end_of_list.