% ordered resolution as chaining:
% implication is denoted by ``implies''.


:-op(600,xfx,implies).

precedence([ implies ,a,b,neg]).

X implies Y, Y implies Z -> X implies Z.
X implies Y, Y implies X -> X=Y.
X implies X.


neg(X)=X -> [].
X implies Y -> neg(Y) implies neg(X).
neg(neg(X))=X.

neg(a)  implies  b.
a  implies  b.
neg(a)  implies  neg(b).
a  implies  neg(b).