is_form(Gamma, var(A)) :-
    member(A, Gamma).

is_form(Gamma, neg(F)) :-
    is_form(Gamma, F).

is_form(Gamma, disj(F, G)) :-
    is_form(Gamma, F),
    is_form(Gamma, G).

is_form(Gamma, conj(F, G)) :-
    is_form(Gamma, F),
    is_form(Gamma, G).

is_form(Gamma, imp(F, G)) :-
    is_form(Gamma, F),
    is_form(Gamma, G).

syn(var(A), A) :- atom(A).
syn(neg(F), ~(F)).
syn(conj(F,G), F*G).
syn(disj(F,G), F+G).
syn(imp(F,G), F=>G).

simplify(var(A), var(A)).
simplify(neg(F), neg(F1)) :-
    simplify(F, F1).
simplify(conj(F, G), conj(F1, G1)) :-
    simplify(F, F1),
    simplify(G, G1).
simplify(disj(F, G), neg(conj(neg(F1), neg(G1)))) :-
    simplify(F, F1),
    simplify(G, G1).
simplify(imp(F, G), neg(conj(F1, neg(G1)))) :-
    simplify(F, F1),
    simplify(G, G1).

eval(Phi, var(A), B) :-
    member(assign(A, B), Phi).
eval(Phi, neg(F), B1) :-
    eval(Phi, F, B),
    B1 is 1 - B.
eval(Phi, conj(F, G), B) :-
    eval(Phi, F, BF),
    eval(Phi, G, BG),
    B is BF * BG.
eval(Phi, disj(F, G), B) :-
    eval(Phi, F, BF),
    eval(Phi, G, BG),
    B is BF + BG - BF * BG.
eval(Phi, imp(F, G), B) :-
    eval(Phi, F, BF),
    eval(Phi, G, BG),
    B is (1-BF) + BG - (1- BF) * BG.