Solving Boolean expressions with Prolog

gistfile1.prolog

% Solving Boolean expressions with Prolog

% Parsing
% prop([-,+,a,*,b,c],T). gives: T = not(or(var(a), and(var(b), var(c))))
prop([A|R], var(A), R):- char_type(A, lower).
prop([-|A], not(C), R):- prop(A, C, R).
prop([+|A], or(C,D), R2):- prop(A, C, R1), prop(R1, D, R2).
prop([*|A], and(C,D), R2):- prop(A, C, R1), prop(R1, D, R2).
prop(T,A):- prop(T,A,[]).

% Evaluating
evl(var(A), Env):- member(A:1, Env).
evl(not(A), Env):- \+ evl(A, Env).
evl(or(C,D), Env):- evl(C, Env); evl(D, Env).
evl(and(C,D), Env):- evl(C, Env), evl(D, Env).

ev(P, Env, R):- !, R = true, prop(P, AST), evl(AST, Env); prop(P, _), R = false.

% Satisfiability and tautology
varlist('var'(A), [A]).
varlist('not'(A), E):- varlist(A,E).
varlist('or'(A,B), E):- varlist(A,C), varlist(B,D), union(C,D,E).
varlist('and'(A,B), E):- varlist(A,C), varlist(B,D), union(C,D,E).

assignment([],[], _).
assignment([H|T1],[H:B|T2], V):- member(B, V), assignment(T1,T2,V).

sat(P):- prop(P,T), varlist(T,Vars), !, assignment(Vars, Env, [0,1]), evl(T, Env).
taut(P):- prop(P,_), \+ sat([-|P]).