Implementation of the calculus of models and certificates for QBF in Sicstus Prolog
An example
| ?- models(binder([a,e,a,e],[_a,_b,_c,_d]),[[~_a, ~_b, ~_c, _d],[~_a, ~_b,_c,~_d],[~_a, _b,_c, ~_d],[~_a, _b,_c, _d],[_a, ~_b,~_c, _d],[_a, ~_b,_c,_d],[_a, _b,_c, ~_d],[_a, _b,_c, _d]], Model).
Model = [(_a->(_b;[(_c->(_d;[])),(~_c->(~_d;[]))])),(~_a->(_b;[(_c->(_d;[])),(~_c->(_d;[]))]))] ? ;
no
An example
| ?- certificate(binder([a,e,a,e],[_a,_b,_c,_d]),[[~_a, ~_b, ~_c, _d],[~_a,~_b,_c,~_d],[~_a, _b,_c, ~_d],[~_a, _b,_c, _d],[_a, ~_b,~_c, _d],[_a,~_b,_c,_d],[_a, _b,_c, ~_d],[_a, _b,_c, _d]], Certificate).
Certificate = [(~_a*_a,1),((~_a+(~_b+ ~_c))*((~_a+(_b+_c))*((_a+(~_b+ ~_c))*((_a+(~_b+_c))*(_a+(_b+_c))))),(~_a+(~_b+_c))*((~_a+(_b+_c))*(_a+(_b+_c))))] ? ;
no