% Evaluation de formules logiques : deuxi\`eme m\'ethode de calcul (v2)


valeur_semantique(P,vrai) :-
	atomique(P),
	effacable(P). 
valeur_semantique(P,faux) :-
	atomique(P),
	non_effacable(P). 
valeur_semantique(non(P),V) :-
	valeur_semantique(P,V1),
	non(V1,V).
valeur_semantique(et(P,Q),V) :-
	valeur_semantique(P,V1),
	valeur_semantique(Q,V2),
	et(V1,V2,V).
valeur_semantique(ou(P,Q),V) :-
	valeur_semantique(non(et(non(P),non(Q))),V).
valeur_semantique(existe(X,P),V) :-
	valeur_semantique(non(tout(X,non(P))),V).
valeur_semantique(tout(X,P),V) :- 
	domaine_D(D),
	liste_valeurs_semantiques(D,[X,P],V1),
	tous_vrais(V1,V).  

non(vrai,faux).
non(faux,vrai).
et(vrai,vrai,vrai).
et(_,faux,faux).
et(faux,_,faux).

liste_valeurs_semantiques([],[X,P],[]).
liste_valeurs_semantiques([I|D],[X,P],[V|L]):-
	subst(P,[X,I],P1),
	valeur_semantique(P1,V),
	liste_valeurs_semantiques(D,[X,P],L).

tous_vrais([],vrai).
tous_vrais([faux|_],faux).
tous_vrais([vrai|L],V) :-
	tous_vrais(L,V).

/* substitutions */
subst(existe(X,P),[X,I],existe(X,P)).  /* X n'est pas libre ici */
subst(existe(Y,P),[X,I],existe(Y,P1)) :-
	X \== Y,
	subst(P,[X,I],P1).
subst(tout(X,P),[X,I],tout(X,P)).  /* X n'est pas libre ici */
subst(tout(Y,P),[X,I],tout(Y,P1)) :-
	X \== Y,
	subst(P,[X,I],P1).
subst(et(U,V),S,et(U1,V1)):-
	subst(U,S,U1),
	subst(V,S,V1).
subst(ou(U,V),S,ou(U1,V1)):-
	subst(U,S,U1),
	subst(V,S,V1).
subst(non(U),S,non(U1)):-
	subst(U,S,U1).
subst(L,S,L1):-
	L =.. [P|U],
	symbole_relationnel(P,A),
	subst_terme(A,U,S,U1),
	L1 =.. [P|U1].	 
subst_terme(1,[T],S,[T1]):-
	terme(T),
	subst1(T,S,T1).
subst_terme(N,[T|Ts],S,[T1|Ts1]):-
	N > 1,
	terme(T),
	subst1(T,S,T1),
	N1 is N - 1,
	subst_terme(N1,Ts,S,Ts1).

subst1(X,[X,I],I).
subst1(Y,[X,I],Y):- X \== Y.

/* les termes */
terme(X) :- 	
	individu(X).
individu(X) :-
	domaine_D(L),
	element(X,L).
terme(X) :- meta_variable(X).	 
meta_variable(X):- integer(X).	 

/* individus */
individus(1,[I],L):-
		element(I,L).
individus(N,[I|Is],L):-
		N > 1,
		element(I,L),
		N1 is N - 1,
		individus(N1,Is,L).
domaine_D([pierre,henry,alain,gerard,david,benjamin,jean_pierre,yvette,deborah,delphine,vanessa]).

/* formules atomiques */

atomique(P) :-
	P =.. [R|Is],
	symbole_relationnel(R,A),
	domaine_D(L),
	individus(A,Is,L).


/* symboles relationnels */

symbole_relationnel(R,A) :-
	domaine_R(L),
	element(R-A,L).


domaine_R([homme-1,femme-1,pere-2,mere-2,enfant-2,fils-2,fille-2,parent-2,frere-2,soeur-2,grand_pere-2,grand_mere-2,oncle-2,tante-2,cousine-2,cousin-2]).

/* divers */

effacable(P) :- clause(P,true) ,!.
non_effacable(P) :- clause(P,true) ,!,fail.
non_effacable(P).

element(E,[E|L]).
element(E,[X|L]) :- element(E,L).

/* Reponses */
reponse(est_ce_que(F),oui):-
	valeur_semantique(F,vrai).
reponse(est_ce_que(F),"je ne sais pas "):-
	valeur_semantique(F,faux).
reponse(quel(X,F),I):-
	individu(I),
	subst(F,[X,I],F1),
	valeur_semantique(F1,vrai).
reponse(quel(X,F),"je ne sais pas"):-
	valeur_semantique(tout(X,non(F)),vrai).

/* Jeu d'essai */

fils(david,henry).
fils(benjamin,henry).
fils(jean_pierre,alain).
frere(alain,henry).

q1(R) :- reponse(est_ce_que(existe(2,fils(2,henry))),R).
q2(R) :- reponse(quel(2,fils(2,henry)),R).
q3(R) :- reponse(quel(2,et(frere(2,henry),existe(3,fils(3,2)))),R).
