/* MOTEURS D'INFERENCES  */

/* (1) Systeme d'ordre zero strict. 

Les "faits" vrais ou faux dont on parle (variables propositionelles) sont representes par des atomes Prolog, p.ex. "carre" ou "losange" pour dire qu'une certaine figure est (ou n'est pas) un carre ou un losange. Les faits connus comme vrais (qui composent la "base de faits") sont determines par le predicat "fait", p.ex. "fait(rectangle)."

Format des regles : clauses de Horn propositionnelles 
 [ conclusion | liste de  premisses ],
 connues via le predicat "regle", p.ex. "regle([carre, rectangle, losange])." Exemples complets ci-après.
*/

/*(2) Moteur en marche arriere 

Prédicat pprouver(But,EnAttente), le second argument pour eviter de boucler,
et son iteré lprouver pour listes de buts */

:- dynamic(fait/1).
:- dynamic(deduit/2).

prouver(But) :- pprouver(But, []).

pprouver(But, BEA) :- fait(But),!.
pprouver(But, BEA) :- membre(But, BEA), !, fail.
pprouver(But, BEA) :- regle([But | Premisses]),
				lprouver(Premisses, [But|BEA]), 
				assert(fait(But)),
				assert(deduit(But,  Premisses)). /* explications */
 
lprouver([], BEA).
lprouver([P|S], BEA) :- pprouver(P, BEA), lprouver(S, BEA).

membre(X, [X|S]) :- !.
membre(X, [_|S]) :- membre(X, S).

/* (3) Moteur en marche avant */

saturer :- nouveau(Y),!,  saturer.
saturer :- write('Saturation terminee'), nl.

nouveau(Z) :- regle([Z|Prem]), not(fait(Z)), lfait(Prem),
			assert(fait(Z)), /* essentiel ! */
			assert(deduit(Z, Prem)). /* pour les explications */
lfait([]).
lfait([X | R]) :- fait(X), lfait(R).


/* (4)  Module d'explication, visualisant l'arbre de preuve */

:- dynamic(deja_vu/1).

pourquoi(Fait) :- explique(Fait, 0).

explique(Fait, Prof) :- deja_vu(Fait), !, tab(Prof),
		write('Le fait "'), write(Fait), 
		write('" a ete obtenu precedemment.'), nl.
explique(Fait, Prof) :- deduit(Fait, LPrem), !, tab(Prof), 
		write('J''ai deduit "'), write(Fait), write('" de '),
		write(LPrem), nl, Profp is Prof+1,
		lexplique(LPrem, Profp),
		tab(Prof), 
		write('Ceci acheve la preuve de "'), write(Fait),
		write('"'), nl, assert(deja_vu(Fait)).

explique(Fait, Prof) :- fait(Fait), !, tab(Prof),
		write('Le fait "'), write(Fait), 
		write('" fait partie des hypotheses initiales.'), nl.

explique(Fait, Prof) :- 
		write('Mais j''ai jamais pretendu que "'), write(Fait),
		write('" !'), nl.

lexplique([], _).
lexplique([Fait|SFaits], Prof) :- explique(Fait, Prof), lexplique(SFaits, Prof).


