VAN UJABB
Logikai programozás.
Előadásvázlat. 2002, tavaszi félév.	Pásztorné Varga Katalin.

Az irodalomból:
K.R. Apt., Logic Programming. 
Handbook of theoretical Computer Science, Springer, 1990.
J.W. Lloyd., Logic Programming. 
Springer, Second, Extended Ed. 1987
R.A. Kowalski., Logic for Problem Solving. 
North Holland, 1979..
I. Bratko: PROLOG Programming For Artificial Intelligence. 
Addison Wesley.
S.H. Nienhuys-Cheng R. de Wolf: Foundations of Inductive Logic Programming. (LNAI 1228) Spinger, 1997

A szemantikus eldöntésprobléma arról dönt, hogy egy formula vagy egy formulahalmaz, függetlenül annak szerkezetétől, rendelkezik-e valamilyen meghatározott szemantikai tulajdonsággal.
{F1, F2, ..., Fn}=0 G 
=0 F1(F2(...( Fn-1(FnG))...)). 
tautológia
 {F1, F2, ..., Fn}= G  
= F1(F2(...( Fn-1(FnG))...)). 
logikailag igaz.

Az eldöntésprobléma különböző alakú ekvivalensei 
0 és 1 rendben 
[ F1(F2(...( Fn-1(FnG))...)).] vagy 
{F1, F2, ..., Fn, G} 		kielégíthetetlen 
ezzel ekvivalens
Itéletlogikában, hogy az 
{F1, F2, ..., Fn, G} KNF-jeiben szereplő klózok 
S halmaza kielégíthetetlen
1 rendű logikában az {F1, F2, ..., Fn, G} Skolem formuláiból alkotott elsőrendű klózok S halmaza kielégíthetetlen
Háttér:
a)  tetszőleges 1 rendű formula átalakítható prenex alakúvá: 		Q1x1,...,QnxnC,  
			ahol Qj az  vagy az  kvantor,.
			C kvantormentes formula 
b) tetszőleges prenex formula átalakítható Skolem formulává:		y1,...,ynCS
			CS a C-ből a Skolem függvények 
			behelyettesítésével áll elő.
Írjuk át CS-t konjunktív normálformába (CSKNF).
A y1,...,ynCSKNF =y1,...,yn(k1...kr)-re alkalmazva az -re vonatkozó kvantorkiemelési szabályt a

x1,...,xnk1...x1,...,xnkr	 formulát kapjuk. Ennek kielégíthetetlensége ekvivalens az 
S={ x1,...,xnk1,...,x1,...,xnkr } 1 rendű klózhalmaz kielégíthetetlenségével. 
Ez a szemantikus eldöntésprobléma egy másik megfogalmazása elsőrendben.
Emlékeztetőül a kvantorszabályok.
Általános DeMorgan szabályok 
xA=xA	xA=xA
A kvantorkiemelési szabályok
1. xA[x]B=x(A[x]B) 
    xA[x]B=x(A[x]B) 
2. xA[x]B= x(A[x]B) 
    xA[x]B= x(A[x] B) 
3. xA[x]xB[x]= x(A[x] B[x]) , 
					de   -ra nem
4. xA[x] xB[x] = x(A[x] B[x]), 
					de   -re nem. 
5. Q1xA[x] Q2xB[x]=Q1xQ2z(A[x]B[x/z]) 
6. Q1xA[x ] Q2xB[x]= Q1xQ2z(A[x ] B[x/z]). 

 Q1 és Q2 tetszőleges kvantorok

f(x1,...,xt) Skolem függvény, ahol x1,...,xt a prefixumban az első -ral kvantált v változót megelőző -ral kantált változók.

Tételbizonyító kalkulusok
Szintaktikus eszközökkel keresik a szemantikus eldöntésprobléma megoldását. 

A főbb tételbizonyító eljárások.

Bizonyításelmélet.
Természetes levezetés.
Gentzen szekvent kalkulus.
Smullyan tábla (tabló) módszer.
Rezolúciós elv (kalkulus)

A rezolúciós elv eldöntésproblémája - S- klózhalmazból levezethető-e az üres klóz 
Helyesség és teljesség - az üres klóz levezetése ekvivalens S kielégíthetetlenségével.
0 rendű rezolúciós elv. Adott S klózhalmaz, 
	Levezetési szabály a rezolvensképzés.
A pontosan egy komlemens párt tartalmazó K1=LK1’, K2=LK2’ klózoknak van rezolvense a 
K=K1’ K2’ vagy K= rez(K1,K2).
A rezolvens tulajdonsága: {K1,K2} =0 K

Def. S klózhalmazból való rezolúciós levezetés egy olyan c1, c2, ...cj,...klózsorozat, ahol
cjS vagy cj=rez(cs,ct) és s,t<j.
A levezetés célja az üres klóz levezetése.

K klózhalmazból való rezolúciós levezetés mint döntési eljárás. 

Eldöntésproblémája : levezethető-e egy K klózhalmazból az üres klóz? 

Példa
S = {AB, AC, AC, BC, C}
Rezolúciós levezetés (2): 				Levezetési fa
1. C, 	S
2. AC, 	S				C		AC		AC
3. AC, 	S 
4. A		rez(1, 2) 				A		A
5. A		rez(1, 3)
6. . 		rez(4, 5) 					

Rezolúciós levezetés (1):				Levezetési fa	

							      C		AC		lineáris
1. C, 	S										input
2. AC, 	S										stratégia
3. A,  		rez(1, 2)					A		AC
4. AC, 	S 				
5. C, 		rez(3, 4)			
6. . 		rez(1, 5) 					

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 
(i=2, 3,...,n) esetben pi a pi-1,qi-1 rezolvense
qi vagy  qiS vagy (s<i)-re a ps, qs- nek rezolvense (azaz egy korábban megkapott centrális klóz).

A kétféle levzetési fa egy lineáris rezolúciós levezetés ábrázolására.
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

Egy S klózhalmazbólvaló lineáris input rezolúciós levezetés egy olyan q1, p1, q2, p2 ...qn, pn klózsorozat, ahol qiS minden i-re. p1S. pi a p(i-1),q(i-1) rezolvense ha i2.

Rezolúciós stratégiák. Lineáris rezolúció teljes. A lineáris input- és az egység rezolúció nem teljes csak Horn logika esetén. Horn logika az összes Horn formulák halmaza (szintaktikus megfogalmazás) vagy a Horn formulákkal szimbolizált összes leképezések halmaza (szemantikus megfogalmazás). Horn formula Horn klózokból álló KNF (0. rend) illetve olyan Skolem normálformula, ahol a mag Horn klózokból álló KNF (1. rend).
Horn klózok. - legfeljebb egy nem negált literált tartalmaznak.
{AB, AB, AB, AB} nincs lineáris input  cáfolat.
{BC, AC, AB, AC, C} van lineáris input  cáfolat.
Teljes levezetési fa, a C-ből való összes levezetést tartalmazza.

		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

A rezolúciós tételbizonyítás lépései:

1. Átírni a feltételeket és átírni a negált tételt KNF maggal rendelkező Skolem formulává, 0. rendben KNF alakú formulává.

2. Ebből állítjuk elő a változótiszta (változóidegen klózokból álló) S klózhalmazt.
Választunk egy rezolúciós algoritmust és azzal feldolgozzuk az S-t. Ha van rezolúciós cáfolat, akkor a tételformula valóban következmény.
***
Megjegyzés: A továbbiakban elsősorban az 1. rendű logika nyelvén formalizált problémamegoldással foglalkozunk. Azonban a rezolúciós kalkulus másodrendű kiterjesztése már ismert. Egy ilyen kiterjesztés beépítése implementált rezolúciós kalkulusokba már létezik. Nulladrendű klózhalmazokkal a rezolúciós stratégiák technikájának megismertetése miatt foglalkozunk.
Megjegyzés: A a változótiszta elsőrendű  S klózhalmaz előállítására több algoritmus ismert. Ezek bonyolultsága nagyon eltérő, azonban a végeredmény ugyanaz. Egy elsőrendű  S klózhalmaz leírása esetén a kvantorokat nem írjuk a klózok elé helytakarékosság miatt. Tehát 
S={xy(P(x)Q(x,f(y))), zv(P(g(z))P(v)), uQ(g(u),u)} helyett
A {P(x)Q(x,f(y)), P(g(z))P(v), Q(g(u),u)} elsőrendű literálok diszjunkcióinak halmazát irjuk.
Komplemens párnak nevezünk két ellenkezően negált, szimbólumról szimbólumra megegyező atomi formulát.
Illesztő helyettesítésnek (unifikációnak) nevezzük azt a  helyettesitést, amelynek alkalmazásával két azonos predikátumszimbólummal kezdődő lirerál alakja egyforma lesz (P(t1,…,tn).= P(g1,…,gn).)= (P(h1,…,hn).

Elsőrendű rezolvens
Ha aK1=L1K1’, K2=L2K2’ és L1, L2-re van  illesztő helyettesités, ahol és L1 = L2, akkor a két klóznak van rezolvense a 
K=K1’ K2’. Jelölés  K= rez(K1,K2).
A rezolvens tulajdonsága: {K1,K2} = K
A logika és a PROLOG.
A PROLOG nyelv szintaxisa lényegében az elsőrendű logika szintaxszisa. A problémát, a feltételeket és a környezet axiómáit formalizáljuk. A rezolúciós kalkulusal való problémamegoldáshoz előállítjuk az elsőrendű klózhalmazt. 
A PROLOG nyelven megírt programot egy lineáris input stratégiát megvalósító algoritmus dolgozza fel. Az algoritmus a tétel negáltját használja kiinduló klózként.
A következő megszorítások általában fennállnak. 1. A lineáris input rezolúció alkalmazhatósága érdekében a feltételeket leíró formulák csakis Horn formulák lehetnek, ahol a klózok tartalmaznak nem negált literált (definit klóz). 2. A tétel negáltját leíró formula olyan klóz, amely csak negált literálokat tartalmazhat.

A logikai programozás elemei 
•	egy lineáris input rezolúciós algoritmus olyan stratégiával, hogy képes legyen bejárni a teljes levezetési fát. 
•	A logikai program a feltételeket megadó definit klózok meghatározott rend szerint felsorolva.
•	a tétel negáltját leíró Horn klóz (csak negált literálokat tartalmaz). Ez a célklóz - ezzel indítjuk a rezolúciós levezetést.
A logikai programozásban alkalmazott rezulúciós stratégiát és egyéb “saját “ eszközöket az ítéletlogika nyelvi eszközeinek felhasználásával mutatjuk be.
A klózhalmaz elemei      DAB, alakúak. 
Ez az ABD, azaz az ABD formulát jelenti. 
A logikai programklóz alakja: D:-A,B vagy D:-B,A. Igy a “ :-” - höz viszonyított hely adja meg azt, hogy 
a klózban az illető literál negált vagy nem.
D:-A,B - ben D a fej, A,B a törzs.
A logikai programban az azonos fejjel rendelkező klózok egymásután egy “partícióban” kell hogy legyenek. A partícióban a programklózok sorrendje és a törzsben a literálok sorrendje a programozó által leírt sorrend.

A {BC, AC, AB, AC, C} klózhalmaz, AB tételformula esetén AB tétel negáltja
 a logikai program,   		
	A:-C.	szabály		:-A,B.	célklóz
	B:-C.	vagy
	C:-A.	definíció
	C:-.	tényállítás

A rezolúciós algoritmus a célklóz bal első literálját választja ki. A rezolvensképzéshez a kiválasztott literállal kezdődő partíció első klózát használja fel és megjegyzi a partíció soronkövetkező elemét. 
Algoritmus.
1. Ha a célklóz az  akkor megkaptunk egy rezolúciós cáfolatot. Vége.
2. A célklóz kiválasztott literáljával kezdődő partíció soronkövetkező klózát használja fel a rezolvensképzéshez, ha ilyen van. Ha nincs, akkor folyt. 4. 
3. Ha van ilyen de nincs rezolvens, akkor folyt. 4. 
Ha van rezolvens, a rezolvenst a kiválasztott literál helyére írja. Az új célklózzal folyt.1. lépés.
4. Visszalépés egy szinttel a levezetési fában. Ha ez nem lehet, akkor vége. Ha lehet folyt. 3.
Ezzel a visszalépési taktikával a rezolúciós algorimus stratégiájával felépíthető teljes levezetési fát “mélységben először” módon járjuk be az  első levezetéséig.

Példa
:-A,B. (1)
A:-C.
:-C,B. (2)
       C:-A.	     C:- (2)
:-A,B.			:-B. (1)
célklóz ism.			B:-C.
kudarc				:-C.(2)
			C:-A.		C.
			:-A.		     
			kudarc		siker
Ha az összes, a célklózzal induló levezetést (megoldást) kell keresni, akkor a siker esetén is vissza kell lépni, ezt a mindig kudarcot jelentő FAIL literálnak (ami egy “beépített eljárás”)a célklóz utoljára feldolgozandó pozíciójába írásával érjük el.

	:-A,B,FAIL

	      A:-C, FAIL. (1)

	:-C,B, FAIL.

	      C:-A. (2/1)	C:-. (2/2)

	:-A,B, FAIL.		:-B, FAIL.
	ismétlődik a cél,
	 visszalépés			B:-C. (1)

				:-C, FAIL.

			      C:-A. (2/1)	   C:-. (2/2)

			:-A, FAIL.		, FAIL		de nincs többlevezetés.

			    A:-C. (1)	

			:-C, FAIL.
		ismétlődik a cél,
		 visszalépés
Megjegyzés. Ha az algoritmus nem ismeri fel a cél ismétlődését, akkor végtelen ciklus keletkezik. Példa végtelen ciklusra. 
P:-P. Célklóz: :-P

Függ-e az eredmény a partíció sorrendjétől?
Cseréljük meg a C partíció sorrendjét.
Az új sorrend:
	C:-.
	C:- A.

A levezetés:
	:-A,B.

	      A:-C. (1)

	:-C,B.

	     C:-. (2/1)

	:-B.

 	     B:-C. (1)

	:-C.

	     C:-. (2/1)

Lehet több szintet is visszalépni, de ez speciális vezérlési feladat. Ez a “vágás” (cut). Jele: ! vagy /.

A működésének megértéséhez az “ős” fogalom ismerete szükséges.

Egy lieáris input levezetésben egy központi klózbeli L literál őse az a központi klózbeli literál, amelyet az L-et tartalmazó mellékklóz fejével rezolváltuk, valamint az ősök ősei.

Példa
A program		A levezetés
a:-b,c.				:-a.
b:-e.				 a:-b,c.
c:-d,e,f.				:-b,c.
c:-a.				 b:-e.
d:-.				:-e,c.
e:-.				 e:-.
cél: :-a.				:-c.
				 c:-d,e,f.
				:-d,e,f.
				d:-.
				:-e,f.
				 e:-.
				:-f.	Mi az :-f. őse? 	A	 :-c. és az	 :-a.
Az őskeresés
A “vágás” (!,/) hatása: ha egy visszalépés egy ! vagy /-t érint, akkor a “vágás” közvetlen ősét is kudarcosnak kell tekinteni. Tehát vissza kell lépni az ős szintje fölötti centrális klózra. Vagyis levágjuk a levezetési fában az ős szintje alatti maradék levezetési fát.

Bővítsük a fenti feladatot egy “vágás” bevezetésével

A program		A levezetés
a:-b,c.				:-a.
b:-e.				 a:-b,c.
c:-d,e,!,f.			:-b,c.
c:-a				 b:-e.
d:-.				:-e,c.
e:-.				 e:-.
cél: :-a.				:-c.
				 c:-d,e,!,f.
				:-d,e,!,f.
				d:-.
				:-e,!,f.
				 e:-.
				:-!,f.
				 !,f
				:-f.	Mi az :-f. közvetlen őse? 	A	 :-c. és a második választási lehetőséget a :-c-re nem használhatjuk. Visszalépés :-e,c.-re, :-b,c.-re, végül :-a.-ra és a program kudarccal fejeződik be.

Egy feladat, ahol a vágást alkalmazni kell például 
a többszörös elágazás megvalósítása logikai programmal.

A programokban a kapcsolók sémája
	 if  a1 then b1, 
else if  a2 then b2, 

	   
else if an-1 then bn-1, 
else  an 

Ennek megvalósítása logikai programmal.

		Logikai program összetevői 
A kapcsoló definíciója. 		Az aj , bj  -k egy definiálása 
							
	 p:-  a1 ,/, b1.				b1:-
	 p:-  a2 ,/, b2. 				b2:-
	   					b3:-
	   					a2:-
	   					a3:-
	 p:- an-1 ,/, bn-1. 				
	 p:- bn .					

Célklóz:  :-p					

A cut, / működése:
A levezetésben átlépjük,(mintha mindig ki lehetne rezolválni) de megjegyezzük, hogy ott / szerepelt a levezetésben. Úgy is tekinthetjük, hogy a / mindig igaz.

Visszalépéskor, ha az elért központi klózból a cut  alkalmazásával haladtunk tovább, akkor mekeresi a vezérlés ennek a cutnak az ősét és még egy központi klózzal feljebb lépve folytatja a bejárást. Olyan mintha az őst tekintené sikertelennek, bár nem nézte végig.

A levezetési fa. n=8.

:-p
   p:-  a1 ,/, b1. (8/1)	p:-  a2 ,/, b2.(8/2),  
:-  a1 ,/, b1.		:-  a2 ,/, b2
kudarc			    a2:-
			:- /, b2
			    /:-
			:- b2
			kudarc, visszalép az ősre (ami a célklóz) és befejeződik

PROLOG, mint tételbizonyító eszköz az 1 rendű logikában
Elsőrendű rezolúciós elv. A rezolúciós elv eldöntésproblémája - 
S={ x1,...,xnk1,...,x1,...,xnkr } 1 rendű klózhalmaz ból levezethető-e az üres klóz - levezetése ekvivalens S kielégíthetetlenségével.

S={ x1,...,xnk1,...,x1,...,xnkr } 1 rendű klózhalmaz kielégíthetetlensége adott univerzumon ekvivalens a klózok magjainak összes alappéldányából alkotott alapklózhalmaz kielégíthetetlenségével.
Adott univerzumon definiálható összes struktúrák felsorolhatók szemantikus fával.
Fogalmak:
Bázis az univerzum feletti összes alapatomok sorozata:
A1, A2, ..., An, ...
Interpretáció egy 
M1, M2, ..., Mn, ...		sorozat, ahol 
		Mk = Mk ha Ak igaz és 
		Mk = Mk ha Ak hamis.
Szemantikus fa, olyan bináris fa, amelynek a szintjei rendre megfelelnek a bázis elemeinek és a k-adik szint elágazó élein egyik ágát Ak-val a másikat Ak-val cimkézzük. Így minden ágon egy interpretációt jelenítünk meg.

Herbrand eredményei.
Herbrand megmutatta, hogy az 1 rendű klózhalmazok kielégíthetetlenségét elegendő egy, a klózhalmaztól függő univerzumon vizsgálni - Herbrand univerzumon.

Herbrand univerzum (S klózhalmazhoz)
•	Hj j-edrendű Herbrand konstansok halmaza.
•	Fj =S-beli függvényszimbólumok összes alaphelyettesítése a Hj-1 elemeivel
H0 - {a1, ..., an} S konstansai vagy  {a} fiktív konstans

	   
Hk - Hk-1  Fk-1 
H - k=0, 1, 2, ... Hk a Herbrand univerzum.

 Példa 
Tekintsük a K= {P(x),   Q(y,z) P(z),   Q(u,f(u))} klózhalmazt. 
H ={a, f(a) , f(f(a)),....,f...f(a)...), ...}
H. 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))),...}
I interpretáció:
{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 H. bázis szemantikus fájának három első szintje.

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

Herbrand tételek.
•	T1. Egy S, 1 rendű klózhalmaz kielégíthetetlen akkor és csak akkor, ha kielégíthetetlen Herbrand univerzumon.
•	H1 Egy S, 1 rendű klózhalmaz kielégíthetetlen akkor és csak akkor, ha van véges zárt szemantikus fája.
•	H2. Egy S, 1 rendű klózhalmaz kielégíthetetlen akkor és csak akkor, ha alapklózai halmazának van véges kielégíthetetlen részhalmaza
Következmény: Ha egy S, 1 rendű klózhalmaz kielégíthetetlen akkor alapklózai halmazából levezethető az üres klóz.
Ez azt jelenti, hogy az elsőrendű klózok magjainak vannak olyan alaphelyettesítései a Herbrand univerzum elemeivel, hogy komplemens párok alakulnak ki a rezolváláshoz. Figyelembevéve, hogy a Herbrand univerzum elemei alaptermek A komplemens alapatompár argumentumainak alakja vagy már eredetileg is a változónévtől eltekintve egyforma volt 
P(f(x))..., P(f(y ))...,   vagy az alaphelyettesítéssel lehetett egyformává tenni. Ezt csak akkor érhettük el, ha a komplemens pár argumentuma közül a kisebb összetettségű megegyezik a másik argumentumának kezdőszeletével: P(f(g(x)))..., P(f(y ))... 
Az első esetben x/y - x-et y-nal illesztve minden alaphelyettesítés komplemens párt ad. 
A második esetben y/g(x) - y-t g(x)-el illesztve már minden alaphelyettesítés komplemens párt ad. Tehát az illesztés utáni klózok az eredetiek alappéldányaiból csak a komplemens párt tartalmazókat adja. Intuitíve nincs szükség az alapklózokra, mivel az illesztett klózok rezolválhatók.

Példa.
S={xyP(x)Q(x,f(y)), zvP(g(z))P(v), uQ(g(u),u)}
Herbrand univerzum: a, g(a), f(a), g(f(a)), …
A táblázatban alaphelyettesítésekhez tartozó alapklózokat találunk.

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))	

Megmutatunk egy alaprezolúciós levezetést. Az illesztő helyettesítés a lehetséges alaphelyettesítéseket megtalálja.

alaprezolúció						1 rendű rezolúció
1. Q(g(f(a)), f(a))			u/f(a)			1. Q(g(u),u)		x/g(u), u/f(y)
2. P(g(f(a)))Q(g(f(a)),f(a))	x/g(f(a)), y/a		2. P(x)Q(x,f(y))
3. P(g(f(a)))						3. P(g(f(y)))
4. P(g(f(a)))			z/f(a), v/g(f(a))		4. P(g(z))P(v)	v/g(z) faktorizál, z/f(y), 
5. 							5. 
Az 1-5 alaprezolóciós levezetés helyett az olyan alaphelyettesítéssel kapott levezetés is sikeres lenne, ahol az "a" helyett tetszőleges H univerzumbeli elem áll. Ekkor viszont lehet egy változót (pl. az y-t) is az "a" helyére tenni.
1. Q(g(u),u)		u/f(y)
2. P(x)Q(x,f(y))	x/g(u), u/f(y) azaz x/g(f(y))
3. P(g(f(y)))
4. P(g(z))P(v)	v/g(z) faktorizál, z/f(y) illeszt azaz v/ g(f(y))
5. 

Illesztő (unifikáló) helyettesítés.
Fogalmak:
W={P(f(g(x))), P(f(y )), P(z)} illesztendő literálhalmaz.
D={ f(g(x)), f(y ), z}, W összeférhetetlenségi halmaza
 az illesztő helyettesítés.
Algoritmus
1. k=0, Wk=W, k=
2. Ha Wk egyetlen atom, akkor vége és k a legáltalánosabb illesztő helyettesítés W-re.
3. Szerkesszük meg Wk összeférhetetlenségi halmazát Dk -t.
4. Ha van Dk -ban olyan vk változó és tk term hogy vk nem fordul elő tk-ban, akkor 5. lépés. Egyébként nincs illesztés, vége.
5. k+1 =k (vk / tk), Wk+1 = Wk(vk / tk)= Wk+1, 
k=k+1 és 2. lépés.

Az algoritmus a legáltalánosabb illesztő helyettesítést adja.
Elsőrendű rezolvens.
Ha K1=L1K1’, K2=L2K2’, ahol K1 és K2 már faktorizált klózok és  a legáltalánosabb illesztő helyettesítés L1,L2-re akkor K=K1’K2’ a K1, K2 elsőrendű rezolvense.
Fennáll, hogy K1, K2= K, így az elsőrendű rezolúciós levezetés értelmezhető.
Ezzel és a lineáris input stratégiával és speciális Horn klózokkal dolgozik a PROLOG.

 Az elsôrendű klózok és a PROLOG programklózai.
A változóidegen klózokat tartalmazó KNF maggal rendelkezô Skolem formula S=x1,...,xnC1...x1,...,xnCr. Ezek az elsôrendű klózok x1,...,xn (L1...Ls) alakúak, ahol Li (1is) (pozitív vagy negatív) elsôrendű literálok. Egy 1. rendű klóz általános alakja 
x1,...,xn ( B1...BsA1...Ak ) ami tulajdonképen
x1,...,xn ( B1...BsA1...Ak ).
A PROLOG jellegű programmozási nyelvekben a program utasításai "elsôrendű klózok". Legtöbb szintaxis szerint ezeket (mind a :-  mind a    jelölést használják)
A1,...,Ak :- B1,...,Bs alakban írják le (a kvantorok nincsenek feltüntetve és a negáció jelet sem kell kiírni, mert a literál helyzete mutatja, hogy az illetô literál negált-e vagy nem az eredeti klózban. 
B1,...,Bs - konjunktív vagy összetartozó feltételek (törzs, body)
A1,...,Ak - diszjunktív vagy alternatív feltételek (fej).
Logikai programklóz azonban csak	 A :- B1,...,Bs   vagy 	A :-  lehet
Gyakorlat.
Bizonyítani a {K1,K2} = K -t.
Mutatni lineáris, lineáris input levezetést.
Szerkeszteni teljes levezetési fákat különböző klózokhoz.
Őskeresés levezetési fában.
Átírás prenex, Skolem formába. Kvantor ki- és bevitel.
Egyszerű PROLOG programok írása, kézi futtatása
Illesztő helyettesítés keresésére példa.		Rezolúciós levezetésre példa.

Problémamegoldás.
Egyszerű kapcsolatok leírása. Pl. családi kapcsolatok
A család élő tagjai a következők nagyapa : István, a fia Imre. Imre felesége Zsuzsa. Kettőjük gyereke Péter. Péter felesége Kati. Kettőjük gyerekei Anna, Balázs, Kata. Kati anyja Katalin. 
Bevezetjük a következő relációkat. Apa (x.y), Anya(x,y).
A családi kapcsolatrendszer a tények alapján:
A logikai program tényállításai
Apa (István, Imre) :-
Apa(Imre, Péter) :-
Apa(Péter, Balázs) :-
Apa(Péter, Anna) :-
Apa(Péter, Kata) :-
Anya(Zsuzsa, Péter) :-
Anya(Katalin, Kati) :-
Anya(Kati, Balázs) :-
Anya(Kati, Anna) :-
Anya(Kati, Kata) :-
Az adatok ilyen felsorolása elegendő ahhoz, hogy a rokoni kapcsolatokat megtudjuk.
Megadjuk a kapcsolatok definícióját:
xy(Apa(x,y)Anya(x,y)Szülője(x,y))
xzy(Apa (x,y)Szülője(y,z) Nagyapa(x,z))
xzy (Anya (x,y)Szülője(y,z) Nagyanya(x,z))
Ezekből lesz a logikai programban a szabály vagy definíció
Szülője(x,y) :- Apa(x,y)
Szülője(x,y) :- Anya(x,y)
Nagyapa(x,z) :- Apa (x,y), Szülője(y,z)
Nagyanya(x,z) :- Anya (x,y), Szülője(y,z)
Ezek az egyszerű definíciók

A tétel lehet
konkrét				egzisztenciális
1. Szülője(István, Imre) ?		3. x Nagyanya(x, Balázs)
2. Nagyanya(Zsuzsa, Anna) ?	4. xy Szülője(x,y)

Válaszlojuk meg az 1.kérdést
:- Szülője(István, Imre)	célklóz
	Szülője(x,y) :- Apa(x,y) (2/1)
:- Apa(István,Imre)
Apa(István,Imre)

Válaszlojuk meg az 3.kérdést		A negált tétel mint 1 rendű klóz xNagyanya(x, Balázs), 
mint célklóz  :- Nagyanya(x, Balázs)
A válasz x-re V(x) válaszrelációval. Az  elérése esetén a V reláció egy választ ad. Az összes megoldásért FAIL a végére. 
(Egyértelműség miatt szükség van a klózok változóidegenségére)

:- Nagyanya(x, Balázs) , V(x), FAIL	célklóz
	Nagyanya(x1,z1) :- Anya (x1,y1), Szülője(y1,z1)	z1 / Balázs x /x1.
:- Anya (x1,y1), Szülője(y1,Balázs),V(x1), FAIL
	Anya(Zsuzsa, Péter) :-.(5/1)  x1 /Zsuzsa,  y1 / Péter
:- Szülője(Péter,Balázs), V(Zsuzsa), FAIL
	Szülője(x2,y2) :- Apa(x2,y2)	x2/Péter , y2/Balázs
:- Apa(Péter, Balázs), V(Zsuzsa), FAIL
	Apa(Péter, Balázs) :-
V(Zsuzsa) vagyis , FAIL, tehát visszalép ....V(Katalin) is megoldás lesz.

Válaszoljuk meg az 4.kérdést		A negált tétel:	x y Szülője(x,y)
:- Szülője(x,y), V(x,y), FAIL
	Szülője(x1,y1) :- Apa(x1,y1)	x/x1, y/y1
:- Apa(x1,y1), V(x1,y1), FAIL
	Apa (István, Imre) :-	(5/1)	x1/István, y1/Imre	Apa(Imre, Péter) :-(5/2)
:- V(István,Imre), FAIL				:- V(Imre, Péter), FAIL

Rekurzív kapcsolatok leírása. Pl. családi kapcsolatokban Ős fogalom.
 xy-nak őse az anyja, az apja, valamint az ősők ősei.
Ős(x,y):-Szülője(x,y).
Ős(x,y):- Ős(x,z) , Szülője(z,y).

:-Ős(Imre, Anna)
	Ős(x,y):- Szülője(x,y)	x/Imre, y/Anna.		Ős(x,y):- Ős(x,z) , Szülője(z,y).
:- Szülője(Imre,Anna)						:- Ős(Imre,z) , Szülője(z,Anna).
   . Szülője(x1,y1) :- Apa(x1,y1) .   Szülője(x1,y1) :- Anya(x1,y1)		Ős(x1,y1):-Szülője(x1,y1).
:- Apa(Imre,Anna)		    :- Anya(Imre,Anna)			:-Szülője(Imre,y1). Szülője(y1,Anna).
kudarc az apa partícióval visszalép	       kudarc az apa partícióval visszalép sít.

kudarc az Anya partícióval visszalép az  Ős partícióra	kudarc mint előbb vissza az Ős-re

Néhány egyszerű logikai program ( a vágás és a sorrend).
Tagadás
NOT a:-a,/,FAIL.	
NOT a:-				
célklóz: :- NOT q(x) 			 sorrend!! 
ha q(x) előfordul a prg.ban, akkor FAIL, ha nem, akkor NOT q(x) igaz.

.1. :- NOT q(x)
 2. NOT a:-a,/,FAIL.		(a/ q(x))
 3. :- q(x),/,FAIL.	r(1,2)					
 4. q(x):-				benne van a logikai programban	
 5. :-/,FAIL)	kudarc, vissza, / miatt ősre vissza ez az 1,ami kudarcos. Visszalépés nincs.

Ha megfordítjuk a sorrendet, a program nem működik jól.
1. :- NOT q(x)
2. :- NOT a:-
3.  		függetlenül a q(x)-től

Útkeresés gráfban.
Példa rekurzív definícióra és végtelen ciklusra.

út(x,y):-él(x,y).
út(x,y):-él(x,z),út(z,y).
él(a,b):-					a			b
él(a,d):-					
él(d,c):-					
él(b,a):-					d			c

cél: :-út(a,c)
					:-út(a,c)

út(x,y):-él(x,y).(2/1)		út(x,y):-él(x,z),út(z,y).(2/2)

:-él(a,c)					:-él(a,z),út(z,c).
kudarc	
							él(a,b):-

							:-út(b,c)

út(x,y):-él(x,y).(2/1)		út(x,y):-él(x,z),út(z,y).(2/2)

:-él(b,c)					:-él(b,z),út(z,c)
kudarc	
							él(b,a):-

							:-út(a,c)

Ismétlődik a cél. Végtelen ciklus. 

Ős(P) egy beépített program, amely az Ős(P) őseit mevizsgálja és igaz (sikeres), ha a P-vel illesztett literál megegyezik valamelyik ősével.
Programmódosítás:
út(x,y):-él(x,z),NOT(ős(út(z,y))),út(z,y), .
					:-út(a,c)		x/a, y/c
út(x,y):-él(x,y).2/1		út(x,y):-él(x,z), 
						NOT(ős(út(z,y))),út(z,y).2/2

:-él(a,c)		:-él(a,z),NOT(ős(út(z,c))),út(z,c).
kudarc		(z/b) él(a,b):- 4/1		él(a,d) 4/2 (z/d)

				:- NOT(ős(út(b,c))),út(b,c)
			nincs út(b,c) ős

							:-út(b,c) (x/b,y/c)
út(x,y):-él(x,y).2/1			út(x,y):-él(x,z),				    NOT(ős(út(z,y))),út(z,y). 2/2
		
:-él(b,c)			:-él(b,z),NOT(ős(út(z,c))),út(z,c)
kudarc			      él(b,a):- 4/4

					:- NOT(ős(út(a,c))),út(a,c)

		van út(a,c) ős, egyszerű visszalépés
		az első lehetséges elágazáshoz

él(a,d) (5/2)

				:- NOT(ős(út(d,c))),út(d,c)
									nincs út(d,c) ős

							:-út(d,c) (x/d,y/c)
			út(x,y):-él(x,y).2/1		

							:-él(d,c)	 
							  él(d,c):- 4/3

de nem adja meg az útvonalat!!
Mi lehet a megoldás?		Más módon kell megfogalmazni a problémát.

További rekurzív definíciók. (családi kapcsolatok). Mikor lehet szükség a teljes definíció “csak akkor” (only if) részére?
1. ős(x,y):-szülője(x,y)		x az y-nak
2. ős(x,y):-szülője(x,z),ős(z,y)
3. nagyszülője(x,y):- szülője(x,z),szülője(z,y)

szülője(,y):-	jelentése	yx szülője(x,y)	=f(y) Skolem fv.

4. gyereke(x,y):-szülője(x,y)		gyereke(x,y) jelentése:: gyereke x-nek y.
5. szülője(x,y):-gyereke(x,y)	

6. szülője(x,y):-anyja(x,y)
7. szülője(x,y):-apja(x,y)

Adatok pl. gyereke(kati,anna):-

Kapcsolat gráf definiálóból a definiált felé mutat az él.

szülője(x,y)			gyereke(x,y)

ős(x,y)		anyja(x,y)	apja(x,y)

A (4,5) egy if and only if definíció.
Az (1,2), a (3), a (6,7) “csak” if   then  definíció.
A teljes definiáltsághoz hiányzik a definíció only if része. Ez nem egyelemű törzs esetén már nem lesz Horn klóz.
A nagyszülője(x,y):- szülője(x,z),szülője(z,y) definíció only if része vajon a 
szülője(x,z),szülője(z,y):-nagyszülője(x,y)  ??

A teljes definíció:
xy (nagyszülôje(x,y) z(szülôje(x,z)szülôje(z,y))). 
Az if then definíció : ha van z, hogy szülôje(x,z) és szülôje(z,y), akkor nagyszülôje(x,y). Formulával
 xy(z(szülôje(x,z)szülôje(z,y))nagyszülôje(x,y))= xy(z(szülôje(x,z)szülôje(z,y))nagyszülôje(x,y))=
xy(z(szülôje(x,z)szülôje(z,y))nagyszülôje(x,y))			mint programklóz
nagyszülôje(x,y):- szülôje(x,z),szülôje(z,y).

Az only if rész  
xy(nagyszülôje(x,y)z(szülôje(x,z)szülôje(z,y)))     =     xy(nagyszülôje(x,y)
z(szülôje(x,z)szülôje(z,y)))= 
xy(nagyszülôje(x,y)(szülôje(x,f(x,y))szülôje(f(x,y),y))) 
az f(x,y) a Skolem függvény pl. f  közvetlen egyenesági rokon. A klózok a következôk lesznek: 
szülôje(x,f(x,y))szülôje(f(x,y),y):-nagyszülôje(x,y) -bôl
a) szülôje(x,f(x,y)):-nagyszülôje(x,y) és 
b) szülôje(f(x,y),y):-nagyszülôje(x,y).

Definíciók kapcsolatáról - Milyen kérdések megválaszolásához szükséges az if and only if definíció?
A fenti programhoz az  “ős-e a nagyszülő?”{ xy (nagyszülője(x,y)ős(x,y))} kérdés megválaszolását,
Csak az only if alak felhasználásával! és a megszokott stratégia feladásával érhetjük el.
A tétel (univerzálisan kvantált!!!)

xy (nagyszülője(x,y)ős(x,y))  = xy (nagyszülője(x,y)ős(x,y))
A tétel negáltja
xy ( nagyszülője(x,y) ős(x,y))
cél: 	:-nagyszülője(x*,y*),ős(x*,y*) vagyis 1. nagyszülője(x*,y*), 2. :-ős(x*,y*), ( két klóz!!!)
1. nagyszülője(x*,y*):-	célklóz
2. :- ős(x*,y*) 		célklóz
3. szülôje(x,f(x,y)):-nagyszülôje(x,y)		a) klóz
4. szülôje(x,f(x,y)):-	rez(1,3)	(x*/x), (y*/f(x,y))
6. ős(x’,y’):-szülője(x’,y’)	1. prgklóz
7. :-szülője(x’,y’) 		rez(2,6)	(x*/x’), (y*/y’)
8. 			rez(4,7)	(x’/x), (y’/f(x,y))

Válaszadás. Kiegészítő adatok. Pl. bevezetünk egy speciális nevű V(...) predikátumot a tételbeli változókkal. V-t felismeri az algoritmus és nem akarja rezolválni, vagy  nincs V, de az algoritmus fel van készítve, hogy a sikeres levezetések esetén kiírja a cél változóinak értékeit.

gyereke(A,B):-
gyereke(B,C):-
gyereke(C,D):-
cél -	:-ős(x,y), V(x,y)
		ős(x,y):-szülője(x,y)
	:-szülője(x,y), V(x,y)
		szülője)x,y):-gyereke(x,y)
	:-gyereke(x,y), V(x,y)
		gyereke(A,B):-
	, V(A,B)

A logikai programozás klasszikus témái .
Rekurzív definíció – listakezelés

L=[a, b, c, d] =	[a b, c, d]
		    lista feje	lista toldaléka.
üres lista = []

Ábrázolása bináris fával

		.
	a		.
		b		.
			c		.
				d		[]

“L” lista eleme definíciója:

eleme(X,[Xtold]):-
eleme(X,[Ytold.]):- eleme(X,[told])

cél		:-eleme(b,[a,b,c,d])
eleme(X,[Xtold]):- 	eleme(X,[Ytold.]):- 
X/b, Xtold/[a,b,c,d])		eleme(X,[told])
kudarc.					X/b,Y/a,told/[b,c,d])
						:-eleme(b,[ b,c,d])
							eleme(X,[Xtold]):-
							X/b, told/[c,d])

elemtörlés
del(X, [Xtold], [told]):-
del(X, [Ytold], [Ytold1]):-del(X,told,told1)

cél		:-del(b, [a,b,b,d], L), V(L)
1.del(X, [Xtold], [told]):-
X/b, Xtold/[a,b,b,d]),L/told
kudarc.
					2.del(X, [Ytold], [Ytold1]):-del(X,told,told1)
					X/b, Ytold/[a,b,b,d]), L/[atold1]
				:-del(b, [b,b,d]),told1),V([atold1])
					del(X, [Xtold], [told]):-
					X/b, Xtold/[b,b,d]), told1/told
				, V([ab,d])      (csak egy előfordulást töröl)

lista hossza, az s(x) rákövetkezési függvény kiszámításának megvalósítása a háttér.
hossz([],0):-
hossz([Xtold],s(N)):-hossz(told, N)
cél		:-hossz([a,b,c], K)
hossz([],0):-
kudarc
			hossz([Xtold],s(N)):-hossz(told, N)
			Xtold /[a,b,c], K/s(N)			K/s(N)
						:-hossz([b,c], N)
hossz([],0):-
kudarc
			hossz([Xtold],s(N1)):-hossz(told, N1)
			Xtold /[b,c], N/s(N1)			N/s(N1)
						:-hossz([c], N1)
hossz([],0):-
kudarc
			hossz([Xtold],s(N2)):-hossz(told, N2)
			Xtold /[c], N1/s(N2)				N1/s(N2)
						:-hossz([], N2)
hossz([],0):-
N2/0								N2/0
									K/s(s(s(0)))

ciklusszervezés listával
lcikl([]):-
lcikl(XL):- print(X),lcikl(L)
ciklusszervezés listával és visszalépéssel
vcikl(L):-eleme(X,L),print(X),FAIL
vcikl(L):-
cél		:-vcikl([a,b])
				vcikl(L):-eleme(X,L),print(X),FAIL
			:-eleme(X, [a,b]),print(a),FAIL
eleme(X, [X,told]:-)		eleme(X,[Ytold.]) :-
:-print(a),FAIL			eleme(X,[told])
print(a)			:-eleme(X,[b]), print(X),FAIL
:-FAIL	   eleme(X, [X,told]):-		      eleme(X,[Ytold.]) :- eleme(X,[told])
				:- print(b),FAIL	:- eleme(X,[]) , print(X),FAIL
			      print(b)				kudarc, befejeződik.
				:-FAIL

ciklusszervezés számlálással
scikl(0):-
scikl(N):-less(0,N),minus(N,1,N1), 
				print(N), scikl(N1)

További listaműveletek
lista utolsó eleme						cél
last(X,[X]):-
last(X,[Y.L]):-last(X,L)		last)X,[1,2,5],V(X)

két lista konkatenációja
1. conc([],L,L):-
2. conc([X|L1],L2,[X|L3]:-conc(L1,L2,L3)
cél :-conc([a,b],[g,h],Q),V(Q)	Q/[X|L3],X/a
conc([],L,L):- 			conc([X|L1],L2,[X|L3]:- 
kudarc 					conc(L1,L2,L3
				:- conc([b],[g,h],[L3]),V([a|L3])
conc([],L,L):- 			conc([X|L1],L2,[X|L3’]:- 
kudarc 				conc(L1,L2,L3’)	X/b,L3/b|L3’, L2/[g,h]
				:-conc([],[g,h],L3’]),V([a|b|L3’])
					conc([],L,L):-	L/[g,h],L/L3’
				, V([a,b,g,h])

Egy elem minden előfordulásának törlése
delm(X,[],[]):-
delm(X,[X|L],M):- /, delm(X,L,M)
delm(X,[Y|L],[Y|M]):- delm(X,L,M)
cél			:- delm(a,[a,b,a,d],Q),V(Q)
1.delm(X,[],[]):-	kudarc		
				2. delm(X,[X|L],M):- /, delm(X,L,M)
			:- /, delm(a,[b,a,d],M)				M/Q
1.delm(X,[],[]):-	kudarc
		2. delm(X,[X|L],M’):- /, delm(X,L,M’)
			X/a, [X|L]/[b|a,d]	kudarc
				3. delm(X,[Y|L],[Y|M’]):- delm(X,L,M’)
			X/a, [Y|L]/[b|a,d],					M/[b|M’]
						:-delm(a,[a,d],M’)
1.delm(X,[],[]):-	kudarc
			2.delm(X,[X|L],M’’):- /, delm(X,L,M’’)
			X/a és [X|L]/[a|d]					M’/M’’
				:-/, delm(a,d,M’’)
1.delm(X,[],[]):-	kudarc
		2.delm(X,[X|L],M*):- /, delm(X,L,M*)
		X/a,[X|L]/d	kudarc
				3. delm(X,[Y|L*],[Y|M*]):- delm(X,L*,M*)
					X/a, Y/d, L*/[], 			M’’/[d|M*]
						:-delm(a,[],M*)
				1.delm(X,[],[]):-		X/a, M*/[],
						
Q/M/ [b/M’],     M’/ M’’,      M’’/[d|M*],     M*/[]		Q=[b,d]

részhalmaz
subset([X|L],Y):-eleme(X,Y),subset(L,Y)
subset([],Y)
diszj. halmazok
diszj(X,Y):-NOT(elemeZ,X),eleme(Z,Y)
lista fordított sorrend
rev([],[]).
rev([H|T],L):-rev(T,Z), conc(Z,[H],L)
új elem hozáírás listához ismétlés nélkül
add(X, L, L1), ahol az L1-ben csak egyszer szerepel az X.

add(X,L,L):-eleme(X,L)
add(X, L, [X|L]

Input  és output változók szerepe nem kötött. Q output változót jelöl.
1. conc([],L,L):-
2. conc([X|L1],L2,[X|L3]:-conc(L1,L2,L3)

cél :-conc([a,b], Q, [a,b,e]),V(Q)	

cél :-conc([a,b],[g,h],Q),V(Q)	

cél :-conc(Q1,Q2,[a,b,g,h]),V(Q1,Q2)	
az eredmény nem meghatározott.

További beépített eljárások, max(x,y,z), less(x,y,z), add(x,y,z), mult(x,y,z),          
Program				Célklóz
NOT(*A) :- *A, /, FAIL.		:- NOT(B).
NOT(*A) :-.

AND(*X, *Y) :- *X, *Y.		:- AND(A, B).

OR(*X, *Y) :- *X.			:- OR(A, B).
OR(*X, *Y) :- *Y.

IF(*A, *B, *C) :- *A, /, *B.		:- IF(X, Y, Z)
IF(*A, *B, *C) :- *C.

IF(*A, *B) :- *A, *B).			:- IF(X, Y).
IF(*A, *B).

LESS(x, y) :- x<y.			:- less(5,7).

EQUAL(x,x) :-.

LSEQ(x,y) :- LESS(x,y), /.		:- LSEQ(6,3).
LSEQ(x,y) :- EQUAL(x,y).

R. Kowalski a "Logic for Problem Solving" c. könyvében (1979).
A formalizálás és a kvantálás problémáival foglalkozik. A létezik kvantor (x) mindig valamely fiktív indivíduumra utal (Skolem függvény), amelyet a formalizálás során lehet esetleg egy speciális jellel jelölni.
Miután a logikai progrmklózok és a célklóz speciális 1 rendű klózok a formalizálás során felmerül, hogy hogyan lehet megfelelő 1 rendű klózokat előállítani.
A feltételek és a konklúzió sokszor nem klóz alakban adottak. A formalizálás után ezeket a lehetőség szerint át kell alakítani megfeleő 1. rendű klózokká. A formalizálásnál a bizonyítandó formulát tagadni kell. Ezt úgy érjük el, hogy a negáltnak számító klózok a :- jel jobboldalára kerülnek. Erre késôbb mint leíró eszközre visszatérünk. Most nézzünk néhány jellegzetes eseteket.
Ha az eredeti megfogalmazás szerint a következmény nem egyetlen atomi formula. Lehet-e ezekben az esetekben Horn klózt kialakítani? Néhány tipikus esetet nézünk meg.
1. A következmény (vagy a tétel) legyen implikáció.
K= BA, ekkor (BA)= (BA) a tétel tagadása, ebbôl célklóz nem állítható elô mivel 
:-BA nem leírható (nem célklóz). A tétel negáltja, ami végül is BA, így két klózzal adható meg.
B:- és :-A
Nézzünk egy példát. Legyen a tétel : Minden ember halandó. x(E(x)H(x)). 
x(E(x)H(x))=x(E(x)H(x))=x(E(x)H(x)). Skolem konstans bevezetése után:E()H() és így a két klóz 
E():-, :-H().
A definícióban a következmény legyen implikáció . x(E(x)(H(x) V(x))).
Átírva x(E(x)H(x) V(x)). A V(x):-E(x),H(x). programklóz pontosan megfelel ennek.
2. A definícióban a következmény legyen konjunktív. Az adott feltételek több konklúziót implikálnak.
anyja(x,y)nô(x)szülôje(x,y)		
anyja(x,y)(nô(x)szülôje(x,y))  disztr. szab. alk.
(anyja(x,y)(nô(x))(anyja(x,y)szülôje(x,y))
az eredmény két Horn klóz: anyja(x,y)nô(x) és anyja(x,y)szülôje(x,y)
			nô(x) :-anyja(x,y)  és  szülôje(x,y):-anyja(x,y)
3. A következmény legyen alternatív. Ez lehet megengedô vagy kizáró. Alapesetben ez megengedô, de ekkor nem Horn klózról van szó. Ez egy általános rezolúciós kalkulus esetén lesz probléma.
ember(x)(nô(x)férfi(x))  Ebben az esetben a  kizáró értelmű, amit ki kell fejezni. Vagyis
ember(x)(nô(x)férfi(x))(nô(x)férfi(x)) kétszer alkalmazva disztr. szabályt:
ember(x)(nô(x)férfi(x))(nô(x)férfi(x)) konjunktív következmény, tehát kettéválasztható 
ember(x)(nô(x)férfi(x))
ember(x)(nô(x)férfi(x)), ebbôl a klózok:
nô(x),férfi(x):-ember(x)
:-nô(x),férfi(x),ember(x)
Legyen a  kizáró értelmű de megengedô értelműként irjuk fel, akkor az alternatív következmények mindegyike lehet egyszerre igaz. ami zavaró lesz, hiszen a valóságban ez nincs így.
1. állat(x),ásvány(x),zöldség(x):- 
2. állat(x):-osztriga(x)
3. ásvány(x):-tégla(x)
4. zöldség(x):-káposzta(x), hozzávéve az 5,6,7 klózokat konzisztens marad az 1-7 klóz.
5. állat(x):-baktérium(x)
6. zöldség(x):-baktérium(x)
7. baktérium(@):-

A feltételrész formalizálási problémái.
4. A feltétel legyen alternatív. Ugyanazt a konklúziót több feltétel is implikálja. Alapesetben a feltételek konjunktívak.
anyja(x,y)apja(x,y)szülôje(x,y)
(anyja(x,y)apja(x,y))szülôje(x,y) disztr. szab.
(anyja(x,y)szülôje(x,y))(apja(x,y)szülôje(x,y)) ebbôl a klózok
szülôje(x,y):-anyja(x,y)
szülôje(x,y):-apja(x,y)
5. A feltétel legyen implikációs alakú.
A feltétel: BA. A kifejezés: (BA)C átírva (BA)C ez egy alternatív feltétel, így a fenti eredmény miatt két klózt kapunk: C:-A és C,B:-
Kontrapozíciót alkalmazva is kiszámolható az eredmény. (BA)C helyett C(BA)-t tekintjük. Ezt tovább alakítva CBA a konjunktív következmény miatt CB és CA. Ennek megfelelôen a klózok 
C:-A és C,B:-.
Példa. B(x)-x boldog, SL(x)-x szereti a logikát, T(x,y)-tanítványa x, y-nak.
Bob minden tanítványa szereti a logikát
x(T(x,Bob)SL(x))
Bob boldog, ha minden tanítványa szereti a logikát
x(T(x,Bob)SL(x))B(Bob) nézzük a kontrapozíciós megoldást
B(Bob)x(T(x,Bob)SL(x))
B(Bob)x(T(x,Bob)SL(x))
B(Bob)(T(,Bob)SL())
B(Bob)(T(,Bob)SL()) és a klózok 
T(,Bob)B(Bob):-
B(Bob):-SL()
A kvantálás problémái.
A minden, valami, semmi, dolgok, egy dolog, stb. kifejezése. Néhány példa.
Egyes emberek szeretik az operát. Formalizálva: x(ember(x)szereti(x,opera)) helyett
ember()szereti(,opera):-	lenne, de ez két tényállításként jelenik meg
ember():-
szereti(,opera):-
Minden embernek van anyja.
xy(ember(x)anyja(y,x)) 		helyett
anyja(anya(x),x):-ember(x)		a klóz	(az anya(x)  a Skolem fúggvény)
yx(ember(x)anyja(y,x))		jelentése létezik olyan aki minden embernek anyja
anyja(,x):-ember(x)		a klóz.

:-jó(x),rossz(x) jelentése	Semmi sem lehet egyszerre jó és rossz x(jó(x)rossz(x))
Minden embernek van ôt szeretô szülôje. xy(ember(x)szülője(y,x))szereti(y,x), átalakítva 
x(ember(x)szülője(f(x),x))szereti(f(x),x) x[(ember(x)szülője(f(x),x))) (ember(x)szereti(f(x),x))]
A programklózok:
szülôje(,x):-ember(x)
szereti(,x):-ember(x)

Vigyázni a kvantorkiemelési szabályokra: xember(x)xlusta(x) nem kiemelhetô a x, jelentése megváltozik.

Egy logikai programklóz mint definíció:” ha törzs akkor fej”, tehát csak egy if-then definíció.
 A definíciók az if then illetve az if and only if alak.
A Horn logikán alapuló logikai programokban a definíciók if then része elegendô, mivel a célklózokban nincs negált literál,
 az if then-el definiált valami mindig pozitív literál és ezért rezolválható a célklózzal, amelyben csak negált literálok szerepelnek. 
Az only if részre akkor van szükség, ha a program tulajdonságát vizsgáljuk, vagy az adatbázis teljességét (integrity) ellenôrizzük, ha olyan a lekérdedezés (tételformula), ahol univerzális kvantor és/vagy negáció is van.
Program-tulajdonság vizsgálat.
A faktoriális program:
xy(fact(x,y)[x=0y=1]x'y'[x=x'+1fact(x',y')y=x*y'] 
A definíció if része
xy([x=0y=1]x'y'[x=x'+1fact(x',y')y=x*y']fact(x,y)), diszjunktív feltétel, vagyis
xy([x=0y=1]fact(x,y))
xy(x'y'[x=x'+1fact(x',y')y=x*y']fact(x,y)), ebbôl
xy(x'y'[x=x'+1fact(x',y')y=x*y']fact(x,y))=
xyx'y'([x=x'+1fact(x',y')y=x*y']fact(x,y)).
Az if rész klózai:
fact(x,y):-x=0,y=1
fact(x,y):-x=x'+1fact(x',y')y=x*y'
Ezzel a programmal bármely :-fact(a,y) cél megoldható, ahol az a egész szám.
A definíció only if része a program tulajdonságok vizsgálatánal már szükségesek.
Pl. itt "A 0 egyetlen faktoriálisa 1" azaz a y(fact(0,y)y=1) belátásához. A tétel negáltja 
y(fact(0,y)y=1)=(fact(0,!)!=1) (! a Skolem konstans) =fact(0,!)(!=1) Ebbôl a célklózok:
fact(0,!):- és :-!=1. A fact(0,!):- nem a megszokott célklóz. Ahoz hogy rezolválni lehessen kell az only if rész.
A definíció only if része
xy(fact(x,y)[x=0y=1]x'y'[x=x'+1fact(x',y')y=x*y']=
xy(fact(x,y)[x=0y=1]x'y'[x=x'+1fact(x',y')y=x*y']=   (Skolemizálás)
xy(fact(x,y){[x=0y=1][x=fx(x,y)+1fact(fx(x,y),fy(x,y))y=x*fy(x,y)]} a{} részre disztr. szab.
xy(fact(x,y){(x=0x=fx(x,y)+1)(x=0fact(fx(x,y),fy(x,y)))(x=0y=x*fy(x,y))
y=1x=fx(x,y)+1)(y=1fact(fx(x,y),fy(x,y)))(y=1y=x*fy(x,y))}  (konj. konkl.)
Az only if rész mint klózok:
x=0x=fx(x,y)+1:-fact(x,y)
x=0fact(fx(x,y),fy(x,y)):-fact(x,y)
x=0y=x*fy(x,y):-fact(x,y)
y=1x=fx(x,y)+1:-fact(x,y)
y=1fact(fx(x,y),fy(x,y)):-fact(x,y)
y=1y=x*fy(x,y):-fact(x,y)
Induljunk ki a negált tétel fact(0,!):- klózából
fact(0,!):-
  y=1x=fx(x,y)+1:-fact(x,y) ---- x/0,y/!

!=10=fx(0,!)+1:-
:-0=u+1  --  u/fx(0,!)

!=1:-
:-!=1   --  a célklózból

Lekérdezés adatbázisból. Ha a kérdésben van univerzális kvantor, akkor  kell az only if rész.
Mivel a logikai program egy partíciója több if-then részdefinícióval adja meg a fej definícióját ahhoz, hogy a definíció only if része megadható legyen a fejben lévő predikátumok argumentumaiba ugyanazokat a változókat vezetjük be és a feltételrészbe korrigáló egyenlőségeket vezetünk be. Ezzel tesszük lehetővé a partíciónak egyetlen if-then definícióvá alakítását, amelyből az only if rész felírható. Ezt a folyamatot azaz a logikai program kiegészítését az only if résszel programkiegészítésnek nevezzük.
A logikai program 		A partíció fejét közös alakra hozzuk. 
tanít(A,104).			tanít(X,Y):-X=A,Y=104
tanít(A,301). 			tanít(X,Y):-X=A,Y=301
tanít(B,221).			tanít(X,Y):-X=B,Y=221
tanít(C,105). 			tanít(X,Y):-X=C,Y=105
tanít(C,201).			tanít(X,Y):-X=C,Y=201

tanár(A).				tanár(X):- X=A
tanár(B).				tanár(X):- X=B
isa(104,programozás).
isa(221,programozás).

A kiegészített program: comp(P)

tanít(x,y)[x=Ay=104][x=Ay=301]
			  [x=By=221][x=Cy=105]	
			  [x=Cy=201]

tanár(x)x=Ax=B

Legyen a kérdés: Tanít-e minden tanár programozást
xy(tanár(x)tanít(x,y)isa(y,programozás)) ? A tételből nem a megszokott PROLOG célklóz áll elő.

( xy(tanár(x)tanít(x,y)isa(y,programozás))) =
xy(tanár(x)tanít(x,y)isa(y,programozás))=
y(tanár(f(y))(tanít(f(y),y)is a(y,programozás))) ez  a tételformula  negáltja skolemizálva, 
mivel a :- utáni formula elé a negáció jele odaértendő ezért a
 :-  tanár(f(y))(tanít(f(y),y)is a(y,programozás) írható ez lényegében a tétel magja 

A célklóz B1...Bs alakban kellene de diszjunkciós alakú, ezért két “célklózhoz jutunk”
:- tanár(f(y))		ez negált literál
:- tanít(f(y),y)), is a(y,programozás)). 
A válaszhoz szükség van a tanár és a tanít reláció only if részére.
Látjuk, hogy a   tanár(f(y)) literál szerepel ezért a
 tanár(x)  x=Ax=B mellett a 
 tanár(x) x=Ax=B-ra is szükség van

Ezekben az esetekben a lineáris input rezolúció, azaz a PROLOGban használt algoritmus nem használnató.
Az eredeti algoritmusra épülő compilereket ezért bővítik az újabb problémákat megoldani képes részekkel.
Hogy lássák a PROLOG képességeit és az új problémák logikai hátterét következésképpen logikai megoldásuk lehetőségét a PROLOG nyelv szemantikáját kell vizsgálni.

A PROLOG nyelv értelmezése.
Deklaratív szemantika:
Egy P logikai program egy elsőrendű logikai nyelven írt speciális formulahalmaz (Horn klózok)
A célklóz a T tétel negáltja.
A kérdés, hogy T a P következményei között van-e.
Vagyis ha M a P modellje, akkor M a T-nek is modellje-e.
Igaz-e hogy {PT}-nek nincs modellje
Az M modell mindig Herbrand modell. Herbrand univerzum HI, Herbrand bázisBP. M BP.
Feladat olyan algoritmus keresése, hogy ami deklaratív szemantika szerint megoldható, az az eljárás szintjén, sőt a megvalósítás szintjén is megoldható legyen.

Procedúrális szemantika.
{PT}-nek van-e definit klózokon alapuló, egy “jó” szelekciós stratégiát alkalmazó, lineáris input (SLD) rezolúciós cáfolata.

Kiszámítási szemantika.
{PT}-nek van-e (SLD) lineáris input rezolúciós cáfolata a konkrét megszorító stratégia mellett.
Egy ilyen stratégia a partíció felírási sorrenben való feldolgozása és 
a célklóz literáljainak rögzített sorrendben való feldolgozása. (A partíció klózainak sorrendjére a program írásánál figyelni kell.)

Példa a fenti stratégia hiányosságára
Logikai program			1. stratégia - a balról első
1. p(x,z):-q(x,y),p(y,z).		literál feldolgozása.
2. p(x,x).
3. q(a,b).				:-p(x,b).
A cél: :-p(x,b).			1		         2
				:-q(x,y),p(y,b)		
				3    (z/b)			(x/b)
				:-p(b,b)		siker
				1	      2
			:-q(b,u),p(u,b)		
			kudarc			(x/b)
						siker

2. stratégia - a jobbról első literál feldolgozása.

					:-p(x,b).
				1			2
			:-q(x,y),p(y,b)			
			1		2		(x/b), siker
	:-q(x,y),q(y,u), p(u,b)		:-q(x,b),			
	1		2			3
:-q(x,y),q(y,u),q(u,v), p(u,b)     :-q(x,y),q(y,b)	
	1			3		(x/a), siker
végtelen				:-q(x,a)		
				kudarc

A teljes levezetési fának a bal szélső ágán lévő levezetésből nem tud kilépni, nem tudja előállítani az összes levezetést.
Ami definit Horn klózokkal formalizálható, az PROLOG nyelven leírható. Az SLD –vel (“jó” S esetén, amikor a teljes levezetési fa bejárható) a levezetési fa alapján szintaktikus tulajdonságokat rendelhetünk a gyökérben lévő klózhoz, a levezetési fához.
A levezetési fa és a fában kapott speciális ágak, levelek.
	Végtelen levezetési fa. (van végtelen ága)
	Végtelen ág = kudarc ? vagy nem biztos a kudarc.
	Kudarc ág  = véges lépésben kiderül a kudarc.
	Kudarc fa = minden ága kudarc ág. (a célklóz kudarcos)
	Sikeres ág  =   levezetése (mindig véges)

Siker halmaz: { A BP :A levezetési fájában van sikeres ág}
Véges kudarc halmaz:	{ A BP :A levezetési fájában minden ág végesen kudarcos}

 Legszűkebb Herbrand modell  (Lloyd) (egy H interpretáció a H. bázis egy részhalmaza – az igaz alapatomok halmaza.)
Egy logikai program mindig kielégíthető.
a) A P program legszűkebb Herbrand modellje a BP azon alapatomjainak MP halmaza, amelyekből akár egyet is elhagyva a kapott alapatomhalmaz már nem modellje P-nek.
6.1. Tétel. Ha MiiI P Herbrand modelljeinek egy halmaza, akkor  iI Mi is Herbrand modellje P-nek.
6.2. Tétel. Legyen P a program. Ekkor MP =A BP :A logikai következménye  P-nek.
Bizonyítás. 
Az A alapatom logikai következménye  P-nek 
akkor és csak akkor, ha P A kielégíthetetlen 
akkor és csak akkor, ha P A-nak nincs Herbrand modellje
akkor és csak akkor, ha  A wrt hamis P minden Herbrand modelljében
akkor és csak akkor, ha  A wrt igaz P minden Herbrand modelljében 
akkor és csak akkor, ha  AMP.
Példa: A legszűkebb modell, mint az összes alapatom következmény halmaza:
ős(x,y):-szülője(x,y).
ős(x,y):-szülője(x,z), ős(z,y).
szülője(x,y):-gyereke(x,y).
gyereke(x,y):- szülője(x,y).
gyereke(a,b).	a tényklóz
gyereke(b,c).	mindig
gyereke(c,d).	következmény
az összes további következmény:
szülője(a,b).
szülője(b,c).
szülője(c,d).
ős(a,b).
ős(b,c).
ős(c,d).
ős(a,c).
ős(b,d).
ős(a,d).

Az MP algoritmikus előállítását a fixpont fogalom használatával érhetjük el. 
A teljes hálók rendezéstartó leképezései rendelkeznek fixpontokkal. 
Egy részben rendezett  halmaz H-t akor nevezünk teljesnek, ha bármely XH ra X alsó és felső határa létezik és ezek elemei H.nak.

Rendeljünk minden P logikai programhoz egy teljes hálót.
Legyen P a program. A BP. hatványhalmaza P(BP)  (2BP)  adja P összes Herbrand interpretációját. Ez tejes háló a  rendezésre nézve. A legkisebb eleme a , a legnagyobb eleme BP. Herbrand interpretációk egy halmazának legkisebb felső korlátja (felső határ)  e halmaz elemeinek uniója és a legnagyobb alsó korlátja (alsó határ) e halmaz elemeinek metszete.
Definíció. Legyen L egy teljes háló értelmezési tartománya és XL. Az X-et irányítottnak nevezzük, ha X minden véges részhalmazának van X-ben felső korlátja.
A közvetlen következmény függvény.
Def. Legyen P egy program. A TP =P(BP) P(BP)   leképezés a következő. Legyen I egy  Herbrand interpretáció. 
TP (I)=A BP:A1,...,AkA - alapelőfordulása egy P-beli klóznak ésA1,...,AkI.
Példa. Legyen a P program:
p(f(x)):-p(x).
q(a):-p(x).
I1 =BP, I2 = TP ( I1 ), I3=.
TP ( I1 )= q(a )p(f(t)): t UP
TP ( I2 )= q(a )p(f(f(t))): t UP 
TP (I3) =.  Nincs alapatom következmény. :-q(a),p(x) következménye comp(P)-nek.

Definíció
TPn és TP n operációk TP -n, ahol
TP0= 			 TP 0=BP
TPn= TP (TP(n-1))		 TP n=TP(TP (n-1))	ha n rákövetkező rendszám
glb(TPk), (k<n)			lub(TP k), (k<n)		ha határérték rendszám
glb - legnagyobb alsó korlát	lub - legkisebb felső korlát.
Az az n amelyre fixpontot kapunk a lezárási rendszám. A TP-ra ez .
Az azonban lehetséges, hogy gfp(TP)  TP .
Példák.									
1. Legyen a P program:
p(f(x)):-p(x).
q(a):-p(x).
Mutassuk meg, hogy TP  =.q(a), azonban gfp(TP) = . Viszont gfp(TP) = TP (+1).
2. Legyen a P program:
p(a):-p(x),q(x).
p(f(x)):-p(x).
q(b).
q(f(x)):-q(x).
Mutassuk meg, hogy TP  =.p(fn(a))| n}{q(fn(b))| n} és a gfp(TP)= TP 2 =. gfp(TP)= TP.=  q(fn(b))| n}
3. Legyen a P program
q(b).
q(f(x)):-q(x).
p(f(x)):-p(x).
p(a):-p(x).
r(c):-r(x),q(x).
r(f(x)):-r(x).
Mutassuk meg, hogy TP.=  q(fn(b))| n}.
TP  =.p(fn(a))| n}{q(fn(b))| n} {r(fn(c))| n} és a gfp(TP)= TP 2 =. gfp(TP)

6.5.Tétel. Legyen P egy program. Ekkor MP = lfp(TP)= TP.
6.3. Tétel. Legyen P egy program.  Ekkor a TP  leképezés folytonos és ezért monoton.
Biz. Legyen X egy irányított részhalmaza P(BP)-nek. Jegyezzük meg, hogy A1,...,Ak  lub(X) akkor és csak akkor, ha 
A1,...,Ak I, bizonyos IX-re.  A TP  leképezés folytonosságának belátásához meg kell mutatni, hogy TP (lub(X))=lub(TP (X)) minden irányított X részhalmazra. A következők állnak fenn:
A TP (lub(X))
akkor és csak akkor, ha  A1,...,AkA - alapelőfordulása egy P-beli klóznak  és A1,...,Ak lub(X), 
akkor és csak akkor, ha  A1,...,AkA - alapelőfordulása egy P-beli klóznak  és A1,...,Ak I, valamely IX-re.
akkor és csak akkor, ha  A TP (I) valamely IX-re.
akkor és csak akkor, ha A lub(TP (X)).
A TP -vel lehet jellemezni azokat a Herbrand interpretációkat, amelyek modelljei P-nek.
6.4.Tétel. Legyen P egy program és I egy Herbrand interpretációja P-nek. I modellje P-nek akkor és csak akkor, ha TP (I)I.
Biz. I modellje P-nek akkor és csak akkor, ha a P program minden klóza minden A1,...,AkA - alapelőfordulása esetén A1,...,AkI esetén AI akkor és csak akkor, ha TP (I) I gy P-beli klóznak .
6.5.Tétel. Legyen P egy program. Ekkor MP = lfp(TP)= TP.
Biz. MP =glbI: I a P egy Herbrand modellje
	=glbI: TP (I)I, a  6.4. tétel miatt
	=lfp(TP), az 5.1. tétel miatt
	= TP, az 5.4. és a 6.3. tételek miatt.

A logikai program szemantikai és szintaktikai tulajdonságainak kapcsolata.
Belátható, hogy P siker halmaza=Tp
Belátható, hogy P kudarc halmaza= BP\Tp.
Def. P egy definit program, dFP  a d lépésben kudarcos A alapatomok halmaza. Részletezve:
a)	A 1FP ha A Tp 1. (Azok az alapatomok, amelyek nem közvetlen következményei BP -nek.
b)	A dFP ahol d>1, ha minden olyan B:- B1,...,Bm klózra és minden olyan  alaphelyettesítésre, ahol A= B és  1km-re Bk d-1FP .
Def. P egy definit program. P véges kudarc halmaza  FP=d1 dFP.
13.1 Tétel. P egy definit program, akkor FP = BP\Tp.
13.4 Tétel. P egy definit program és ABp. Ha P{:-A} levezetési fája végesen kudarcos, ahol a mélység k, akkor ATpk.
13.5 Tétel. P egy definit program és :- A1,...,Am egy definit cél. Ha a célnak a 1, 2 ... alaphelyettesítések mellett nincs véges kudarcos  levezetési fája, akkor adott k-hoz létezik n, hogy 
[Ai 1, 2.... n ] Tpk.
13.6 Tétel. P egy definit program és ABp. A következők ekvivalensek:
a)	AFp
b)	A Tp .
c)	A a véges kudarc halmaz eleme.
d)	P{:-A} minden fair levezetési fája végesen kudarcos.

 Negáció kezelése
:-A jelentése  A, de ha a tétel A, akkor  :- A lenne a célklóz ami szintaktikailag helytelen.
Az MP és a véges kudarc halmaz ismerete alapján a negáció kezelésével ki lehetett bővíteni a logikai programozást.
Hogyan értelmezzük A-t mint a P következményét.
1.Zárt világ feltételezés (closed world assumption CWA). 
Ha  egy  A  alapatom nem logikai következménye egy programnak, akkor a A bizonyítottnak  tekintendő.  azaz
Ha A minden alappéldánya eleme minden M -nek, akkor A nem következmény azaz 
Ha A minden alappéldánya eleme MP -nek, akkor A nem következmény
Például legyen a program a következő
   tanuló(János).
   tanuló(Béla).
   tanuló(Jóska).
   tanár(Mária).

Tegyük fel, hogy azt szeretnénk belátni, hogy Mária nem tanuló , vagyis azt, hogy (tanuló(Mária).A fentiek szerint  a  logikai programnak  a  (tanuló(Mária) nem  következménye.  De  a logikai programnak a tanuló(Mária) sem következménye. Az ilyen esetek kezelésére egy speciális levezetési  szabályt  vezetünk be:  Ha  egy  A  alapatom nem   logikai következménye egy programnak, akkor a  (A  bizonyítottnak  tekintendő.  Ezt  a 
hozzáállást hívják zárt világ feltételezésnek  (closed world assumption CWA). Ezzel a levezetési szabállyal már le tudjuk vezetni azt,  hogy (tanuló(Mária), .mivel a programnak a tanuló(Mária) nem logikai következménye.
Adatbázis környezetben a CWA szabály természetes, mivel azt az információt, ami nincs benne  az  adatbázisban  nem  tekintjük igaznak. A deduktív adatbázisokban a szabályok jelenléte miatt az  adatbázisból  levezethető összes  dolgok halmazát nem lehet egyszerűen meghatározni. A  CWA  használata  általában természetes, de nem mindig megfelelő. A megoldás módja, hogy elő kell állítani a program legszűkebb modelljét MP = lfp(TP)= TP-t és megvizsgálni, hogy az A eleme-e. Ha A nem eleme Mp akkor (A a program kovetkezménye. Egy  levezetési   szabály   nem   monoton,   ha   új   axiómák bevezetésével egyes korábban bebizonyítok tételek hamissá válnak. Például, ha a fenti programhoz hozzáveszünk tanuló(Mária):- tényklózt, akkor a CWA-val már  le  lehet  vezetni  azt,  hogy tanuló(Mária). Mint az ismert Mp= P siker halmaza, ezért véges lépésben bármely A-ról el lehet dönteni, hogy elemeüe Mp-nek, bár erre az elsőrendű  logika   eldönthetetlensége  miatt  nincs általános algoritmus. 

2. A negáció mint kudarc szabály.(Negation as failure)
Ha  egy A  alapatom végesen kudarcos, akkor a A következménye a P programnak
Ha AFp, akkor A következménye a P programnak.
Az SLD rezolúció kiterjesztése SLDNF rezolúcióvá. A a negált cél feldolgozásánál felépíti a cél SLD fáját, ha az végesen kudarcos, akkor a negált cél sikeres, a következő részcéllal folytatódik a levezetés.
Példa: 
tanuló(János).
   tanuló(Béla).
   tanuló(Jóska).
   tanár(Mária).
Kérdés: (tanuló(Mária). A célklóz :- (tanuló(Mária), azaz tanuló(Mária).

:-(tanuló(Mária).----------:-tanuló(Mária).
			tanuló(János).	tanuló(Béla).	tanuló(Jóska).

			kudarc		kudarc		kudarc
	siker

A “tanuló(Mária)” eleme a véges kudarc halmaznak, tehát igaz, hogy Mária nem tanuló.

1. háziállat(x):-kicsi(x), kutya(x).
2. háziállat(x):-cica(x)
3. kicsi(a).
4. pók(a)
Igaz-e, hogy az a nem háziállat 
Célklóz:  :- ( háziállat(a)), azaz háziállat(a).

:- ( háziállat(a)). ------------:  :- háziállat(a).
			1			2
		:- kicsi(a), kutya(a).		:-cica(x).
			3			kudarc
			:- kutya(a).
			kudarc
	siker

A “háziállat(a)” eleme a véges kudarc halmaznak, tehát igaz, hogy az a nem háziállat.

3. Programkiegészítés és Herbrand szabály. (comp(P) és Herbrand szabály)
Def. Herbrand szabály: ha comp(P)A-nak nincs Herbrand modellje, akkor A következménye a P programnak.

				Bp					A levezetése a
									negáció mint kudarc szabállyal

				Tp .

									A levezetése
				gfp(Tp)					Herbrand szabállyal

				Tp					A levezetése
									zárt világ feltételezés
									(CWA) szabállyal

14.6. Tétel. Legyen P egy definit program és G egy definit cél és  válaszhelyettesítés P{G}re.   korrekt válasz comp(P){G}-re akkor és csak akkor ha  korrekt válasz P{G}-re.

Negációkezelés rétegzéssel.

Def. Normál program  programklózai  A:-L1,...,Ln alakúak, ahol  A atom és L1,...,Ln literálok.
Minden P normál program konzisztens, de comp(P) lehet, hogy nem. Megadunk egy elégséges gyenge szintaktikus feltételt arra, hogy comp(P) konzisztens legyen
Def. Egy normál program szint leképezése a program predikátum szimbólumainak a nem negatív egész számokra való leképezése. A perdikátum szimbólum szintje a hozzárendelt egész szám.
Def. Egy normál program hierarchikus, ha van olyan szint leképezése, hogy  minden p(t1,...,tm):- L1,...,Ln progam klózban a törzsben lévő predikátumszimbólumok szintje kisebb, mint p szintje.
Def. Egy normál program rétegzett, ha van olyan szint leképezése, hogy  minden p(t1,...,tm):- L1,...,Ln progam klózban a törzsben lévő pozitív predikátum szimbólumok szintje kisebb vagy egyenlő mint p szintje és a törzsben lévő negatív predikátum szimbólumok szintje kisebb mint p szintje.
Megjegyzés. Minden definit és minden hierarchikus program egyben rétegzett is.
Megjegyzés. Normál programok esetén TP nem monoton . Rétegzett P-re olyan tulajdonságai vannak TP -nek, amelyek biztosítják hogy comp(P)-nek van minimális Herbrand modellje.
Példa rétegzett programra.
q:-r.
r:-p.
r:-p.
p:-p.
Algoritmus a rétegzés megkeresésére.
1. Minden predikátumhoz az 1 számot rendeljük.
2. Minden negált részcélt tartalmazó programklózban, a fej rétegszámát 1-el megemeljük a negált részcéléhoz képest. Ha nem kellett már átszámozni, akkor vége. A program rétegzett.
3. Az uj rétegszámokat átvezetjük és folytatás a 2-vel.
Hajtsuk végre az algoritmust a fenti példára. A szinszámokat a predikátumok elé írjuk.
	1	   2		   3		   2		  3 nincs változás.
1q:-1r.		2q:-1r.		2q:-2r.		3q:-2r.		3q:-2r.
1r:-1p.		1r:-1p.		2r:-1p.		2r:-1p.		2r:-1p.
1r:-1p.		2r:-1p.		2r:-1p.		2r:-1p.		2r:-1p.
1p:-1p.		1p:-1p.		1p:-1p.		1p:-1p.		1p:-1p.

1	p	p	
2	r	r	
3	q		

A lényeg az, hogy a program képes definiálni egy predikátumot mielőtt az a programklóz sorrakerülne amelynek a törzsében az illető predikátum negáltja szerepel.
Válasz helyettesítések
Ismert fogalmak: illesztő (egységesítő) helyettesítés  (mgu;  most general unifier), legáltalánosabb illesztő (egységesítő) helyettesítést kiszámító algoritmus.
Az E és F kifejezések variánsok, ha léteznek olyan  és   helyettesítések, hogy E=F és F=E.
Speciális helyettesítés az átnevező helyettesítés x1/y1,...,xn/yn, ahol x1,...,xnV az yi-különbözőek és  (V\x1,...,xn)y1,...,yn=.
Def. Legyen P egy program és G a cél. Egy válasz helyettesítés PG-re a G változóira vonatkozó  helyettesítés.
Megjegyzés. Nem kötelező, hogy  a helyettesítés  G minden változójára vonatkozzon. Speciálisan, ha G nem tartalmaz változókat, akkor az egyetlen lehetséges válasz helyettesítés az identikus helyettesítés.
Def. Legyen P egy program és  G a cél (:-A1,...,Ak) és  egy válasz helyettesítés PG-re. Azt mondjuk, hogy  korrekt válasz helyettesítés PG-re, ha (A1...Ak) logikai következménye P-nek.
A 3.1 tétel szerint  korrekt válasz helyettesítés PG-re, akkor és csak akkor, ha  P(A1...Ak) kielégíthetetlen.
Ez a korrekt válaszhelyettesítés fogalom egy modellelméleti intuitív fogalom. Egyszerűen  egy P program és egy G cél esetén elvárható output deklaratív definíciója. Természetesen  ennek a fogalomnak nézzük a procedúrális megfelelőjét is, amelyet a rendszer cáfoló eljárása (algoritmusa) alapján definiálunk.
 nem korrekt válasz helyettesítés PG-re, ha a levezető rendszer  nemmel válaszol. Azt mondhatjuk. hogy a  nem válasz korrekt, ha PG kielégíthető.

Megj. A 6.2. tétel és a korrekt válaszhelyettesítés definíciója alapján azt lehet remélni, hogy  a 6.2. tétel élesíthető úgy, hogy egy  válaszhelyettesítés korrekt akkor és csak akkor, ha (A1...Ak) wrt igaz a P leszűkebb Herbrand modelljében. Sajnos ez ebben az általános formában nem áll fenn. 
Példa. Legyen a P program:
p(a):-
A cél legyen :-p(x),   pedig az identikus helyettesítés. MP =p(a) és így xp(x) igaz MP -ben. Azonban  nem korrekt válaszhelyettesítés, mivel  xp(x) nem logikai következménye P-nek.
Az ok az, hogy xp(x) nem klóz és így nem lehet csak a Herbrand interpretációkat tekinteni akkor, amikor a p(a) xp(x)  kielégíthetetlenségét vizsgáljuk. Azonban, ha a -ra korlátozást vezetünk be, akkor a 6.2. tételt általánosító eredményhez juthatunk.
6.6. Tétel. Legyen P egy program és :-A1,...,Ak  a G cél. Tegyük fel, hogy  válasz helyettesítés a PG-re, de úgy, hogy (A1...Ak )  alapkifejezés. Ekkor a következők ekvivalensek:
(a)  korrekt
(b) (A1...Ak ) wrt igaz P minden Herbrand modelljében
(c) (A1...Ak ) wrt igaz P legszűkebb Herbrand modelljében.
Biz. Elég azt bizonyítani, hogy (c) implikálja (a)-t. Tehát
(A1...Ak ) wrt igaz P legszűkebb Herbrand modelljében
implikálja, hogy  (A1...Ak ) wrt igaz P minden Herbrand modelljében
implikálja, hogy  (A1...Ak ) wrt hamis P minden Herbrand modelljében
implikálja, hogy P(A1...Ak ) -nek nincs Herbrand modellje
implikálja, hogy P(A1...Ak ) -nek nincs  modellje.
Feladatok megoldása a Lloyd könyvből.

Néhány feladat
Útkeresés gráfban.
út(x,y):-él(x,y).
út(x,y):-él(x,z),út(z,y).
él(a,b):-					a			b
él(a,d):-					
él(d,c):-					
él(b,a):-					d			c

cél: :-út(a,c)

Ha az adatokat adjuk meg listával. [a-b, a-d, d-c, b-a ], A – egy operátor.
Hogy kell módosítani a programot? Lehet-e így választ kapni?

Példák programkiegészítésre.
szülôje(x,y):-anyja(x,y)
szülôje(x,y):-apja(x,y)
anyja(x,y)apja(x,y)szülôje(x,y)
anyja(x,y)apja(x,y):- szülôje(x,y)

Példák legszűkebb modell keresésre
A logikai program		
1. p(x,z):-q(x,y),p(y,z).	
2. p(x,x).
3. q(a,b).
Herbrand univerzum : {a,b}
Legszűkebb Herbrand modell: { q(a,b), p(h,h), p(a,b) } ={ q(a,b), p(a,a), p(b,b), p(a,b) }
a cél: :-p(x,b).

Legyen a P program:
p(f(x)):-p(x).
q(a):-p(x).
Herbrand univerzum : {a, f(a), f(f(a)),...}
Legszűkebb Herbrand modell: üres, nincs alapatom következmény.

Legyen a P program:
p(x):-q(y),r(y).
q(h(y)):-q(y).
r(g(y)).
Adjon meg  két SLD levezetési fát a P{:-p(a)}-ra. Az egyik legyen végesen kudarcos, a másik legyen végtelen.

Keresse meg az alábbi programok rétegzését:
1.
q:-r.
r:-p.
r:-p.
p:-p.
Változtat-e a rétegzésen, ha :-q a cél. Mi a program következménye q vagy q?
Mi lesz a comp(P)
________________
2.
p:-r.
p:-p.
g:-s, p.
Mi lesz a comp(P)
_________________
3. 
r:-p.
r:- p.
p:-p.
Mi lesz a comp(P)
_____________________
4.
p:-q(x).
q(a).
Mutassa meg, hogy p nem logikai következménye  comp(P)-nek
_________________________________________________________
5.
p:-r.
r:-q(x).
q(a).
Mutassa meg, hogy p logikai következménye  comp(P)-nek. Avagy p eleme a véges kudarc halmaznak.
Bizonyítani a {K1,K2} =0 K -t.
Mutatni lineáris, lineáris input levezetést.
Szerkeszteni teljes levezetési fákat különböző klózokhoz.
Őskeresés levezetési fában.
Átírás prenex, Skolem formába. Kvantor ki- és bevitel.
Egyszerű PROLOG programok írása, kézi futtatása
Illesztő helyettesítés keresésére példa.
Rezolúciós levezetésre példa.

1. Mutassa meg 1 rendű rezolúcióval,  az alábbi  formulákról, hogy
	a) 	xP(x)xQ(x)xP(x) logikailag igaz 
	b)	x(P(x)Q(x))xP(x) logikailag igaz 
Megoldás:  ( xP(x)xQ(x)xP(x)) = (( x(P(x)Q(x))xP(x)) = x(P(x)Q(x))xP(x) = 
x(P(x)Q(x))x P(x) = xy(P(x)Q(x) P(y)). y-ra f(x) Skolem függvény.
A klózok: xP(x), yQ(y), zP(f(z))
Herbrand univerzum: {a, f(a), f(f(a)), ...}	x/f(z) illesztéssel P(x), P(f(z)),  rezolúciós levezetés.

2. Igazolja az X= x(P(x)Q(x))[xP(x) xQ(x)] formula érvényeségét 1 rendű rezolúcióval
Megoldás: (x(P(x)Q(x)) [xP(x) xQ(x)]) = x(P(x)Q(x)) [xP(x) xQ(x)] = 
x(P(x)Q(x)) [xP(x) xQ(x)] = x(P(x)Q(x)) xP(x) xQ(x) =
xy(P(x)Q(x) P(y) Q(y)) = y(P(a)Qa) P(y) Q(y))		a       Skolem konstans
y/a illesztéssel 	P(y), P(a) Q(a), Q(a), Q(y), 

3. A {P(a), xP(x)} formulahalmazról mutassa meg, hogy Herbrand univerzumon kielégíthetetlen, de általában kielégíthető. Mi ennek az oka?
Megoldás:
Herbrand univerzum: {a} P(a) nem lehet egyszerre igaz és hamis is.

4. F={x(P(x) y(D(y) L(x,y))),  x(P(x) y(Q(y) L(x,y)))}
	T=  x(D(x) Q(x))
Mutassa meg 1 rendű rezolúcióval, hogy T logikai következménye F-nek
Megoldás:  T és F-ből a klózhalmaz
x( (P(x) y(D(y)) L(x,y))), x(P(x) y(Q(y) L(x,y))),  T=  x(D(x)Q(x))
x y (P(x) (D(y)) L(x,y))), xy (P(x) Q(y) L(x,y))	,	x(D(x)Q(x))
y (P(a) (D(y)L(a,y))),
A klózok:
y (P(a), y(D(y) L(a,y)),
xy (P(x) Q(y) L(x,y))
x(D(x), xQ(x)
____________________________________
A sorrend és a cut hatása.
Mutassuk meg, hogy az egyes logikai programok jelentése a következő:
A program	a jelentése
p:-a,b.
p:-c.		(ab)cp

p:-a,!,b
p:-c		(ab)(ac)p

p:-c.
p:- a,!,b		c(ab)p