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 (·······@cs.cornell.edu)