Rezolúciós elv, az ítéletlogikában 					2001-12-08

{F1, F2, ..., Fn} =0G     
=0 F1(F2(...( Fn-1(FnG))...)). 

( F1(F2(...( Fn-1(FnG))...)))=
 F1F2... Fn-1FnG 	(=E)		 kielégíthetetlen
azaz
F1,F2,..., Fn-1,Fn,G 			 kielégíthetetlen

Átírva (E)-t
KNFF1KNFF2...KNFFn-1KNFFnKNFG
és így 
KNFF1,KNFF2,...,KNFFn-1,KNFFn, KNFG kielégíthetetlen
A belőle kapott S klózhalmaz kielégíthetelen
(Minden interpretációban hamis legalább egy S –beli klóz.
Az összes interpretáció felsorolása:
a) Az n-változós igazságtábla 2n sorában lévő igazságkiértékelések.
b) Szemantikus fa.
Definíció. Egy n-változós szemantikus fa egy n-szintű bináris fa, ahol a szintek a változóknak vannak megfeleltetve. Egy X változó szintjén a csúcsokból kiinduló élpárokhoz X, X. cimkéket rendelünk. X jelentése X igaz, X jelentése X hamis. Igy egy n- szintű szemantikus fa ágain az összes (2n ) lehetséges igazságkiértékelés (interpretáció) megjelenik.

Szemantikus fa az X, Y, Z logikai változókra. Bázis: X, Y, Z

				X			X
				
			Y	       Y			Y	       Y
					
		Z	  Z 	Z	  Z 	Z	  Z 	Z	  Z
						
		i i i	i i h	i h i	i h h	h i i	h i h	h h i	h h h

S klózhalmaz és a szemantikus fa 
Egy k klóz hamis egy interpretációban, ha minden literálja hamis. 
Egy L literál hamis abban az interpretációban, ahol a szemantikus fában a literálnak megfelelő címke L. 
Egy klóz illesztése a szemantikus fára az olyan ágak kiválasztása amelyeken a klóz minden literálja negálva szerepel. Ezekben az interpretációkban ez a klóz hamis.
Cáfoló csúcsnak nevezzük a szemantikus fa azon csúcsát, amelyiket elérve egy klóz (amely azt megelőzően még nem volt hamis) hamissá válik.
Levezető csúcsnak nevezzük a szemantikus fa azon csúcsát, amelyiket két cáfoló csúcs követ.
A szemantikus fa egy ága zárt, ha cáfoló csúcsban végződik.
A szemantikus fa zárt, ha minden ága zárt.

Tétel: Minden zárt T szemantikus fának van legalább egy levezető csúcsa.
Bizonyítás: Tegyük fel, hogy T zárt, de nincs levezető csúcsa. T szintszáma n. Más szóval T egyetlen szintjén sincs levezető csúcs. Tehát minden szinten van legalább egy csúcs, amelyet követő két csúcs közül legalább az egyik nem cáfoló csúcs. Igy van ez az n-dik szinten is, ami azt jelenti, hogy T-nek van legalább egy nyitott ága ellentétben azzal, hogy egy zárt T-ből indultunk ki.

Példa: 
{XY, XZ, XZ, YZ, Z} khtlen

                        X                        X
                                                                     
        Y            Y                      Y             Y
                           XY                            
Z        Z                              Z      Z          Z       Z
Z,    XZ                Z    XZ   Z     XZ
YZ                           YZ

Zárt szemantikus fa

	{XY, XZ, YZ, Z} khető

                                                           
                        X                        X
                                                                     
        Y            Y                      Y             Y
                             XY                            
Z        Z                              Z      Z          Z       Z
Z,                               Z    XZ   Z     XZ
YZ                         YZ

Nem zárt szemantikus fa 

cáfoló csúcs, levezető csúcs, zárt ág, zárt fa. 

Elnevezések:
n-változós klóz	  n-argumentumos klóz
1-változós klóz	  egységklóz
0-változós klóz	  üres klóz	

Rezolvens fogalma. Legyen C1, C2 két olyan klóz amelyben pontosan egy komplemens pár fordul elő. Tehát C1=L C1’ és C2=L C2’; C1’ és C2’ elemi diszjunkciók. Ekkor létezik rezolvensük C= C1’ C2’ (res(C1, C2)=C).

Tétel: { C1, C2}=0 C
Bizonyítás: Legyen  egy igazságkiértékelés (interpretáció) és 
=0 { C1, C2}. Megmutatjuk, hogy =0 C. 
Két eset lehetséges L=i vagy L =i.

a) L=i. C1=L C1’ és C2=L C2’
              i       i        ?          i       h         i
Mivel C= C1’ C2’, C=i

b) L =i. Ekkor C1’=i és így C=i.

Megjegyzés: A tétel annak belátásával is bizonyítható, hogy C1 C2 C1 C2C logikai törvény.

Az üres klóz kielégíthetetlen, mivel az L, L rezolvense, de ebben az esetben a rezolvens képzés egyszerűsítés, tehát L L.

Definíció. S klózhalmazból való rezolúciós levezetés egy olyan k1, k2, …., kn klózsorozat, ahol kj  S vagy kj rezolvense két őt megelőző ks, kt klóznak s, t<j.
A levezetés célja üres klóz.	(Megállási feltétel  levezetése)
			
S klózhalmazból való rezolúciós levezetés egy döntési eljárás. Eldöntésproblémája : levezethető-e egy S klózhalmazból az üres klóz? 

Egy S klózhalmaznak van rezolúciós cáfolata, ha az S klózhalmazból levezethető az üres klóz.

Példa {AB, AC, AC, BC, C}-ből rezolúciós levezetés:
 C, AC, AC, C, ; 
egy másik rezolúciós levezetés :
C, AC, A, AC, C, 

Tétel: (Helyesség) Ha a S klózhalmazból levezethető az üres klóz, akkor a S klózhalmaz kielégíthetetlen.

Bizonyítás: Létezik az üres klóznak S-ből való levezetése k1, k2, …., kn =.. Tegyük fel, hogy S mégis kielégíthető. Megmutatjuk, hogy az S-ből való rezolúciós levezetés minden klóza következménye S-nek. 
    Vegyül sorra a rezolúciós levezetés klózait. Ha j=1, akkor  kj  S így S=0 kj . Tegyük fel, hogy  j=(m-1)-ig S=0 kj . Tekintsük km –t. Ha  km  S, akkor S=0 km . Ha  km rezolvense két őt megelőző ks, kt klóznak s, t<j, akkor S=0 ks és S=0 kt valamint a rezolvensekre vonatkozó tétel miatt 
{ ks, kt=0 km }ezért S=0 km . Tehát, ha S kielégíthető, akor az üres klóz is kielégíthető, ami ellentmondás.

Tétel: (Teljesség) Ha a S klózhalmaz kielégíthetetlen, akkor a S klózhalmaznak van rezolúciós cáfolata.
Bizonyítás: Az S klózhalmaz kielégíthetetlen, tehát a szemantikus fája zárt. Megmutatjuk, a zárt szemantikus fa segítségével, hogy a fát lezáró S klózhalmazból mindig létezik az üres klózra rezolúciós levezetés. Megadunk egy algoritmust egy ilyen rezolúciós levezetés előállítására.

S és a szemantikus fája adott.
1. k:=0. Sk:=S. nk:= Sk szemantikus fájának szintszáma. LIST=
2. Ha nk =0, akkor levezettük az -t. 
3. Válasszuk ki S k szemantikus fájának egy Q levezető csúcsát. Nevezzük ck,0 , ck,1 –nek a Q-t tartalmazó két ágra illesztett klózt és ck-nak a rezolvensüket. Tegyük a LIST végére ck,0 , ck,1 , ck klózokat.
4. Sk+1:=Sk{ ck }. k:=k+1. Állítsuk elő Sk zárt szemantikus fáját. Folytatás 2.-vel. 

Megjegyzés: Ha S két klózának k rezolvensét hozzávesszük S-hez, akkor Sk szemantikus fájában kevesebb lesz a csúcsok száma, mint S szemantikus fájában volt. Ez biztosítja, hogy a fenti algoritmus véges lépésben befejeződik.

Előrekövetkeztetés és visszakövetkeztetés rezolúciós kalkulussal.

Minden kalkulus a tételbizonyítási feladatot oldja meg. Ez pedig épen a visszakövetkeztetés.
 Nézzük meg a rezolúciós kalkulus esetén az előre- és a vissza következtetés módját és lehetőségét.

{F1, F2, ..., Fn} a feltételhalmaz, G a tételformula.
Visszakövetkeztetés: A feltételhalmazhoz hozzávesszük a tételformula negáltját: 
{F1, F2, ..., Fn}G. Előállítjuk a kapott formulahalmazból az S klózhalmazt. Ha az -nak van rezolúciós levezetése S-ből, akkor {F1, F2, ..., Fn}=0G.

Előrekövetkeztetés: Mivel egy S-ből való rezolúciós levezetés minden klóza szemantikus következménye S-nek ezért ha S a feltételformulákból alkotott klózhalmaz, akkor az S-ből való rezolúciós levezetés minden klóza a {F1, F2, ..., Fn} feltételhalmaz következménye.

Rezolúciós stratégiák. 

Az S klózhalmazból való rezolúciós levezetés definíciója nem tartalmaz semmilyen utalást arra, hogy milyen módon lehet tartalmi vagy formai alapon valamilyen stratégiát kialakítani a rezolúciós levezetés előállítására. Az alábbiakban néhány fontosabb stratégiát ismertetünk.

Def. Levezetési fa. Egy rezolúciós levezetés szerkezetét mutató gráf, ahol a csúcsokban klózok vannak. Két csúcsból akkor vezet él egy csúcsba, ha ott a két klóz rezolvense van. 
Példa. S={AB, AC, AC, BC, C} 

1. rezolúciós levezetés 			levezetési fája
1.	C,					C		AC		AC
2.	 AC,
3.	 AC								C
4.	, C,
5.	 ; 							

2. rezolúciós levezetés 			levezetési fája
1.	C,				C		AC
2.	 AC,
3.	 A,						A		AC
4.	 AC,
5.	 C,							C
6.	 					

Lineáris rezolúció (teljes kalkulus)
Egy S klózhalmazból való lineáris levezetés egy olyan p1, q1, p2, q2, …, qn klózsorozat, amelyben j>1-re qj=res(pj-1, qj-1). A qj klózokat centrális klózoknak, a pj klózokat mellék klózoknak nevezzük.

3. rezolúciós levezetés 			levezetési fája

1. C,		S				C		AC
2. AC,	S
3. A,		res(1,2)
4. AC,	S				A		AC
5. C,		res(3,4)
6. C,		S
7. .		res(5,6) 			C		C

						
					központi		mellék klózok

Lineáris levezetés
Teljes levezetési fa
		C

	BC		AC

	B				A

	AB			AB		AC

	A   +			B		C

	AC			BC		BC	AC  **nem ad újat

	C			C		B

	C			C		AB

						A	folyt. mint +-nál

S={AB, AC, AC, BC, C}

1. C          S				C	          AC	AB		BC
2. AC       S
3. A            res(1,2)				A 			AC
4. AB    S
5. BC S
6. AC  res(4,5)
7. C          res(3,6)						C		AC
8. AC    S
9. A         res(3,6)						A
10.           res(3,6)

Lineáris rezolúciós levezetés egy S klózhalmazból egy olyan q1, p1, q2, p2 ...qn, pn klózsorozat, ahol q1, p1S a qi (i=2, 3,...,n) esetben a pi a pi-1,qi-1 rezolvense, ahol qi-1S, vagy egy korábban megkapott centrális klóz (rezolvense valamely ps, qs (s<i)-nek).
központi klózok  mellék klózok		lineáris reprezentáció
	p1	q1				p1
						   q1
	p2	q2				  
						p2
	p3					   q2
	.
	.					p3
	.					.
	p(i-1)	q(i-1)				.
						.
	pi					p(i-1)
						  q(i-1)
						  
						pi

A lineáris rezolúciós levezetési stratégia jól áttekinthető levezetési szerkezetet eredményez. Amennyiben egy levezetést lineáris gráffal ábrázolunk, a gyökérben lévő p1 klózzal kezdődő összes levezetést egyetlen fával ábrázolhatjuk. Ezzel biztosítjuk, hogy ha van az -nak levezetése p1-ből akkor azt meg is találjuk a levezetések fájának bejárásával.

Példa: Legyen S={AB, AC, AC, BC, C} és induljunk ki AC-ból. 

					AC

		AB		AC	       BC	        C

	BC			C		BA			A

	C			  C		  AC			AC

	     B					BC			C

						  C			C

						B			

Lineáris input rezolúciós levezetés egy S klózhalmazból egy olyan q1, p1, q2, p2 ...qn, pn klózsorozat, ahol q1, p1S a qi (i=2, 3,...,n) esetben vagy  qiS  és a pi pedig a p(i-1),q(i-1) rezolvense.

Egységrezolúciós levezetés egy S klózhalmazból egy olyan q1, q2, ...qn  klózsorozat, ahol qjS, vagy  qs, qt rezolvense, ahol a két ős egyike egységklóz.
A lineáris input rezolúcó és az egységrezolúció ekvivalensek.
Pl. S={BC, AC, AB, AC, C} Horn klózok halmaza
lineáris input levezetés			egységrezolúciós levezetés
1. BC       S				1. BC       S
2. AB     S				2. C               S
3. AC  rez(1,2)				3. B            rez(1,2)
4. AC     S				4. AB   S
5. C  	      rez(3,4)				5. A        rez(3,4)
6.  C       S					6. AC      S
7.         rez(5,6)				7. C         rez(5,6)
						8.             rez(2,7)
Tétel: Ha az  levezethetô lineáris input rezolúcióval egy S klózhalmazból, akkor S-ben van legalább egy egységklóz.
Biz. Az -t mint rezolvenst egy centrális egységklózból és egy klózhalmazbeli klózból kapjuk, Ez utóbbi csak egységklóz lehet.
Definíció: Horn klózok az olyan klózok, amelyekben legfeljebb egy nem negált literál szerepel. Horn formulák a Horn klózokból álló konjunktív normál formák.  Horn logika a Horn formulák halmaza.
Tétel:Kielégíthetetlen Horn klózhalmazban van legalább egy egységklóz.

{AB, AB, AB, AB} nincs lineáris input  cáfolat.
{BC, AC, AB, AC, C} van lineáris input  cáfolat.
A lineáris input-és az egység rezolúció (nem teljes kalkulus)

Elsőrendű logika formuláinak logikailag ekvivalens átalakításai.
Az első a  prenex forma. Jelöle Q a , kvantorok bármelyikét. A Qx1, Qx2,  ..., QxnB formula egy prenex formula. Qx1, Qx2,  ..., Qxn a prefixum és B a formula törzse, matrixa. B  kvantormentes formula.
Minden 1. rendű formula átírható prenex formába.
Ha a prenex formula törzse KNF-ben vagy DNF-ben van, akkor a formula  prenex konjunktív / prenex diszjunktív formula.
A másik speciális (normal) formula egy 1. rendű formula Skolem formája.
A x1, x2,  ..., xnA  formulát , ahol a prefixumban csak univerzális kvantorok vannak Skolem formulának nevezzük.

Minden 1. rendű formula átírható Skolem formába.
Először átírjuk a formulát prenex formába. Azután bevezetjuk a Skolem függvényeket és elimináljuk az egzisztenciális kvantorokat.
Tekintsük az első egzisztenciális kvantort a prefixumban, legyen ez xj. Ha a formula igaz, akkor az x1, x2, ..., xj-1 változók minden értékkombinációjához létezik legalább egy értéke az xj változónak amelyre a formula értéke i. Ezt a tényt az  f(x1, x2, ..., xj-1 ) =xj   függvénnyel fejezzük ki. Ez a függvény rendeli az xj -hez a megfelelő értéket. Ezt a lépést végrehajtjuk  a soronkövetkező egzisztenciális kvantorra addig amíg, minden egzisztenciális kvantort nem elimináltunk.
Pl. xyP(x,y)	Skolem alak: xP(x,f(x))
A prenex formulák kifejtése adott véges univerzumú  U=m  interpretációban.

egzisztenciális formula
(xA) =A(x/u1) A(x/u2)  ... A(x/um),

Skolem formula (univerzális formula)
(xA) =  A(x/u1) A(x/u2)  ... A(x/um) ,
ahol A(x/uj)  alapformula (1jm).

Elsőrendű rezolúciós kalkulus
Definíciók
- Az 1. rendű literál egy atomi  formula vagy egy negált atomi formula: pl. P(x1, x2, ..., xj), P(x1, x2, ..., xj). 
- Alapliterál egy változót nem tartalmazó literál : 
P(a1, a2, ..., aj), P(a1, a2, ..., aj).
- 1. rendű klóz egy olyan univerzálisan kvantált (Skolem) formula, amelynek 1. rendű literálokból álló klóz a törzse. 
Példa; xy(P(x)R(x,y)) egy 1. rendű klóz de ahol ez nem okoz félreértést ott a prefixumot nem írjuk ki: P(x)R(x,y).
-	Alapklóz  alapliterálok diszjunkciója:pl. P(a)R(a,b)

Ha egy xA formula A törzsének alakja KNF, akkor (xA) minden véges U univerzum feletti A(x/u1) A(x/u2)  ... A(x/um) kifejtésében az A(x/uj)  egy-egy alap KNF, vagyis (xA) kifejtése alapklózok konjunkciója. Ha a xA formula kielégíthetetlen az U felett (kielégíthetetlen minden U univerzumú megfelelő típusú struktúrában), akkor ezen alap 
KNF-ák konjunkciója kielégíthetetlen , ami azt jelenti, hogy a kifejtett formulában lévő alapklózok halmaza kielégíthetetlen. Más szóval bármely interpretációban legalább egy alapklóz hamis. Következésképen az üres klóz levezethető ezen alapklózok halmazából 
0-adrendű rezolúciós kalkulussal .

Az {F1, F2, ..., Fn}=G rezolúciós kalkulussal való eldöntéséhez adjunk meg olyan elsőrendű klózhalmazt, amelynek kielégíthetetlensége ekvivalens azzal, hogy 
{F1, F2, ..., Fn}=G
Mint ismert
Ha  {F1, F2, ..., Fn}=G,  akkor 
=F1(F2(...( Fn-1(FnG))...)). Eldöntésprobléma.
A rezolúcióval való megoldáshoz negáljuk az F1(F2(...( Fn-1(FnG))...))  -t.
A kapott  [F1F2... Fn-1FnG] formula kielégíthetetlen.

Megjegyzés. A fenti formulát fel lehet írni elsőrendű klózok konjunkciójaként olyan rezolúciós algoritmust keresünk, ahol a levezetési szabály az elsőrendű klózok rezonveseinek előállítása és amelynek “sikeres” befejeződése ennek az elsőrendű eldöntésproblémának a megoldását jelenti. 

Megkonstruáljuk ez utóbbi formula Skolem alakját, amelyben a mag KNF alakú, és a klózok változóidegenek. Mivel a formula magja klózok konjunkciója az univerzális kvantorra vonatkozó szabály szerint a kvantorokat bevisszük a formulába így a hatáskör egyetlen klóz. Az új formula elsőrendű klózok konjunkciója. Egy klóz prefixumában csak a klózbeli változókra vonatkozó kvantorok hatásosak, tehát a többit nem feltétlenül tartjuk meg.

Az eldöntésprobléma új alakja a Skolem formula logikailag ekvivalens átalakításával kapott formula elsőrendű klózai S halmazának kielégíthetetlensége.

Az eldöntésprobléma megoldásához meg kellene vizsgálni minden számosság mellett  az összes struktúrát.
Ha csak egy adott problémát kell megoldani , ami azt jelenti, hogy a problémát leíró logikai nyelv mellett adott az U univerzum is, akkor a klózhalmaz kielégíthetetlenségét az U univerzum feletti összes struktúrán elegendő megvizsgálni. 
S kielégíthetetlen az U felett, ha tekintve az U univerzum felett az  összes struktúrát a következő állítások ekvivalensek:

- a) ha S h(amis) minden U feletti, a nyelvnek megfelelő típusú struktúrában, 
- b) ha az alapklózok halmaza kielégíthetetlen minden U feletti, a nyelvnek megfelelő típusú struktúrában.

Definíciók.

- Az L nyelv B bázisa U felett a nyelv összes alapatomjainak halmaza, vagyis a predikátumszimbólumokból az U elemeinek behelyettesítésével kapott alapatomok teljesen rendezett halmaza. 

Legyen U={u1, u2, ... } és a Predikátumok : P(x), Q(x,y), akkor
B={P(u1), Q(u1,u1), P(u2), Q(u1,u2), Q(u2, u1), Q(u2, u2), P(u3), ...}	vagy szimbolikusan
B={A1,      A2,           A3,      A4,           A5,             A6,            A7,      ...}
Az U feletti (1,2; ) típusú struktúra (vagy más szóhasználat szerint: egy megfelelő I interpretáció) akkor adott, ha minden alapatom értéke rögzített, vagyis 
I={ m1,      m2,           m3,      m4,           m5,             m6,            m7,      ...}, 
ahol mj=Aj, ha Aj értéke igaz és mj=Aj, ha Aj értéke hamis. Ennek megfelelően egy interpretáció:
I={P(u1), Q(u1,u1), P(u2),  Q(u1,u2),  Q(u2, u1), Q(u2, u2), P(u3), ...}

Szemantikus fa.
Egy bázishoz kötődő olyan bináris fa, amelynek ágain az U feletti összes lehetséges - adott típusú - struktúra megjeleníthető.
 A szemantikus fa egy B bázisra annyi szintet tartalmaz amennyi eleme a bázisnak van. Az Aj báziselemhez rendelt szinten az élpárokhoz az Aj, Aj cimkéket rendeljük. (Aj azt jelenti, hogy Aj igaz, Aj azt jelenti, hogy Aj hamis.) Igy a szemantikus fa egy-egy ágán egy-egy interpretáció jelenik meg.
A szemantikus fa tartalmazza egy U univerzum feletti összes lehetséges - adott típusú - struktúrát.

Példa:
A B bázis szemantikus fája.

				P(u1)			P(u1)
			          				        
		Q(u1,u1)	     Q(u1,u1)	   Q(u1,u1)	      Q(u1,u1)
					
		P(u2)	 P(u2) P(u2)	 P(u2) P(u2)	 P(u2) P(u2)	  P(u2)
						
A 	-val jelölt út jelzi a fenti I interpretációt reprezentáló ágat.

Legyen a klózhalmaz:  S= {P(x),   Q(y,z) P(z),   Q(u,v)}
Legyen a helyettesítés x/u1, y/u1, z/u1, u/u1, v/u1 , Sa={P(u1), Q(u1,u1) P(u1),   Q(u1,u1)}  alapklózhalmazra a szemantikus fa zárt lesz. 
Ha S kielégíthetetlen, akkor bármely interpretációban legalább egy alapklóz hamis. Ez azt jelenti, hogy a szemantikus fa  minden ágára illeszthető alapklóz (minden ág lezárható).

				P(u1)			P(u1)
							 	P(u1)       
		Q(u1,u1)	     Q(u1,u1)	  

	Q(u1,u1) P(u1)	         Q(u1,u1)

Más szóval egy S elsőrendű klózhalmaz kielégíthetetlen egy U univerzum felett akkor és csak akkor S alapklózai halmazának van véges kielégíthetetlen részhalmaza. A 0-adrendű eszözökkel dolgozó alaprezolúciós levezetés az alapklózok rezolvensének értelmezésén alapul. 
Ez a következő, komplemens literálpár egy alapatom és ugyanannak az alapatomnak a negáltja. 

Rezolvens fogalma. Legyen C1, C2 két olyan alapklóz amelyben pontosan egy komplemens pár fordul elő. Tehát C1=L C1’ és C2=L C2’; C1’ és C2’ alapklózok. Ekkor létezik rezolvensük C= C1’ C2’ (res(C1, C2)=C).
Itt is fennáll, hogy { C1, C2}=0 C

Alaprezolúciós levezetés Sa -ból: 
1. Q(u1,u1) P(u1)	Sa
2.  P(u1)			Sa
3. Q(u1,u1)		rez(1,2)
4. Q(u1,u1)			Sa
5. 

A probléma az, hogy így csak egy adott univerzum melletti kielégíthetetlenséget lehet belátni.

Lőwenheim-Skolem tétel kimondja, hogy egy F formula akkor elégíthető ki egyáltalán, ha kielégíthető legfeljebb megszámlálható halmazon.

Herbrand megmutatta, hogy minden elsőrendű klózhalmazhoz létezik legfeljebb megszámlálhatóan végtelen univerzum, a Herbrand univerzum. Egy elsőrendű klózhalmaz kielégíthetetlen  akkor és csak akkor, ha kielégíthetetlen a Herbrand univerzumon. 
Herbrand univerzum konstrukciója lépésről lépésre.

H0 = {a klózhalmazban lévő konstansok halmaza} vagy ha a klózhalmazban nincs konstans, egy szimbolikus konstans {a}
Hi+1 = Hi  Fi={ alaptermek; a klózhalmazban lévő függvényszimbólumokba behelyettesítve Hi elemeit}
H = kN Hk 

Az előző példában :  S= {P(x),   Q(y,z) P(z),   Q(u,v)} H = {a}

Tekintsük a S= {P(x),   Q(y,z) P(z),   Q(u,f(u))} klózhalmazt. 
H0 ={a}  - fiktív konstans
H1= {a, f(a)}
.
Hj= {a, f(a), f(f(a)),....,f...f(a)...)} j.szeres iteráció
.
H ={a, f(a), f(f(a)),....,f...f(a)...), ...}

Herbrand bázis:
{P(a), Q(a,a), P(f(a)), Q(a,f(a)), Q(f(a),a), Q(f(a),f(a)), P(f(f(a))),...}
A helyettesítés: x/a, y/a, u/a , z/f(a)

Az alapklózhalmaz: {P(f(a)), Q(a,f(a)) P(f(a)),   Q(a,f(a))}
Könnyen ellenőrizhető, hogy a bázisra épülő szemantikus fa már a harmadik szinten zárt.

Bizonyítás nélkül felsoroljuk az alapvető Herbrand tételeket.
H. Egy S elsőrendű klózhalmaz kielégíthetetlen akkor és csak akkor, ha S kielégíthetetlen az általa meghatározott Herbrand univerzumon értelmezett minden IH Herbrand interpretációban. Más szóval S kielégíthetetlen akkor és csak akkor, ha nincs Herbrand modellje.

Példa arra, hogy a H1 tétel csak elsőrendű klózhalmaz esetén áll fenn. 
Legyen egy nem elsőrendű klózhalmaz S={P(a), xP(x)}. 
S Herbrand univerzuma: {a}, Herbrand bázisa {P(a)}, Herbrand interpretációk: P(a), P(a). Egyikük sem elégíti ki S-et. Ugyanakkor S kielégíthető például az U={0,1}(P(x)) struktúrában, ahol P(0)=i és P(1)=h.

H1. Egy S elsőrendű klózhalmaz kielégíthetetlen akkor és csak akkor, ha S bármely szemantikus fájához van véges zárt szemantikus fája.

H2. Egy S elsőrendű klózhalmaz kielégíthetetlen akkor és csak akkor, ha S klózai alapelőfordulásainak van véges kielégíthetetlen S’ részhalmaza.

Formalizáció az elsőrendû logikában. Problémamegoldás alaprezolúcióval.

Egy állítás formalizálásához először az állítás környezetét mint formális rendszert tekintjük. Ez a formális rendszer adja a leíró nyelvet. Az ABC: az univerzum elemei, és a rajta definiált relációk  és operációk. Ezzel a nyelvvel leírhatjuk az egyszerû (prim) állításokat majd a logikai összekötők és a kvantorok felhasználásával a további prím és az összetett állításokat. Tehát a feltétel formulákat és a tétel formulát ezen a nyelven formalizáljuk. Mivel a tételbizonyító módszereket formalizált nyelvre dolgoztuk ki, ezért ezek alkalmazhatók bármely konkrét struktúrára úgy, hogy a tételbizonyító eljárást a struktúra nyelvével dolgozik. Ha a probléma egy matematikai struktúrabeli probléma , akkor a struktúra adott. Ha a probléma nem egy matematikai probléma, akkor először meg kell konstruálni egy megfelelő struktúrát.

Példa egy nem matematikai problémára: (Ez a mesterséges intelligencia klasszikus problémája .)
“A majom és a banán”
A helyzet. A majom egy szobában van. A szobában van még egy szék és egy köteg banán. A banán a plafonról lóg le úgy, hogy a majom nem tudja elérni.
A probléma. Meg tudja-e szerezni ilyen körülmények között a majom a banánt?
1. lépés. A környezet matematikai struktúraként való elképzelése.
- Az U univerzum tartalmazza a probléma leírásához szükséges objektumokat.
	 U={m, b, c, f}. (m-majom, b-banán, c-szék, f-padló)
- Az alaprelációk, az egyszerû állítások vagy paraméteres állítások jelölésére:
	R(x,y)       -  x képes elérni y-t
	M(x)	   -  x okos
	Z(x,y)       -  x az y közelében van
	O(x,y)       -  x az y-on van
	A(x,y)       -  x az y alatt van   
	T(x)	   -  x magas
	I(x)	   -  x a szobában van
	V(x,y,z)    -  x képes y-t a  z közelébe vinni
	F(x,y)       -  x képes felmászni y-ra
A :”struktúra”: {m,b,c,f}(R,M,Z,O,A,T,I,V,F;)
		típus:   (2, 1,  2, 2,2, 1,1,3,2;)
A struktúra axiómái.
A1. x1y1 (M(x1)Z(x1,y1)R(x1,y1))
A2. x2y2 (O(x2,y2)A(y2,b)T(y2)Z(x2,b))
A3. x3y3 z3 (I(x3)I(y3)I(z3)V(x3,y3,z3)Z(z3,f)A(y3,z3))
A4. x4y4 (F(x4,y4)O(x4,y4))
A feltételek:
1. M(m)
2. T(c)
3. (I(m)I(b)I(c)
4. V(m,c,b)
5. Z(b,f)
6. F(m,c)
A tétel : R(m,b)
A problémát mint tételbizonyítási feladatot tekintve: F={A1, A2, A3, A4, 1, 2, 3, 4, 5, 6} (a feltételformulák halmaza) és a tételformula R(m,b). A probléma rezolúcióval való megoldásához tehát az F, R(m,b)-ből állítjuk elő az 1. rendû klózhalmazt
Igy az elsőrendû klózhalmaz: 
{x1y1 (M(x1) Z(x1,y1)R(x1,y1)), x2y2 (O(x2,y2) A(y2,b) T(y2)Z(x2,b)), 
 x3y3 z3 (I(x3) I(y3)I(z3) V(x3,y3,z3)Z(z3,f)A(y3,z3)), x4y4 (F(x4,y4)O(x4,y4)),  
 M(m), T(c),  (I(m), I(b), .I(c); V(m,c,b), Z(b,f),  F(m,c), R(m,b)} 

A kapott klózhalmaz:
 S={(M(x1) Z(x1,y1)R(x1,y1)), (O(x2,y2) A(y2,b) T(y2)Z(x2,b)), 
 (I(x3) I(y3)I(z3) V(x3,y3,z3)Z(z3,f)A(y3,z3)), (F(x4,y4)O(x4,y4)),  
 M(m), T(c),  I(m), I(b), .I(c); V(m,c,b), Z(b,f),  F(m,c), , R(m,b)} 

H = {m, b, c, f}.

Konstruáljuk meg a rezolúciós levezetést a következő helyettesítés mellett:

x1/m, y1/b, x2/m, y2/c,.  x3/m, y3/c, z3/b, x4/m, y4/c

Salap={M(m) Z(m,b)R(m,b),		O(m,c) A(c,b) T(c)Z(m,b), 
 I(m) I(c)I(b) V(m,c,b)Z(b,f)A(c,b),		F(m,c)O(m,c),  
 M(m), T(c),  (I(m), I(b), .I(c); V(m,c,b), Z(b,f),  F(m,c), R(m,b)} 
Legyen a bázis: 
{R(m,b), M(m), T(c), Z(b,f), F(m,c), I(m), I(b), .I(c); V(m,c,b), Z(m,b), A(c,b), O(m,c),...

A szemantikus fa könnyen lezárható

0. rendű rezolúciós levezetés az Salap -ból  

1. R(m,b)			2. M(m) Z(m,b)R(m,b)

3. M(m) Z(m,b)		4. M(m)

5. Z(m,b)			6. Q(m,c) A(c,b) T(c)Z(m,b)

7. Q(m,c) A(c,b) T(c)	8. F(m,c)O(m,c)

9. . F(m,c)A(c,b) T(c)	10. F(m,c),

11. A(c,b) T(c)		12. I(m) I(c)I(b) V(m,c,b)Z(b,f)A(c,b)

13. I(m) I(c)I(b) V(m,c,b)Z(b,f) T(c)		14. I(m)

15. I(c)I(b) V(m,c,b)Z(b,f) T(c)		16. I(c)

17. I(b) V(m,c,b)Z(b,f) T(c)		18. I(b)

19. V(m,c,b)Z(b,f) T(c)		20. T(c)

21. V(m,c,b)Z(b,f)			22. Z(b,f)

23. V(m,c,b)				24. V(m,c,b)

25.           

Elsőrendű rezolúciós kalkulus

Legyen    S= {1. xP(f(f(x))),     
2. yz(Q(y,z) P(z)), 
3. uQ(u,f(u))} 

Elsőrendű komplemens literálpár olyan azonos predikátum szimbólummal kezdődő atomi formulapár, amelyek a negáción kívül semmiben sem térnek el egymástól. Az elsőrendű rezolvens fogalma. Két elsőrendű klóznak akkor van rezolvense, ha egyetlen komplemens literálpárt tartalmaznak. Amennyiben egy azonos predikátum szimbólummal kezdődő atomi formulapár argumentumai nem egyformák megvizsgáljuk, hogy van-e olyan helyettesítés, amely egyforma argumentumokat eredményez. Az ilyen helyettesítést illesztő vagy egységesítő helyettesítésnek nevezik.
Tekintsük a K= {P(x),   Q(y,z) P(z),   Q(u,f(u))} klózhalmazt. 

H0 ={a}  - fiktív konstans
H1= {a, f(a)}
.
Hj= {a, f(a), f(f(a)),....,f...f(a)...)} j.szeres iteráció
H ={a, f(a), f(f(a)),....,f...f(a)...), ...}

Herbrand Bázis:
{P(a), Q(a,a), P(f(a)), Q(a,f(a)), Q(f(a),a), Q(f(a),f(a)), P(f(f(a))),...}

Legyen egy helyettesítés:    x/a, 	      y/a, z/f(a) 		u/a ,
A kapott alapklózhalmaz: {P(f(a)), Q(a,f(a)) P(f(a)),   Q(a,f(a))}
Alaprezolúció:
1.	Q(a,f(a)) P(f(a))
2.	Q(a,f(a))
3.	P(f(a))		rez(1,2)
4.	P(f(a))
5.				rez(3,4)

Elsőrendű rezolúció
Alaprezolúció és 1. rendű rezolúció kapcsolata.

xyP(x)Q(x,f(y)), zvP(g(z))P(v), uQ(g(u),u)

H univerzum: a, g(a), f(a), g(f(a)), g(g(a)), f(f(a)), f(g(a)), …
Alapklózok:
x	y	z	v	u	P(x)Q(x,f(y))	P(g(z))P(v)	Q(g(u),u)	
a	a	a	a	a	P(a)Q(a,f(a))	P(g(a))P(a)	Q(g(a),a)	
g(a)	a	a	g(a)	a	P(g(a))Q(g(a),f(a))	P(g(a))P(g(a))	Q(g(a),a)	
g(a)	a	a	g(a)	f(a)	P(g(a))Q(g(a),f(a))	P(g(a))P(g(a))	Q(g(f(a)), f(a))	
g(f(a))	a	f(a)	g(f(a))	f(a)	P(g(f(a)))Q(g(f(a)),f(a))	P(g(f(a)))P(g(f(a)))	Q(g(f(a)), f(a))	

alaprezolúció							1 rendű rezolúció
1. Q(g(f(a)), f(a))			u/f(a)			
2. P(g(f(a)))Q(g(f(a)),f(a))	x/g(f(a)), y/a		
3. P(g(f(a)))						
4. P(g(f(a)))			z/f(a), v/ g(f(a))		
5. 							

Egy másik sikeres alaphelyettesítés
1. Q(g(f(f(a))), f(f(a)))			u/f(f(a))			
2. P(g(f(f(a))))Q(g(f(f(a))),f(f(a)))	x/g(f(f(a))), y/ f(a)	
3. P(g(f(f(a))))							
4. P(g(f(f(a))))				z/f(f(a)), v/ g(f(f(a)))	
5. 								
Sikeres helyettesítéseket kapunk, ha amikor y/h (h a Herbrand univerzum bármely eleme) helyettesítést alkalmazzuk, akkor ezzel együtt az u/f(h), x/g(f(h)), x/g(f(h)), v/ g(f(h)) helyettesítéseket használjuk. h -t helyettesíthetjük egy y változóval, az biztosítja, hogy bármely Herbrand univerzum elem odakerüljön. y-ba behelyettesítve egy h-t alkalmas alaphelyettesítést kapunk.
Illesztő helyettesítésnek nevezzük a lehetséges alkalmas alaphelyettesítéseket magábafoglaló helyettesítéseket. Például
1. Q(g(u),u)		x/g(u), u/f(y)
2. P(x)Q(x,f(y))
3. P(g(f(y)))
4. P(g(z))P(v)	z/f(y), v/g(f(y))
5. 

Például a xP(f(f(x))), yz(Q(y,z) P(z)) alapján a P(f(f(x))) és a (Q(y,z) P(z)) re, nem létezik rezolvens, de az z\f(f(x)) illesztő helyettesítés mellett már igen. A rezolvens Q(y, f(f(x))).
Teljesül-e hogy ha C1, C2 elsőrendű klózok és C a rezolvensük, akkor { C1, C2}= C.
Legyenek a , ,  helyettesítések.  legáltalánosabb helyettesítésnek nevezzük, ha bármely -hoz van olyan  hogy = ( és  kompozíciója)
Definíció: Jelölje W az azonos predikátumszimbólumú atomi formulák halmazát és D a W összeférhetetlenségi halmazát. Az összeférhetetlenségi halmazt azok a részkifejezések alkotják, amelyek a W elemeinek argumentumain egyidőben balról jobbra haladva az első nem egyforma szimbólummal kezdődik.
Pl. W={ P(f(f(x))), P(y)), P(f(z))}, D={ f(f(x)), y, f(z)}

A legáltalánosabb illesztő helyettesítés egy algoritmusa:
1. k:=0, Wk:=W, k=.
2. Ha Wk egyelemű, akkor a legáltalánosabb illesztő helyettesítés k. Stop.
3. Dk megszerkesztése.
4. Ha van Dk –ban olyan vk változó és tk term, hogy a vk változó nem fordul elő tk ban, akkor folytatás az 5. Lépéssel. Egyébként nincs illesztő helyettesítés. Stop.
5. k+1:= k ( vk /tk), Wk+1 :=Wk (vk /tk) = Wk+1
6. k:=k+1. 2. Lépés.

Példa: W={Q(f(a),g(x)), Q(y, y)}
1. k:=0, W0:=W, 0=.
2. W0 nem egyelemű.
3. D0={f(a), y}
4. v0=y, t0=f(a)  
5. A helyettesítés 1=(y/f(a). W1:=W0(y/f(a))= {Q(f(a),g(x)), Q(f(a), f(a))}.
6. k:=1.
2. W1 nem egyelemű.
3. D1={g(x), f(a)}. 
4. Nincs változó D1-ben. Sikertelen.

Az alaprezolúciót véve alapul az alábbi megállapításokat tehetjük:
-	az illesztéssel a két klóz magjának olyan szerkezete alakul ki, amelyekben bármely alaphelyetteítésre az azonos predikátum szimbólummal kezdődő atomi formulapár illesztett argumentuma egyforma.
-	egy olyan klózban ahol több azonos predikátum szimbólummal kezdődő atomi formula szerepel az illeszthető literálok argumentumai megegyeznek arra az alaphelyettesítésre, ahol a behelyettesítendő Herbrand univerzumbeli elem sémája és az illesztő helyettesítés sémája megegyezik. Ezzel a klóz literálszámát arra a minimumra csökkenthetjük, amit alaphelyettesítéssel egyáltalán elérhetünk.
Definíció: Legyen  egy C klóz több azonos predikátum szimbólummal kezdődő, azonosan negált literáljára a legáltalánosabb illesztő helyettesítés. C-t C faktorának nevezzük.
Például legyen a klóz P(f(f(x))) Q(y,z) P(z)) P(g(y))P(f(u))P(f(f(v)))
WP={ P(f(f(x))), P(f(u)), P(f(f(v)))}
1=(u/f(x))
WP(u/f(x))={ P(f(f(x))), P(f(f(v)))}
2=( u/f(x)) (v/x)
WP(u/f(x)) (v/x)={ P(f(f(x)))}

WP={ P(z), P(g(y))}
1=(z/g(y))
WP (z/g(y))={ P(g(y))}
A klóz faktora:
[P(f(f(x))) Q(y,z) P(z)) P(g(y))P(f(u))P(f(f(v)))]( u/f(x)) (v/x)( z/g(y))
P(f(f(x))) Q(y,g(y)) P(g(y)))
Probléma: Az illesztő helyettesítés kötött változókba való helyettesítés. Hogyan lehetséges ez amikor helyettesíteni csak szabad változókba lehet?
Definíció: Legyenek C1, C2 változóidegen elsőrendű klózok. Legyen az L1, L2 literál rendre a C1, C2 eleme. Ha L1= L2-nek  legáltalánosabb illesztő helyettesítése, akkor a C1, C2 klózok (ős vagy szülő klózok) bináris rezolvense a C1- L1 C2- L2 klóz.
L1, L2 azok a literálok, amelyek szerint rezolváltunk.
A C1, C2 szülő klózok elsőrendű rezolvense a következő bináris rezolvensek valamelyike.
-	C1, C2 		bináris rezolvense
-	C1 faktora, C2 	bináris rezolvense 
-	C1, C2 faktora 	bináris rezolvense
-	C1 faktora, C2 faktora bináris rezolvense
Tétel: { C1, C2}= C
Bizonyítás: Legyen  egy interpretáció és = { C1, C2}. Megmutatjuk, hogy = C 
(C= C1- L1 C2- L2 C'1 C'2)
C1, C2 változóidegen klózok. = { C1, C2} azt jelenti, hogy a C1, C2 magjai U felett minden behelyettesítés mellett igazak (azaz a belőlük előálló alapklózok halmazának minden eleme igaz).Ugyanez fennáll a  illesztő helyettesítés elvégzése után is, mivel C'1=L1 C'1, C'1=L2 C'2 alapklózai halmaza részhalmazát képezi C1, C2 alapklózai halmazának. C= C'1 C'2) amelyben a C'1, C'2 alappéldány párjainak legalább egyike az L1, L2 értékétől függően biztosan igaz.

Definíció: S elsőrendű klózhalmaz. S klózhalmazból való 1. rendű rezolúciós levezetés egy olyan k1, k2, …., kn 1. rendű klózsorozat, ahol kj  S vagy kj 1. rendű rezolvense két őt megelőző ks, kt klóznak s, t<j. Legyen j a legkisebb indexű rezolvens klóz. 
Megjegyzés: A levezetésben minden kj –t megelőző klóz következménye S-nek, tehát ks, kt is. Így a rezolvensre vonatkozó tétel miat kj is következménye S-nek.
A levezetés célja üres klóz.

Az 1. rendű rezolúciós kalkulus helyes és teljes eljárás.
Tétel: (Helyesség) Ha a S 1. rendű klózhalmazból levezethető az üres klóz, akkor az S kielégíthetetlen.
Bizonyítás: Létezik az üres klóznak S-ből való levezetése k1, k2, …., kn =.. Tegyük fel, hogy S mégis kielégíthető. Megmutatjuk, hogy az S-ből való rezolúciós levezetés minden klóza következménye S-nek. Vegyül sorra a rezolúciós levezetés klózait. Ha kj  S akkor S= kj ,ha j az első index, hogy kj 1. rendű rezolvense két őt megelőző ks, kt klóznak s, t<j, akkor S= ks és S= kt valamint a rezolvensekre vonatkozó tétel miatt { ks, kt= kj }ezért S= kj . Tehát, ha S kielégíthető, akor az üres klóz is kielégíthető, ami ellentmondás.
Tétel: (Teljesség) Ha a S klózhalmaz kielégíthetetlen, akkor a S klózhalmaznak van elsőrendű rezolúciós cáfolata.
Bizonyítás: Az S klózhalmaz kielégíthetetlen, tehát H1 miatt van végesen zárt szemantikus fája. A zárt szemantikus fa léte, hogy a fát lezáró alap klózhalmazból létezik az üres klózra alaprezolúciós levezetés. Ezután azt kell megmutatni, hogy egy alaprezolúciós cáfolat alapján egyértelműen előállítható az üres klózra egy elsőrendű levezetés S-ből. Ennek biztosítására szolgál a lifting lemma.

Lifting lemma. Ha C1, C2 elsőrendű klózok valmilyen  helyettesítéssel előállított C1, C2 példányainak elsőrendű rezolvense C* , akkor ez valamely példánya a C1, C2 klózok C elsőrendű rezolvensének.

Példa 1. Rendű rezolúciós levezetésre.
Legyen S={P(x)Q(f(x),x), P(g(b))), Q(y,z)}. Kezdjük az 1, rendű rezolúciós levezetést Q(y,z)-vel.
1. Q(y,z) 	S
2. P(x)Q(f(x),x)	S, a legáltalánosabb illesztő helyettesítés (y/f(x)), (z/x).
3. P(x)	bináris rezolvense 1. alapján a Q(y,z) (y/f(x)), (z/x) és 2-nek.
4. P(g(b)))	S, a legáltalánosabb illesztő helyettesítés (x/g(b)).
5.  		bináris rezolvense 3. Alapján a P(x) (x/g(b)) és 4-nek.

A rezolúciós stratégiák elsőrendben is megvalósíthatók. Ezek közül a legfontosabbak.
A lineáris input stratégia a logikai programozásban a PROLOG típusú programozási nyelvek és a DATALOG adatbázis kezelő és lekérdező nyelvek fordítóprogramjainak alapja. Jól használható annak ellenére, hogy nem teljes.
A mesterséges intelligencia alkalmazásokban fontos szerepe van a szemantikus rezolúciós stratégiának (teljes), amely hatékonyan csökkenti a rezolúciós levezetés lépésszámát azáltal, hogy S elemeit két osztályba sorolja aszerint, hogy egy tetszőleges, de rögzített interpretációban a klóz igaz vagy hamis. Rezolválni csak különböző osztályba tartozó két klózt lehet.