Just a little note. There is an interesting relationship from
s(CAPS) to QSAT. If we split the propositonal variables V into
two camps, V1 the abducible ones, and V2 the normal ones,
we can do deduction and abduction in one go.
/* SWI-Prolog */
?- use_module(library(clpb)).
?- sat(V1 ~(V2^ ~(P =< Q))).
But there are even more tricks in stock with a QSAT
solver, especially from within Prolog. Works also for
Jekejeke Prolog not only SWI-Prolog. Namely listing models.
We can list models when we ommit V1, here
the s(CAPS) r and not r example:
/* Two Models */
?- sat(~(R^ ~((P+Q)*(R>=P*Q)=<R))), labeling([P,Q]).
P = 0, Q = 0;
P = 1, Q = 1.
/* One Model */
?- sat(~(R^ ~((P+Q)*(R>=P*Q)=< ~R))), labeling([P,Q]).
P = 0, Q = 0.
The later makes us think about completion. What if
a Prolog r <- p & q effectively means r <-> p & q. This is
called closed world assumption. We can also tinker with
closed world assumption by replacing (>=)/2 by (=:=)/2:
/* Two Models */
?- sat(~(R^ ~((P+Q)*(R=:=P*Q)=<R))), labeling([P,Q]).
P = 0, Q = 0;
P = 1, Q = 1.
/* Three Models */
?- sat(~(R^ ~((P+Q)*(R=:=P*Q)=< ~R))), labeling([P,Q]).
P = 0, Q = 0;
P = 0, Q = 1;
P = 1, Q = 0.
In the above we listed all models, not only those where p v q
holds, but the QSAT query could be arranged to filter accordingly.
Cool!