/* Demonstrateur de clauses de Horn - Parcours en largeur de l'arbre de
   recherche */
pl(D,A,P):- 		/* D: Denegation, A: Arbre de recherche, P: Preuve */
	denegation(D),
	once(bagcl(D,A)), /* Construction de l'arbre initial */
	pls([D,ou,A],P).
pls(A,P):-atrue(A,P).
pls(A,P):-
	once(exp(A)),pls(A,P).
t(L):-t0(L),exp(L),atrue(L).	
t0(L):- t1(L),exp(L).
t1([a(x),ou,L]) :- bagcl(a(X),L).

/* Recherche d'un chemin de preuve */

atrue([C,X],[C]):- X == true.
atrue(X,[C|P]):-
	nonvar(X), 
	X = [C,et,A],
	et_atrue(A,P).
atrue(X,[C|P]):-
	nonvar(X), 
	X = [C,ou,A],
	ou_atrue(A,P).
ou_atrue(X,P):-
	nonvar(X), 
	X = [T|R],
	(atrue(T,P);ou_atrue(R,P)).
et_atrue(X,[]):- X == [].
et_atrue(X,[P1|P2]):-
	nonvar(X), 
	X = [T|R],
	atrue(T,P1),et_atrue(R,P2).

/* Exploration d'un niveau de l'arbre */
exp([X,true]).
exp([C,ou,X]):-
	var(X),	bagcl(C,X).
exp([_,ou,X]):-
	nonvar(X), expr(X).
exp([_,et,X]):-
	expr(X).
expr([]).
expr([T|R]):-
	exp(T), expr(R).


/* bagcl(T,L) construit la liste L des clauses dont la tete 
   est unifiable avec T */

bagcl(T,nil):-
	not(clause(T,C)).
bagcl(T,L):-
	clause(T,C),
	once(mfa(T,C,A)),	/* mise en forme d'arbre "et" de C */
	once(add_cl(A)),
	fail.
bagcl(T,L) :- !,
	retract(cl(L)).

add_cl(C) :-
	not(cl(X)),
	assert(cl([C])).
add_cl(C) :- 
	retract(cl(L)),
	conc(L,[C],L1), 
	assert(cl(L1)).

mfa(T,true,[T,true]).
mfa(T,C,[T,et,A]):-
	mf(C,A).

mf(C,[[C,ou,_]]):-
	functor(C,X,_),
	X \== ','.
mf(C,[[C1,ou,_]|S]):-
	functor(C,',',2),
	arg(1,C,C1),
	arg(2,C,C2),
	mf(C2,S).

/* Utilitaires */

once(P):- P,!.

conc([],L,L).
conc([X|R],Y,[X|Z]):-
	conc(R,Y,Z).
hors(X,[]).
hors(X,[Y|Z]):- 
	X \== Y, 
	hors(X,Z).

/* Jeux d'essai : clauses de horn representees par des clauses Prolog */

denegation(a(X)).
a(X):- b(X), c(X).
a(3):- c(3).
b(1).
b(2).
c(X):- d(X), e(X).
c(1).
c(3).