Negation predicate not/2 for SAT Solver in Prolog

I'm writing a SAT Solver in Prolog. Here's what I've been able to come up so far:

cst(true).
cst(false).

is_true(cst(true)).
is_false(cst(false)).

and(A,B) :- 
    is_true(A),
    is_true(B).

or(A,B) :-
    is_true(A),
    is_false(B).
or(A,B) :-
    is_false(A),
    is_true(B).
or(A,B) :-
    and(A,B).

% not(A) :-

I'm stuck on the not/1. Can anyone give me a clue?

Note that I'm not using Prolog's negation for the interpretation of the logical negation. So I implemented a second predicate is_false(+F) instead, which is true if the formula F is false.

Edit: I meant not/1 in the title, not not/2!

Solution

So your idea was good but there was no possibility to nest your terms. The solution was to use a predicate like the "Interpretation" in formal logic: you drag your is_true or is_false through the whole term:

is_true(cst(true)).
is_true(and(A,B)) :-
    is_true(A),
    is_true(B).
is_true(or(A,B)) :-
    is_true(A),
    is_false(B).
is_true(or(A,B)) :-
    is_false(A),
    is_true(B).
is_true(or(A,B)) :-
    is_true(A),
    is_true(B).
is_true(not(A)) :-
    is_false(A).

is_false(cst(false)).
is_false(and(A,B)) :-
    is_true(A),
    is_false(B).
is_false(and(A,B)) :-
    is_false(A),
    is_true(B).
is_false(and(A,B)) :-
    is_false(A),
    is_false(B).
is_false(or(A,B)):-
    is_false(A),
    is_false(B).   
is_false(not(A)) :-
    is_true(A).
    
?- is_true( or(not(and(cst(true), cst(false))), cst(false)) ).
true.

?- is_true( or(not(and(cst(true), cst(true))), cst(false)) ).
false.    

?- is_false( or(not(and(cst(true), cst(true))), cst(false)) ).
true.

?- is_false( or(not(and(cst(true), cst(false))), cst(false)) ).
false.