% Boolean algebra 

% boolean variables have two values: 1(true) and 0(false)

bool(X):-X=0;X=1.
bools([]).
bools([X|Y]):-bool(X), bools(Y).

% How to evaluate a boolean formula
eval(0, 0):-!.
eval(1, 1):-!.
eval(-1, 0):-!.
eval(-0, 1):-!.
eval(-X, V):-eval(X,XV), V is 1-XV, !.
eval(X+Y,V):-eval(X,XV), eval(Y,YV), V is XV+YV-XV*YV,!.
eval(X*Y,V):-eval(X,XV), eval(Y,YV), V is XV*YV,!.

eval(X-Y, V):-eval(X+(-Y),V),!.

eval(X=Y, V):-eval(X*Y+(-X)*(-Y),V),!. 
eval(X->Y, V):-eval(Y-X,V). 


test(E):-eval(E,1).

disprove([Var1|Rest], Proposition):-bools([Var1|Rest]), eval(Proposition,0).