/* LA RESOLUTION PROPOSITIONNELLE LINEAIRE POUR LES CLAUSES DE HORN 
   ================================================================= */

/* Exemples */

ref1([[p], [u], [q,p,u], [r,q], [s,r]]). but1([u,s]).
ref2([[q,p], [p,q], [r,q], [s,r], [p], [u]]). but2([u,s]).

essaih1 :- ref1(R), but1(B), write('Horn'), resh(B,R), write('OK'), nl.

essaih2 :- ref2(R), but2(B), write('Horn'), resh(B,R), write('OK'), nl.


regh(LButs, LHyp) :- setof(C, regle(C), R), append(R, LHyp, RC),
			resh(LButs, RC).

regpg(LButs, LHyp) :- setof(C, regle(C), R), append(R, LHyp, RC),
			respg(LButs, RC).

/*(2) La resolution lineaire a partir d'une liste de buts 
      ---------------------------------------------------- */

/* reshorn(LButs, LClauses, LRef, AncButs), 
  lance' par reshorn(LButs, [LButs], LRef, LRef) */

reshorn([B|SButs], [[B|Q]|SCl], LRef, AncButs) :-
		  union(Q,SButs,NButs), 
		  sreshorn(NButs, [B|SButs], SCl, LRef, AncButs).
reshorn(LButs, [_|SCl], LRef, AncButs) :- 
		  reshorn(LButs, SCl, LRef, AncButs).

sreshorn([], LButs, SCl, LRef, AncButs) :- !.
	/* Liste de buts vide = Resolvante vide, on a fini */
sreshorn(NButs, LButs, SCl, LRef, AncButs) :- 
	 		present(NButs, AncButs), !,  
			reshorn(LButs, SCl, LRef, AncButs).
sreshorn(NButs, LButs, SCl, LRef, AncButs) :- /* write(NButs), nl, */
			reshorn(NButs, LRef, LRef, [NButs|AncButs]).

union(L1, L2, Res) :- add(L1, L2, PRes), /* emprunte' a res_prop */
			sort(PRes, Res). /* pour le test "present" */
add([], X, X).
add([A|S], X, Y) :- present(A, X), !, add(S, X, Y).
add([A|S], X, [A|Y]) :-  add(S, X, Y).

present(A, [B|S]):- A=B, !. /* on teste l'egalite, pas l'identite' */
present(A, [_|S]):- present(A, S).

/* Le predicat d'appel */

resh(LButs, LCl) :- sort(LButs, SLButs),
		 reshorn(LButs, LCl, LCl, [SLButs]).


/* Résolution à la Prolog */

resprol([], LRef, LCl) :- !.
resprol([B|SButs], LRef, [[B|Q]|SCl]) :- /* sans "cut" */
		append(Q, SButs, NButs), resprol(NButs, LRef, LRef).
resprol(LButs, LRef, [_|SCl]) :- resprol(LButs, LRef, SCl).


/* Appel par...*/
respg(LButs, LCl) :- resprol(LButs, LCl, LCl).

essaip1 :- ref1(R), but1(B), write('Prolog'), respg(B,R), write('FINI').
essaip2 :- ref2(R), but2(B), write('Prolog'), respg(B,R), write('FINI').


/* Bases de règles */

regh(LButs, LHyp) :- setof(C, regle(C), R), append(R, LHyp, RC), % par la résolution SLD
                  resh(LButs, RC).

regpg(LButs, LHyp) :- setof(C, regle(C), R), append(R, LHyp, RC), % par la résolution Prolog
                  respg(LButs, RC).
