Atomi			P(1, x, ceva)
	Predicat	P
	Argumente -- Termeni
					Constante
					Variabile
					Funcții
Propoziții compuse -- Atomi +
	Conectori logici
	Cuantificatori

Forma normală
	Literal - atom sau atom negat
	Clauză - disjuncție de literali


Inferență -- Premise ~~~-> Concluzie
			Concluzia derivă din premise
			
Metoda de inferență - rezoluția
Regula de inferență - pasul de rezoluție



Principiu

p V  q V !r V !s		- avem !r
t V !u V  r				- avem r
----------------- atunci este adevărat că:
p V Q V !s V t V !u
	- toți literalii originali, mai puțin cei doi literali care au *rezolvat*



!p V q				<=> p => q			dacă q este fals, atunci !p este adevărat
!q V r				<=> q => r			dacă q este adevărat, atunci r este adevărat
------
!p V r

"Clauzele rezolvă dacă avem doi literali (câte unul în fiecare clauză) care rezolvă (unul este în formă negativă și unul în formă pozitivă)."


Metoda rezoluției

premise: p, s, p=>q, q^s=>r
concluzia: r

1. Transformăm în FNC

Listă de clauze (premise + negarea concluziei):
p
s
!p V q
!q V !s V r
!r

Mulțimea de clauze ~   p  ^  s  ^  !p V q  ^  !q V !s V r  ^  !r

2. Căutăm perechi de clauze care rezolvă și realizăm pași de rezoluție
	Folosim metoda reducerii la absurd.
s
!q V !s V r
-----------
!q V r

!q V r
!r
------
!q

p
!p V q
------
q

q				{q}
!q				{!q}
-----
{} -- clauza vidă		-- contradicție (clauza vidă este falsă)
	se notează cu un pătrat.




!om(x) V are_inima(x)
om(Marcel)
------------------ {x <- Marcel} om(x) unifică cu om(Marcel) sub această substituție
are_inima(x)  [x<-Marcel]
are_inimă(Marcel)



În LPOI, doi literali rezolvă dacă atomii lor *unifică*

2 expresii unifică dacă putem găsi o legare (substituție) a variabilelor a.î. după substituție cele 2 expresii să fie identice. Atenție! O variabilă nu trebuie substituită cu o expresie care conține variabila în interior.


1. ∀x.∀y.cal(x) ^ câine(y) => mrapid(x, y)
2. Ex.ogar(x) ^ (∀y.iepure(y) => mrapid(x, y))
3. cal(Harry) ^ iepure(Ralph)
4. !mrapid(Harry, Ralph)

CAL ^ CÂINE => MR
!(CAL ^ CÂINE) V MR
!CAL V !CÂINE V MR

1.  !cal(x) V !câine(y) V mrapid(x, y)
2a. ogar(G)
2b. !iepure(x) V mrapid(G, x)
3a. cal(H)
3b. iepure(R)
4.  !mrapid(H, R)
5.  !ogar(x) V câine(x)
6.  !mrapid(x, y) V !mrapid(y, z) V mrapid(x, z)

3a + 1 ->  
	!cal(x) V !câine(y) V mrapid(x, y)
	cal(H)
	------------------------------------ {x <- H}
7.	!câine(y) V mrapid(H, y)		"Harry este mai rapid decât orice câine"

7 + 5
	!câine(y) V mrapid(H, y)			rezolvă: !câine(y) cu câine(x)
	!ogar(x) V câine(x)
	-------------------------- {y <- x}
8.	!ogar(x) V mrapid(H, x)			"Harry este mai rapid decât orice ogar"

8+2a
	!ogar(x) V mrapid(H, x)
	ogar(G)
	-------------- {x <- G}
9.	mrapid(H, G)

9+6
	!mrapid(x, y) V !mrapid(y, z) V mrapid(x, z)
	mrapid(H, G)
	-----------------------------	{x<-H, y<-G}
10	!mrapid(G, z) V mrapid(H, z)	"Dacă Greg este mai rapid decât cineva, și Harry este mai rapid decât acel cineva"
	
10+2b
	!mrapid(G, z) V mrapid(H, z)
	!iepure(x) V mrapid(G, x)
	--------------------------------- {z <- x}
11	mrapid(H, x) V !iepure(x)		"Harry este mai rapid decât orice iepure"
	
11+4
	mrapid(H, x) V !iepure(x)
	!mrapid(H, R)
	-------------------- {x <- R}
12	!iepure(R)

12 + 3b
	iepure(R)
	!iepure(R)
	-------------
	clauza vidă