:-op(50,fy,ne).
:-op(55,yfx,<=>).
:-op(60,yfx,=>).
:-op(65,yfx,i).
:-op(65,yfx,ili).

skini_ekv(<=>(Ai,Bi),i(=>(Ao,Bo),=>(Bo,Ao))):-
  skini_ekv(Ai,Ao),
  skini_ekv(Bi,Bo).
skini_ekv(=>(Ai,Bi),=>(Ao,Bo)):-
  skini_ekv(Ai,Ao),
  skini_ekv(Bi,Bo).
skini_ekv(i(Ai,Bi),i(Ao,Bo)):-
  skini_ekv(Ai,Ao),
  skini_ekv(Bi,Bo).
skini_ekv(ili(Ai,Bi),ili(Ao,Bo)):-
  skini_ekv(Ai,Ao),
  skini_ekv(Bi,Bo).
skini_ekv(ne(Ai),ne(Ao)):-
  skini_ekv(Ai,Ao).
skini_ekv(A,A).

skini_imp(=>(Ai,Bi),ili(ne(Ao),Bo)):-
  skini_imp(Ai,Ao),
  skini_imp(Bi,Bo).
skini_imp(i(Ai,Bi),i(Ao,Bo)):-
  skini_imp(Ai,Ao),
  skini_imp(Bi,Bo).
skini_imp(ili(Ai,Bi),ili(Ao,Bo)):-
  skini_imp(Ai,Ao),
  skini_imp(Bi,Bo).
skini_imp(ne(Ai),ne(Ao)):-
  skini_imp(Ai,Ao).
skini_imp(A,A).

udubi(ne(ne(Ai)),Ao):-
  udubi(Ai,Ao).
udubi(ne(i(Ai,Bi)),ili(C,D)):-
  udubi(Ai,Ao),
  udubi(Bi,Bo),
  udubi(ne(Ao),C),
  udubi(ne(Bo),D).
udubi(ne(ili(Ai,Bi)),i(C,D)):-
  udubi(Ai,Ao),
  udubi(Bi,Bo),
  udubi(ne(Ao),C),
  udubi(ne(Bo),D).
udubi(i(Ai,Bi),i(Ao,Bo)):-
  udubi(Ai,Ao),
  udubi(Bi,Bo).
udubi(ili(Ai,Bi),ili(Ao,Bo)):-
  udubi(Ai,Ao),
  udubi(Bi,Bo).
udubi(ne(Ai),ne(Ao)):-
  udubi(Ai,Ao).
udubi(A,A).

normiraj(ili(Ai,Bi),C):-
  normiraj(Ai,Ao),
  normiraj(Bi,Bo),
  distribuiraj(ili(Ao,Bo),C).
normiraj(i(Ai,Bi),i(Ao,Bo)):-
  normiraj(Ai,Ao),
  normiraj(Bi,Bo).
normiraj(A,A).

distribuiraj(ili(A,i(B,C)),i(D,E)):-
  distribuiraj(ili(A,B),D),
  distribuiraj(ili(A,C),E).
distribuiraj(ili(i(A,B),C),i(D,E)):-
  distribuiraj(ili(A,C),D),
  distribuiraj(ili(B,C),E).
distribuiraj(A,A).

asociraj(i(i(A,B),C),D):-
  asociraj(i(A,i(B,C)),D).
asociraj(i(Ai,Bi),i(Ao,Bo)):-
  asociraj(Ai,Ao),
  asociraj(Bi,Bo).
asociraj(ili(ili(A,B),C),D):-
  asociraj(ili(A,ili(B,C)),D).
asociraj(ili(Ai,Bi),ili(Ao,Bo)):-
  asociraj(Ai,Ao),
  asociraj(Bi,Bo).
asociraj(A,A).

lista_i(i(Ai,Bi),[Ao|Bo]):-
  lista_ili(Ai,Ao),
  lista_i(Bi,Bo).
lista_i(Ai,[Ao]):-
  lista_ili(Ai,Ao).

lista_ili(ili(Ai,Bi),[Ao|Bo]):-
  lista_ne(Ai,Ao),
  lista_ili(Bi,Bo).
lista_ili(Ai,[Ao]):-
  lista_ne(Ai,Ao).

lista_ne(ne(A),-A).
lista_ne(A,A).

provera([A|B]):-
  clan(A,P),
  clan(A,-P),
  provera(B).
provera([]).

clan([A|_],A).
clan([_|A],B):-
clan(A,B).

taut((A <=> B) <=> ((A => B) i (B => A))). 
taut((A => B) <=> (ne A ili B)).
taut((ne ne A) <=> A).
taut((ne (A ili B)) <=> (ne A i ne B)).
taut((ne (A i B)) <=> (ne A ili ne B)).

taut(A):-
  write(A),
  nl,
  display(A),
  nl,
  skini_ekv(A,A1),
  skini_imp(A1,A2),
  udubi(A2,A3),
  normiraj(A3,A4),
  asociraj(A4,A5),
  lista_i(A5,A6),
  write(A6),
  !,
  provera(A6).
  
  
start:-write('                **************************'),nl,
       write('                * UTVRDJIVAC TAUTOLOGIJA *'),nl,
       write('                **************************'),nl,nl,
       write('Autori   :  CEROVAC NENAD     i     DOLINAC ZELJKO '),nl,
       write('Br.indexa:     231/87                   253/87 '),nl,
       repeat,nl,
       write('Unesite pravilno formulu iskaznog racuna(sa zagradama).'),nl,
       write('Notacija:  ne  -negacija'),nl,
       write('          <=>  -ekvivalencija'),nl,
       write('           =>  -implikacija'),nl,
       write('           i   -konjunkcija'),nl,
       write('          ili  -disjunkcija'),nl,nl,
       write('Operatore i promenljive(mala slova) odvojite prazninom.'),nl,
       write('Unos zavrsite tackom.'),nl,
       read(A),
       kontrola(A).
	   
kontrola(A):-taut(A),nl,nl,	   
	         write('JESTE TAUTOLOGIJA'),nl,nl,zelja(A),
			 ponovo,read(E),!,E=n.
kontrola(A):-nl,nl,write('NIJE TAUTOLOGIJA'),nl,nl,
             ponovo,read(E),E=n. 			   
	   
ponovo:-write('Hocete li jos da radite?(d./n.)'),nl.
       
/* Poziva se sa: start. */