I have a knowledge base with the following:
numeral(0).
numeral(s(X)) :- numeral(X).
numeral(X+Y) :- numeral(X), numeral(Y).
add(0,X,X).
add(s(X),Y,s(Z)) :- add(X,Y,Z).
add2(W+X,Y+Z,R) :- add(W,X,A),add(Y,Z,T),add2(A,T,R).
add2(X+Y,Z,R) :- add(X,Y,A),add2(A,Z,R).
add2(X,Y+Z,R) :- add(Y,Z,A),add2(X,A,R).
add2(X,Y,R) :- add(X,Y,R).
which evaluates correctly queries such as:
?- add2(s(0)+s(s(0)), s(s(0)), Z).
Z = s(s(s(s(s(0)))))
?- add2(0, s(0)+s(s(0)), Z).
Z = s(s(s(0)))
?- add2(s(s(0)), s(0)+s(s(0)), Z).
Z = s(s(s(s(s(0)))))
However the following query is evaluated to:
?- add2(s(0)+s(0), s(0+s(s(0))), Z).
Z = s(s(s(0+s(s(0))))) .
But the required output is:
?- add2(s(0)+s(0), s(0+s(s(0))), Z).
Z = s(s(s(s(s(0)))))
I know the issue is with the line:
add2(W+X,Y+Z,R) :- add(W,X,A),add(Y,Z,T),add2(A,T,R).
But i just can't figure it out. Any help would be appreciated!
I think you make the problem more complex by handling the cases with an add2/3 predicate. You first need to resolve the structure of the first two arguments to something of the shape s(s(...s(0)...)).
In order to do this, we can make an resolve/2 function that looks for (+)/2 terms and recursively works with add/3:
resolve(0,0).
resolve(s(X),s(Y)) :-
resolve(X,Y).
resolve(X+Y,Z) :-
resolve(X,RX),
resolve(Y,RY),
add(RX,RY,Z).
So now for a grammar:
E -> 0
E -> s(E)
E -> E + E
resolve/2 will convert this to a grammar with:
E -> 0
E -> s(E)
For example:
?- resolve(s(0)+s(0),X).
X = s(s(0)).
?- resolve(s(0+s(s(0))),X).
X = s(s(s(0))).
And now our add2/3 predicate will first resolve/2 the operands, and then add these together:
add2(A,B,C) :-
resolve(A,RA),
resolve(B,RB),
add(RA,RB,C).
The sample queries you then write resolve to:
?- add2(s(0)+s(s(0)), s(s(0)), Z).
Z = s(s(s(s(s(0))))).
?- add2(0, s(0)+s(s(0)), Z).
Z = s(s(s(0))).
?- add2(s(s(0)), s(0)+s(s(0)), Z).
Z = s(s(s(s(s(0))))).
?- add2(s(0)+s(0), s(0+s(s(0))), Z).
Z = s(s(s(s(s(0))))).