feldman@hermod.cs.cornell.edu (Ronen Feldman) (07/13/90)
In my former message I claimed that program2 was equivalent to program1 for every X . As Brendan Mahony pointed out to me if for some X : f1(X) and f2(X) are true but f3(X) is false then a(X) is true but a1(X) is false. I have to change the declaration of a1 to be: a1(X) :- f1(X), f2(X). a1(s(X)) :- b1(X). b1(X) :- f1(X), f2(X), f3(X). b1(s(X)) :- b1(X). I think that now a1(X) = a(X) for every X. If we want a1(X) to be equivalent to b(X) or c(X) the first clause will have to be changed to a1(X) :- f2(X), f3(X) or a1(X) :- f3(X), f1(X) accordingly. Sorry about that The query still holds, can anybody suggest an automatic way to get the new declaration? Ronen (feldman@cs.cornell.edu)