(Taking code from this and this)
less(0, s(_)).
less(s(X), s(Y)) :- less(X, Y).
neq(X, Y) :- less(X, Y); less(Y, X).
eq(0, 0).
eq(s(X), s(Y)) :- eq(X, Y).
horn_intersect([],_,[]).
horn_intersect(_,[],[]).
horn_intersect([X|Xs],List2,[X|Ms]) :- in(X,List2),horn_intersect(Xs,List2,Ms).
horn_intersect([X|Xs],List2,Ms) :- not_in(X,List2),horn_intersect(Xs,List2,Ms).
in(X,[K|_]) :- eq(X, K).
in(X,[K|Ms]) :- neq(X, K),in(X,Ms).
not_in(_,[]).
not_in(X,[K|Ms]) :- neq(X, K),not_in(X,Ms).
Tests:
?- horn_intersect([X], [Y], Z).
X = Y, Y = 0,
Z = [0] ;
X = Y, Y = s(0),
Z = [s(0)] ;
X = Y, Y = s(s(0)),
Z = [s(s(0))] ;
X = Y, Y = s(s(s(0))),
Z = [s(s(s(0)))] ;
X = Y, Y = s(s(s(s(0)))),
Z = [s(s(s(s(0))))] ;
X = Y, Y = s(s(s(s(s(0))))),
Z = [s(s(s(s(s(0)))))] ;
X = Y, Y = s(s(s(s(s(s(0)))))),
Z = [s(s(s(s(s(s(0))))))] ;
X = Y, Y = s(s(s(s(s(s(s(0))))))),
Z = [s(s(s(s(s(s(s(0)))))))] ;
X = Y, Y = s(s(s(s(s(s(s(s(0)))))))),
Z = [s(s(s(s(s(s(s(s(0))))))))] ;
X = Y, Y = s(s(s(s(s(s(s(s(s(0))))))))),
Z = [s(s(s(s(s(s(s(s(s(...)))))))))] ;
X = Y, Y = s(s(s(s(s(s(s(s(s(s(...)))))))))),
Z = [s(s(s(s(s(s(s(s(s(...)))))))))] .
?- horn_intersect(X, Y, Z).
X = Z, Z = [] ;
Y = Z, Z = [] ;
X = Z, Z = [0],
Y = [0|_2472] ;
X = Z, Z = [0, 0],
Y = [0|_2472] ;
X = Z, Z = [0, 0, 0],
Y = [0|_2472] ;
X = Z, Z = [0, 0, 0, 0],
Y = [0|_2472] ;
X = Z, Z = [0, 0, 0, 0, 0],
Y = [0|_2472] ;
X = Z, Z = [0, 0, 0, 0, 0, 0],
Y = [0|_2472] ;
X = Z, Z = [0, 0, 0, 0, 0, 0, 0],
Y = [0|_2472] ;
X = Z, Z = [0, 0, 0, 0, 0, 0, 0, 0],
Y = [0|_2472] ;
X = Z, Z = [0, 0, 0, 0, 0, 0, 0, 0, 0],
Y = [0|_2472] ;
X = Z, Z = [0, 0, 0, 0, 0, 0, 0, 0, 0|...],
Y = [0|_2472] ;
X = Z, Z = [0, 0, 0, 0, 0, 0, 0, 0, 0|...],
Y = [0|_2472] .