Calculation logic formula models with prolog

Question

Given a CNF logic formula [[a, b, c], [b, d], [not(d), a]] that is equal to ((a or b or c) and (b or d) and (not d or a)), how do I calculate its models (possible values for its atoms that makes the formula true), using prolog? This is what i've got so far:

A valuation to the formula is a list of terms in the form os val(X,B), where X is an atom, and B is its value (0 or 1).

The relation value(X, Vs, B) is given by

value(X, [val(X, B)|_], B) :− !.
value(X, [_|Ps], B) :− value(X, Ps, B).

and its true whenever B is the value for the atom X in the valuation Vs.

The relation sp(F, Ss), given by

sp([],[]).
sp([F|Fs], Ss) :- setof(A, member(A,F), R), sp(Fs, N), append(R,N,M), setof(B,member(B,M),Ss).

and its true whenever Ss is the list of atoms in logic formula F.

The relation valuation(As, Vs), given by

valuation([],[]).
valuation([A|As], [V|Vs]) :- (V = val(A,0); V = val(A,1)), valuation(As,Vs).

that is true whenever Vs is a possible valuation for the list of atoms As.

---

What I need:

The relation ext(F, Vs, B) that is true whenever F is a formula, Vs is a possible valuation for that formula, and B is the value of the formula applying Vs valuation. For example, the consult

ext([[a], [not(b), c]] , [val(a, 1), val(b, 0), val(c , 1)], B).

should return the value B = 1.

The relation model(F,Vs) that is true whenever the valuation Vs is a model for the formula F.

The relation models(F, Ms) that is true whenever Ms is a list which elements are models for the formula F. I guess we need to use prolog’s setof here.

And, at last, I don't know whats the best implementation of val(X,B) to make it work. I dont know if I should specify val(_,1) and val(_,0) to be true or only val(_,1), what is better knowing the other relations to be implemented?

Answer 1

Not sure to understand exactly what you want but...

First of all, let me try to simplify your code.

1) I think your value/2 should be written as

value(X, [val(X, B) | _], B).

value(X, [_ | Ps], B) :-
   value(X, Ps, B).

2) I don't understand the purpose of your sp/2 but seems to me that can be simplified as

sp([], []).

sp([[A] | Fs], [A | Ss]) :-
  sp(Fs, Ss).

sp([[A | As] | Fs], [A | Ss]) :- 
  append(As, Fs, N),
  sp(N, Ss).

3) I don't understand the purpose of your valutation/2 but seems to me that can be simplified as

isBool(0).

isBool(1).

valuation([], []).

valuation([A | As], [val(A, B) | Vs]) :-
  isBool(B),
  valuation(As,Vs).

Now I try to respond to your question

4)

I need [...] The relation ext(F, Vs, B) that is true whenever F is a formula, Vs is a possible valuation for that formula, and B is the value of the formula applying Vs valuation

I suppose the following should work [caution: not tested really much]

ext([], _, 1).

ext([[] |_], _, 0).

ext([[X | L1] | L2], Vs, B) :-
  value(X, Vs, 0),
  ext([L1 | L2], Vs, B).

ext([[not(X) | L1] | L2], Vs, B) :-
  value(X, Vs, 1),
  ext([L1 | L2], Vs, B).

ext([[X | _] | L], Vs, B) :-
  value(X, Vs, 1),
  ext(L, Vs, B).

ext([[not(X) | _] | L], Vs, B) :-
  value(X, Vs, 0),
  ext(L, Vs, B).

5)

I need [...] The relation model(F,Vs) that is true whenever the valuation Vs is a model for the formula F

What about the following ?

model(F, Vs) :-
  ext(F, Vs, _).  % or ext(F, Vs, 1)?

6)

I need [...] The relation models(F, Ms) that is true whenever Ms is a list which elements are models for the formula F

If I understand correctly what do you want, given model/2, models/2 could be written as

models(_, []).

models(F, [Vs | Vl]) :-
  model(F, Vs),
  models(F, Vl).

7)

I don't know whats the best implementation of val(X,B) to make it work. I dont know if I should specify val(,1) and val(,0) to be true or only val(_,1)

Not sure to understand your question.

val/2 can't be true for every value; so you can't impose true val(_,1) and/or val(_,0) because given an atom (a, by example) is true val(a,1) or val(a,0) but ins't true val(X,1) for every X.

Answer 2

Another approach here. Translate to executable Prolog, and reify a specific execution (i.e. a proof with specific symbol bindings):

ext(F, Vs, B) :-
    or_list(F, [], C, Vs), !,
    assign(Vs), ( call(C), B = true ; B = false ).

assign(Dict) :- maplist(domain, Dict).

domain(val(_, true)).
domain(val(_, false)).

or_list([A], D, T, Du) :-
    !, and_list(A, D, T, Du).
or_list([A|As], D, ( T ; Ts ), Du) :-
    and_list(A, D, T, Dut),
    or_list(As, Dut, Ts, Du).

and_list([V], D, T, Du) :-
    !, negation(V, D, T, Du).
and_list([V|Vs], D, ( T , Ts ), Du) :-
    negation(V, D, T, Dut),
    and_list(Vs, Dut, Ts, Du).

negation(not(V), D, \+T, Du) :-
    !, sym_bind(V, D, T, Du).
negation(V, D, T, Du) :-
    sym_bind(V, D, T, Du).

sym_bind(V, D, T, D) :-
    memberchk(val(V, T), D), !.
sym_bind(V, D, T, [val(V, T)|D]).

note:

• false/true instead of 0/1
• list to structure translation: could be way shorter, using foldl or DCGs or passing down the operators (that is (;)/2 (,)/2 (+)/1), but this way the Prolog patterns should be clearer...

Answer 3

I could finally finish it while waiting for replies, and improved it using max66's answer.

I made it to accept propositional logic forms too, so models/2 accepts both styles (CNF and Propositional form, based on operators and, not, or, imp, iff that I set).

:- op(400, fy , not).
:- op(500, xfy, and).
:- op(600, xfy, or ).
:- op(700, xfy, imp).
:- op(800, xfy, iff ).

distr(_, [], []).
distr([], _, []).
distr([C|Cs], Ds, Es) :- distr_un(C, Ds, Ss), distr(Cs, Ds, Ts), append(Ss, Ts, Es).
distr_un(_, [], []).
distr_un(C, [D|Ds], [E|Es]) :- append(C, D, E), distr_un(C, Ds, Es).

cnf(F, [[F]]) :- atom(F), !.
cnf(not(F), [[not(F )]]) :- atom(F), !.
cnf(not not F, Rs) :- cnf(F, Rs).
cnf(not (F imp G), Rs) :- cnf(F and not G, Rs).
cnf(not (F iff G), Rs) :- cnf((F and not G) or (not F and G), Rs).
cnf(not(F and G), Rs) :- cnf((not F) or (not G), Rs).
cnf(not(F or G), Rs) :- cnf((not F) and (not G), Rs).
cnf(F and G, Rs) :- cnf(F, Cs), cnf(G, Ds), append(Cs, Ds, Rs).
cnf(F or G, Rs) :- cnf(F, Cs), cnf(G, Ds), distr(Cs, Ds, Rs).
cnf(F imp G, Rs) :- cnf((not F) or G, Rs).
cnf(F iff G, Rs) :- cnf((not F or G) and (not G or F), Rs).

val(X,0) :- atom(X).
val(X,1) :- atom(X).
value(X, [val(X, B)|_], B) :- !.
value(X, [_|Ps], B) :- value(X, Ps, B), !.
value(not X, [val(X, B)|_], V) :- V is 1-B, !.
value(not X, [_|Ps], B) :- value(not X, Ps, B), !.
sp([],[]).
sp([F|Fs], Ss) :- setof(A1, member(not A1, F), R1), setof(A, (member(A,F), atom(A)), R),  sp(Fs, N), append(R,N,M1), append(M1, R1, M), setof(B,member(B,M),Ss), !.
sp([F|Fs], Ss) :- setof(A, (member(A,F), atom(A)), R),  sp(Fs, N), append(R,N,M), setof(B,member(B,M),Ss), !.
sp([F|Fs], Ss) :- setof(A, (member(not A,F), atom(A)), R),  sp(Fs, N), append(R,N,M), setof(B,member(B,M),Ss), !.
valuation([],[]).
valuation([A|As], [V|Vs]) :- (V = val(A,0); V = val(A,1)), valuation(As,Vs).
ext([F|Fs], Vs, B) :- sp([F|Fs], Ss), valuation(Ss, Vs), ext_([F|Fs], Vs, B).
ext_([], _, 1).
ext_([F|Fs], Vs, 1) :- cl(F, Vs, 1), ext_(Fs, Vs, 1).
ext_([F|Fs], Vs, 0) :- cl(F, Vs, 0); ext_(Fs, Vs, 0).
cl([A|As], Vs, 1) :- value(A,Vs,1); cl(As, Vs, 1).
cl([A|As], Vs, 0) :- value(A,Vs,0), cl(As,Vs,0).
cl([], _, 0).
model(F, Vs) :- ext(F, Vs, 1).
models(F, Vs) :- cnf(F, Fs), setof(V, model(Fs, V), Vs).
models(F, Vs) :- setof(V, model(F, V), Vs).

I tested it and it seems to be working as intended.