Prolog: Resolvent/Resolution solver and recursion-CodePudding

Given 2 lists of positiv and negativ literals (representing clauses) I want to to get all possible Resolutions of these 2 clauses.

resolution([pos(X)|T],[H2|T2],R):- select(neg(X), [H2|T2],L),union(T,L,R).
resolution([neg(X)|T],[H2|T2],R):- select(pos(X),[H2|T2],L),union(T,L,R).   
resolution([H|T],[H2|T2],R):-resolution(T,[H2|T2],R).

This works for the first literal of the first list ([H|T]) but for after that due to how I wrote the recursion I lose the Head of the list after every recursion so that I don't get the whole union of my 2 original list but the union of the second list and the the subset of the first list after the deleted literal.

I couldn't figure out how I (try to) do a resolution for every element of the first list with the second whilst keeping all elements of the first list.

My idea is something like this:

resolution([[_]|[pos(X)|T]],[H2|T2],R):- select(neg(X),[H2|T2],L),select(pos(X),[[_]|[pos(X)|T]],Q),union(Q,L,R).
resolution([[_]|[neg(X)|T]],[H2|T2],R):- select(pos(X),[H2|T2],L),select(neg(X),[[_]|[neg(X)|T]],Q),union(Q,L,R). 
resolution([[_]|[neg(X)|T]],[H2|T2],R):-resolution([[[_]|[neg(X)]]|T],[H2|T2],R).

Trying to shift the element I am using for the resolution while keeping my list how it was but this doesn't work at all at the moment.

What the upper codes outputs:

?-resolution([pos(1),neg(3),pos(4)],[neg(1),pos(3),neg(5)],R).
R = [neg(3), pos(4), pos(3), neg(5)] 
R = [pos(4), neg(1), neg(5)]

(resolution with pos(1),neg(1) and neg(3),pos(3))

What it I want it to output:

?-resolution([pos(1),neg(3),pos(4)],[neg(1),pos(3),neg(5)],R).

R = [neg(3), pos(4), pos(3), neg(5)]
R = [pos(1),pos(4), neg(1), neg(5)]

Keeping the pos(1) of the first list.

CodePudding user response：

"Shifting" an element to the "result" list can be done by using the list constructor [_ | _] in the "result" parameter as well, i.e., changing the last clause of your original program to:

resolution([pos(X)|T],[H2|T2],R):- select(neg(X), [H2|T2],L),union(T,L,R).
resolution([neg(X)|T],[H2|T2],R):- select(pos(X),[H2|T2],L),union(T,L,R).
resolution([H|T], [H2|T2], [H | R]) :-
    resolution(T, [H2|T2], R).

And there you go:

?- resolution([pos(1),neg(3),pos(4)],[neg(1),pos(3),neg(5)],R).
R = [neg(3), pos(4), pos(3), neg(5)] ;
R = [pos(1), pos(4), neg(1), neg(5)] ;
false.

This isn't perfect, for what if H is already present in R? It would be duplicated in the result. So maybe change to this:

resolution([pos(X)|T],[H2|T2],R):- select(neg(X), [H2|T2],L),union(T,L,R).
resolution([neg(X)|T],[H2|T2],R):- select(pos(X),[H2|T2],L),union(T,L,R).
resolution([H|T], [H2|T2], Resolvent) :-
    resolution(T, [H2|T2], R),
    union([H], R, Resolvent).

It's a bit of a pity that this loses the tail recursivity of the predicate.

For whatever it's worth, I don't see why you bother with recursion at all. What you are trying to do amounts to selecting an element from a list and keeping all other elements around. Your implementation of this, with the small fix from my first version, is basically an unfolded version of select/3 itself. Why not go full select/3? Like this:

resolution(ClauseA, ClauseB, Resolvent) :-
    select(Literal, ClauseA, RestA),
    literal_opposite(Literal, OppositeLiteral),
    select(OppositeLiteral, ClauseB, RestB),
    union(RestA, RestB, Resolvent).

literal_opposite(pos(X), neg(X)).
literal_opposite(neg(X), pos(X)).

This is actually pretty close to a textbook definition of resolution.