/*  L'algorithme de Wang  en Prolog  */

/*  Dans ce programme, on repre'sente la se'quence courante comme 
    un couple de listes de termes Antec et Conseq . 
    Ces termes seront e'crits avec la syntaxe concre`te habituelle, 
    les connecteurs binaires en position infixe'e a` trois niveaux de priorite's. 
    Pour e'viter les conflits avec la syntaxe des listes Prolog, qui utilise le symbole "|", 
    on revient ici aux noms français des connecteurs, 
    et on introduit donc les conventions ne'cessaires a` l'usage du lecteur Prolog comme suit  : 
*/

:- op(900, yfx, [imp]) .
:- op(800, yfx, [ou]) .
:- op(700, yfx, [et]) .
:- op(600, fx, [non]) .

/*  Il sera utile de ve'rifier si Antec et Conseq ont ou non une formule en commun. 
    La solution ici retenue s'applique a` des formule atomiques repre'sente'es par des atomes Prolog.
    Il faudra la raffiner pour traiter des objets plus complexes. 
*/

inter(L, M) :-concat(X, [A|Y], L), concat(U, [A|V], M).

concat([], X, X).  
concat([A|X], Y, [A|Z]) :- concat(X, Y, Z).

/* Les deux listes de formules Antec et Conseq seront ge're'es avec les formules
   non-triviales en te^te et les variables (formules atomiques) en queue ;
   de'finissons donc comment une nouvelle formule doit s'ajouter a` une liste.
*/

consp(X imp Y). consp(X ou Y). consp(X et Y). consp(non X).

ajouter(F, L, [F|L]) :- consp(F), !.
ajouter(F, L, M) :- concat(L, [F], M).

/* Enonçons a` pre'sent les re`gles gouvernant la validite' d'une se'quence. 
   Le pre'dicat valide sera charge' en outre de ramener la liste des e'ventuels contre-exemples 
   pour les propositions  qui ne sont pas des tautologies. 
   On rappelle que cette liste peut e^tre vue comme une repre'sentation de la proposition 
   en forme  conjonctive re'duite.
*/

valide(Antec, Conseq, []) :- inter(Antec, Conseq), !.

/* Les re`gles visant la ne'gation.*/
valide( [non X | R], Conseq, Contrex) :- ! , 
	ajouter(X, Conseq, Ncsq), valide(R, Ncsq, Contrex).

valide(Antec , [non X | R], Contrex) :- !, 
	ajouter(X, Antec, Ntc), valide(Ntc, R, Contrex).

/* Les re`gles re'gissant la disjonction.*/

 valide( [X ou Y | R], Conseq, Contrex) :- !,
     ajouter(X, R, Ntc1), valide(Ntc1, Conseq, Contrex1),
     ajouter(Y, R, Ntc2), valide(Ntc2, Conseq, Contrex2),
	concat(Contrex1, Contrex2, Contrex).

 valide(Antec, [X ou Y | R], Contrex) :- !,
     ajouter(X, R, Ncsq1), ajouter(Y, Ncsq1, Ncsq2),
     valide(Antec, Ncsq2, Contrex).

/* Les re`gles sur la conjonction.*/

 valide([X et Y | R], Conseq, Contrex) :- !,
     ajouter(X, R, Ntc1), ajouter(Y, Ntc1, Ntc2),
     valide(Ntc2, Conseq, Contrex).

 valide(Antec, [X et Y | R], Contrex) :- !,
     ajouter(X, R, Ncsq1), valide(Antec, Ncsq1, Contrex1),
     ajouter(Y, R, Ncsq2), valide(Antec, Ncsq2, Contrex2),
	concat(Contrex1, Contrex2, Contrex).


/* Enfin, les re`gles sur l'implication.*/

 valide([X imp Y | R], Conseq, Contrex) :- !,
     ajouter(Y, R, Ntc), valide(Ntc, Conseq, Contrex1),
     ajouter(X, Conseq, Ncsq), valide(R , Ncsq, Contrex2),
	concat(Contrex1, Contrex2, Contrex).


 valide(Antec, [X imp Y | R], Contrex) :- !,
     ajouter(X, Antec, Ntc), ajouter(Y, R, Ncsq),
     valide(Ntc, Ncsq, Contrex).

 /* Et si aucune des situations pre'ce'dentes ne se pre'sente, c'est que toutes les
formules sont atomiques, et comme Antec et Conseq ont une intersection vide,
il s'ensuit que la se'quence n'est pas valide.*/

valide(Antec, Conseq, [[Antec, Conseq]]) :- !, 
	write('Pas une tautologie'),  nl.     

/* Ceci acheve la de'finition du pre'dicat "valide" ; voici un pre'dicat "top-level" pour le mettre en œuvre commode'ment.*/

wang(Formule, Cx) :- valide([], [Formule], Cx), 
								write('OK'), nl.

/* Quelques exemples de tautologies (fabriquer des non-tautologies, c'est plus facile!) . */

w1 :- wang(a ou non a, []).

w2 :- wang(a imp (b imp a), []).

w3 :- wang((a ou b) et non a imp b, []).

w4 :- wang((a imp b) imp (non b imp non a), []).

w5 :- wang((a imp b) et a imp b, []).

w6 :- wang(non a ou (b imp c) imp a et non b ou (a imp c), []).

myst :- wang((pp imp qq) et 
		   (qq imp rr) et 
		   (rr imp ss) et 
		   (tt imp non ss) imp (pp imp non tt), []).

big :- wang(
		(x et y et u) ou (non x et non y et u) ou
		(non x et y et non u) ou (x et non y et non u)
		ou
		(non x et y et v) ou (x et non y et v) ou
		(x et y et non v) ou (non x et non y et non v)
		ou
		(non z et t et v) ou (z et non t et v) ou
		(z et t et non v) ou (non z et non t et non v)
		ou
		(non z et t et u) ou (z et non t et u) ou
		(z et t et non u) ou (non z et non t et non u)
		, []).

/*
-----------------------------------------------------------------
| ?- myst.
OK

yes
| ?- wang(d ou c imp a et non b ou c, X).
Pas une tautologie
Pas une tautologie
OK

X = [[[d],[c,a]], [[d,b],[c]]]
yes

*/
