Pentru acest exercițiu, veți calcula rezolventul a două clauze.

O clauză se numește trivială atunci când conține atât o variabilă propozițională p, cât și negarea ei non(p). De exemplu, o clauză [a, non(b), non(c), non(a)] este trivială, întrucât conține atât a, cât și non(a).

În acest exercițiu, considerăm că toate clauzele sunt NETRIVIALE (i.e. nicio clauză nu este trivială).

Scrieți un predicat literalForResolution/3 care primește două clauze C1 și C2, și returnează primul literal care poate fi utilizat în rezoluție. În cazul în care nu există un astfel de literal, se va întoarce false.

Un literal se definește ca literal ::= p | non(p), unde p este un atom propozițional (din Var).

Un literal poate fi utilizat în rezoluție dacă apare într-o clauză, iar în cealaltă apare negat, sau vice-versa. De exemplu, dacă p apare în C1, și non(p) apare în C2, atunci p este un literal care poate fi utilizat în rezoluție. La fel, dacă non(p) apare în C1, și p apare în C2, atunci p este un literal care poate fi utilizat în rezoluție.

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

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

?- literalForResolution([d, non(b), non(c)], [x, non(y), z], L).
false

Hint: două clauze recursive pe capul lui C1. Dacă H e atom și non(H) ∈ C2, returnează H. Dacă H = non(P) și P ∈ C2, returnează P. Altfel, recursia pe coadă.