p=>q  ~~>  !p V q

Vx.Ey.p(x) ^ q(y) => r(x, y)

Vx.Ey.  (p(x) ^ q(y)) => r(x, y)
Vx.Ey.  !(p(x) ^ q(y)) V r(x, y)
Vx.Ey.  (  !p(x) V !q(y)  ) V r(x, y)
Vx.  (  !p(x) V !q(f(x))  ) V r(x, f(x))

operatorii Și și Sau sunt asociativi

(a V b) V c  același lucru cu  a V (b V c)  este același lucru cu a V b V c

Vx.  !p(x) V !q(f(x)) V r(x, f(x))

{!p(x), !q(f(x), r(x, f(x))}


Dacă cerința cere rezolvare prin rezoluție, rezolvați prin rezoluție.


@<, @> -- sortare în funcție de ordinea "naturală"


forall/2
forall(:Pred, :Cond)
	- găsesște toate soluțiile pentru Pred
	- evaluează Cond pentru toate soluțiile lui Pred 
	- întoarce conjuncția acestor evaluări
	* forall nu leagă nimic în exterior

findall/3
findall(+Template, :Goal, -Bag)
	- avem variabilele Xi care nu sunt apriori legate, care apar în Template și care apar în Goal.
	- găsește toate soluțiile pentru Goal
	- formează forma Template cu variabilele Xi
	- pentru fiecare soluție pentru Goal, pune forma Template în lista Bag
	

bagof/3
bagof(+Template, :Goal, -Bag)
	- avem variabilele Xi care nu sunt apriori legate, care *apar în Template* și care apar în Goal.
	- avem variabilele Yi care nu sunt apriori legate, care apar în Goal, *fără* să apară în Template
	- pentru fiecare legare diferită pentru Yi, găsește toate soluțiile pentru Goal și strânge soluțiile (în forma din Template), în Bag
	
	- pentru a nu separa după anumite variabile Yi, adaug variabilele după care NU vreau să separ în fața lui Goal, cu operatorul "existențial" ^

	- findall este echivalent cu bagof, cu toate variabilele Yi adăugate cu operatorul existențial ^ în fața lui Goal



setof/3
setof(+Template, :Goal, -Bag)
	- la fel ca bagof
	- elimină duplicatele din Bag și sortează Bag conform ordinii naturale




Cheryl

--	May				15	16			19	--
--	June					17	18		--
	July		14		16
	August		14	15		17
				--

Albert știe luna
Bernard știe data

Albert: nu știu
Albert: nici Bernard nu știe
	nu este mai sau iunie
Bernard: acum știu
	nu este 14
	rămân 16 iulie, 15 și 17 august
Albert: acum știu și eu
	este 16 iulie