proposition(p)
proposition(q)
proposition(r)

negation(not(X)) :- sentence(X)
conjunction(and(X,Y)) :- sentence(X) & sentence(Y)
disjunction(or(X,Y)) :- sentence(X) & sentence(Y)

sentence(X) :- proposition(X)
sentence(X) :- negation(X)
sentence(X) :- conjunction(X)
sentence(X) :- disjunction(X)

boolean(0)
boolean(1)

assignment(a(P,Q,R)) :- boolean(P) & boolean(Q) & boolean(R)

satisfies(p,a(1,Q,R)) :- boolean(Q) & boolean(R)
satisfies(q,a(P,1,R)) :- boolean(Q) & boolean(R)
satisfies(r,a(P,Q,1)) :- boolean(Q) & boolean(R)
satisfies(not(S),A) :- sentence(S) & assignment(A) & ~satisfies(S,A)
satisfies(and(S,T),A) :- satisfies(S,A) & satisfies(T,A)
satisfies(or(S,T),A) :- satisfies(S,A)
satisfies(or(S,T),A) :- satisfies(T,A)

satisfiable(S) :- satisfies(S,A)