PROLOG: ayuda con A. de resolución

[paper_dark_angel]

Añado:

He revisado el programa y he hecho algunos cambios, y parece en principio que funciona (no he hecho tampoco demasiadas pruebas), pero es un simple parche, realmente no se cual era el problema, y diría que me ha salido de chiripa, así que si alguno lo sabe por favor decidmelo

Aquí estan los cambios

conseguir_resolvente(S,[R3|S]):-
member(C1,S),member(C2,S),
clashing(C1,C2),
append(C1,C2,R1),
limpiar_complementarios(R1,R2),
limpiar_repetidos(R2,R3),
not(member(R3,S)).

(le he quitado eso de que se cargue las clausulas contradictorias y que no calcule resolventes que ya esten calculadas de antes)


resolve_set(S):-
conseguir_resolvente(S,S2),!,
resolve_set(S2).


(le he metido un corte detrás de lo de conseguir_resolvente, en plan "si ya has encontrado una nueva, no sigas buscando, añadela, y empieza desde el principio")


Parece funcionar mejor, pero me sigue sin gustar demasiado la visión general, ya que no lo comprendo del todo... (y no, no soy creyente)