Calculul propozițional în Prolog

Reprezentare

Variabilele propoziționale sunt atomi Prolog (atom(X) e true). Operatorii logici sunt reprezentați prin termeni compuși:

| Operator logic | Reprezentare Prolog | |---|---| | ¬ | non/1 | | ∧ | and/2 | | ∨ | or/2 | | → | imp/2 |

Formula p → (q ∨ r):

?- X = imp(p, or(q, r)).

Extragerea variabilelor

vars(X, [X]) :- atom(X).
vars(non(P), Res) :- vars(P, Res).
vars(imp(P, Q), Res) :- vars(P, ResP), vars(Q, ResQ), union(ResP, ResQ, Res).
vars(and(P, Q), Res) :- vars(P, ResP), vars(Q, ResQ), union(ResP, ResQ, Res).
vars(or(P, Q),  Res) :- vars(P, ResP), vars(Q, ResQ), union(ResP, ResQ, Res).

?- vars(imp(non(a), imp(a, b)), S).
S = [a, b]

Evaluări

Reprezentăm o valuare e : Var → {0, 1} ca listă de perechi [(a, 1), (b, 0)].

val(X, [(X, E) | _], E) :- !.
val(X, [_ | T], E) :- val(X, T, E).

?- val(b, [(a, 1), (b, 0)], X).
X = 0

Operații booleene pe {0, 1}

bnon(0, 1) :- !.
bnon(1, 0) :- !.
bor(1, _, 1) :- !.
bor(_, 1, 1) :- !.
bor(0, 0, 0) :- !.
bimp(P, Q, Res) :- bnon(P, NonP), bor(NonP, Q, Res).
band(P, Q, Res) :-
    bnon(P, NonP), bnon(Q, NonQ),
    bor(NonP, NonQ, NonRes),
    bnon(NonRes, Res).

Evaluare recursivă a formulei

eval(X, List, Res) :- val(X, List, Res).
eval(non(P), List, Res) :- eval(P, List, ResP), bnon(ResP, Res).
eval(imp(P, Q), List, Res) :- eval(P, List, RP), eval(Q, List, RQ), bimp(RP, RQ, Res).
eval(and(P, Q), List, Res) :- eval(P, List, RP), eval(Q, List, RQ), band(RP, RQ, Res).
eval(or(P, Q),  List, Res) :- eval(P, List, RP), eval(Q, List, RQ), bor(RP, RQ, Res).

Tautologie

O formulă e tautologie dacă se evaluează la 1 pe toate valuările posibile.

taut(Form) :-
    all_evals(Form, Evals),
    all_eq_1(Evals).

Rezoluție (Subiectul III din parțial)

O clauză este o mulțime de literali. Un literal este o variabilă propozițională (p) sau negarea ei (non(p)).

O clauză se numește trivială dacă conține atât un literal p cât și negarea lui non(p). În problemele de parțial, presupunem că toate clauzele sunt netriviale.

Regula rezoluției — dacă C1 conține p și C2 conține non(p) (sau invers), atunci:

rezolvent(C1, C2) = (C1 \ {p}) ∪ (C2 \ {non(p)})

Exemplu:

C1 = [a, non(b), c]
C2 = [d, c, b, a]
       ^ literal pentru rezoluție: b apare în C2, non(b) apare în C1

rezolvent = [a, c] ∪ [d, c, a] = [a, c, d]    (ca multime)

?- rezolvent([a, non(b), c], [d, c, b, a], R).
R = [d, c, a].

?- rezolvent([b], [non(b)], R).
R = [].

?- rezolvent([p, q, r], [p, q, s], R).
false.     % — niciun literal nu poate fi folosit pentru rezoluție

Selecția literalului pentru rezoluție — primul literal care apare într-o clauză și negat în cealaltă:

?- literalForResolution([a, non(b), non(c)], [b, non(a)], L).
L = a

TODO — secțiunea de rezoluție mai are nevoie de notițele tale de seminar (definiția formală a rezolvenției și exemplele profesorului). Partea de mai sus e construită din partial_prolog.pl. Dacă ai notițe de la seminar, trimite-mi-le și completez cu vocea profesorului.

Ștergere element dintr-o listă (select/3)

Util pentru calculul rezolvenței:

?- select(a, [b, a, c], R).
R = [b, c].

?- select(a, [b, c], R).
false.

Pentru a evita duplicatele în rezolvent, combinăm cu sort/2 sau union/3.