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


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,V],
	symbole_relationnel(P),
	terme(U),
	subst1(U,S,U1),
	terme(V),
	subst1(V,S,V1),
	L1 =.. [P,U1,V1].	 
subst(L,S,L1):-
	L =.. [P,U],
	symbole_relationnel(P),
	terme(U),
	subst1(U,S,U1),
	L1 =.. [P,U1].
subst1(X,[X,I],I).
subst1(Y,[X,I],Y):- X \== Y.

/* les termes */
terme(X) :- individu(X).
terme(X) :- meta_variable(X).	 
meta_variable(X):- integer(X).	 

/* individus */
individu(I):-
	domaine_D(L),
	element(I,L).

domaine_D([pierre,henry,alain,gerard,david,benjamin,jean_pierre,yvette,deborah,delphine,vanessa]).

/* formules atomiques */

atomique(P) :-
	P =.. [R,X],
	symbole_relationnel(R),
	individu(X).
atomique(P) :-
	P =.. [R,X,Y],
	symbole_relationnel(R),
	individu(X),
	individu(Y).

/* symboles relationnels */

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


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

/* divers */

effacable(P) :- clause(P,true) , !.
non_effacable(P) :- clause(P,true),!,impasse.
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).
