% problem-set/pelletier/p44.clauses % created : 08/17/89 % revised : 08/17/89 % description: % % Full Predicate Logic (without Identities and Functions). Problem #44 % (Ax)[Fx -> (Ey)(Gy & Hxy) & (Ez)(Gz & -Hxz)] % (Ex)[Jx & (Ay)[Gy -> Hxy]] % --------------------------- % (Ex)(Jx & -Fx) % representation: % % declare_predicates(2,[H,J]). % declare_predicates(1,[F,G,K,L]). % declare_variables([x,y,z]). % premises (all x (F(x) -> ((exists y (G(y) & H(x,y))) & (exists z (G(z) & -H(x,z)))))). (exists x (J(x) & (all y (G(y) -> H(x,y))))). % denial of conclusion -(exists x (J(x) & -F(x))).