Logikai alapok a programozáshoz (bővített óravázlat)
BSc a és b szakirány.
2005, szeptember.

Tankönyv: Pásztorné Varga Katalin, Várterész Magda: A matematikai logika alkalmazásszemléletű tárgyalása. PANEM Kiadó Budapest, 2003

Aki még a jegyzetből tanul, annak ugyanez az anyag a jegyzetbeli jelölésekkel a 
http://people.inf.elte.hu/OVAZL203.rtf
címen található.
 
1. óra 
Általános bevezetés. 
	A gondolkodás fontos része a mindennapi életnek.
	A gondolkodás fontos része bármely (humán vagy természet) tudománynak
A logika tárgya, célkitűzése.
	Gondolkodási folyamatok vizsgálata
	A helyes következtetés, definiálása.
	A helyes következtetés törvényeinek feltárása.

KÖVETKEZTETÉS - (ekvivalens megfogalmazások)

Adott ismeretek	 új ismeret
premisszák	 konklúzió
feltételek	 következmény
állítások		 állítás
A   jel a gondolkodási folyamatot jelöli, amelyet esetleg 
	valamilyen nyelven leírva ismertethetünk

Helyes a következtetés ha: 
a következmény biztosan igaz, ha a premisszák igazak, vagy 
ha a feltételek igazak a következmény is igaz, vagy
helytálló ismeretekből kialakított új ismeret is helytálló.  
Az eredmény nem szubjektív, csak a premisszákban szereplő állítások igazságértéke befolyásolja (azok nyelvi jelentése nem).

Példa (csak a logikai összekötőjelek értelmén alapuló következtetésre)

Ha nálam van a kapukulcs, akkor ki tudom nyitni a kaput.
Nálam van a kapukulcs		(tehát)
Ki tudom nyitni a kaput.

Egy másik ugyanilyen szerkezetű következtetés:
Ha van itthon kávé, akkor tudok főzni egy jó kávét.
Van itthon kávé		(tehát)
Tudok főzni egy jó kávét.

Vagy
Minden ember halandó.
János ember.         (tehát)
János halandó  

A következtetések közös sémája:
Ha A, akkor B.
A		(tehát)
B

Itt A és B állításokat jelölnek.
Az állítás és az állítások közötti kapcsolatok a logika alapját képezik.
Az állítás fogalma, igazságértéke. Hogyan lehet az állítás igazságértékét megállapítani. 
Az állítás egy olyan kijelentés, amelyről el lehet dönteni, hogy igaz-e vagy nem.
Azt, hogy egy állítás igaz (i) vagy hamis (h) az állítás igazságértékének nevezzük.
Az igazságértékek. Kettőnél több igazságérték lehetősége.

Klasszikus kétértékű logikában két igazságértéket használunk.

Posztulátumok:
Ellentmondástalanság (ellentmondás) elve:egyetlen állítás sem lehet igaz is és hamis is.
Kizárt harmadik elve:	nincs olyan állítás, amely sem nem igaz sem nem hamis.
Az állítás igazságértékét vagy tapasztalati tények, vagy a tudományos eredmények ismeretében állapítjuk meg.

Példák állítások leírására.
Egyszerű állítások (konkrét indivíduum(ok)ról konkrét állítás).      

Kijelentő mondattal.		Mondat funktorral		logikai függvénnyel
Anna most írja a leckéjét.	…	most írja a leckéjét 		IR(Anna,lecke)
Hófehérke mesehős		…mesehős			MH(Hófehérke)
A 9 összetett szám.		… összetett szám			összetett szám(9)
Péter dohányzik.			… dohányzik			dohányzik(Péter)
Juci iskolában van most.		… iskolában van most		iskolában van most(Juci)
Jeanne d’Arc máglyahalált halt.		stb.

NEM LOGIKAI alkotóelemek az állítások leírására:
KIJELENTŐ MONDAT
	NÉV		+		ÁLLíTÁS (FUNKTOR)
Tulajdonnév
1 sz. személyes névmások (én, te, ő, ez)
Indivíduum leírás:  Pista sógora		mikor valóban leírás??? Egyértelműség!

Állítások az általánosító állítások is (nem egy indivíduumról, hanem egy halmazról szólnak)
Általánosító állítások 		értelmezési tartomány
Minden cica szeret fára mászni. 		{cicák}		    x F(x), 	(F(x)=i, ha x szeret fára mászni
Van olyan hallgató, aki szereti a logikát. {egyetemi hallgatók}    xL(x), 	(L(x)=i, ha x szereti a logikát.
ahol x befutja az értelmezési tartományt / univerzumot/ indivíduumhalmazt

NEM ÁLLÍTÁS egy kijelentés, ha
-- a kijelenető mondat alanya okoz problémát azaz
		nem létező indivíduumról állít valamit:
Az amerikai király felesége 2000 május 5-én az operában volt Pesten.
Az orosz cár tegnap elutazott Moszkvából.   stb.

		Az indivíduum meghatározása (leírása) nem egyértelmű.
A sógorom ma reggel hívott telefonon. (Amennyiben egynél több a sógorok száma.)
-- a kijelenető mondatbeli állítás okoz problémát azaz
		ha az indivíduumról szóló állítás nem egyértelmű:
Anna elég jól úszik.
Zoltán még nem öreg.  stb.

Egy logikai függvénykapcsolattal leírt kijelentés, ahol a logikai függvénykapcsolat argumentumában változó is szerepel. Pl. x<5. Paraméteres állítás.

		ha a kijelentés jövőidejű:
Holnap fagylaltozni fogok.
Jövő vasárnap kirándulni megyek.
		A paradoxonok: ha a mondat ugyan állít valamit, de bizonyos kiegészítő ismeretek miatt 
		nem dönthető el, hogy igaz-e vagy nem.
Egy krétai lakos kijelenti: “Minden krétai hazudik”.
Tegyük fel, hogy a “Minden krétai hazudik” állítás igaz. Tehát a krétaink igazat mondott, 
vagyis a “Minden krétai hazudik”állítás (mivel azt egy krétai mondta) nem igaz.
Tegyük fel, hogy a “Minden krétai hazudik”állítás nem igaz. Tehát a krétaink hazudott , 
vagyis a “Nem minden krétai hazudik”.állításnak igaznak kellene lennie. Erre viszont 
nincs bizonyíték, mivel az egyetlen ismert krétai hazudott. Lehet, hogy valóban 
minden krétai hazudik. De akkor a fenti állítás igaz lenne. Azaz a krétaink igazat mondott volna...
Összetett állítások. – állítást jelentő összetett mondatok, amelyeket olyan kötőszavak kötnek össze, amelyek ezt biztosítják.
Logikai összekötőjelek és a logikai műveletek.

A lehetséges kétváltozós logikai műveletek közös igazságtáblája.
		1	2	3	4	5	6	7	8	9	10	11	12	13	14	15	16	
X	Y	XY	XY	XY	XY							X	Y	X	Y	i	h	
i	i	i	i	i	i	h	h	h	h	h	i	h	h	i	i	i	h	
i	h	h	i	h	h	i	i	h	i	h	i	h	i	i	h	i	h	
h	i	h	i	i	h	i	i	h	h	i	h	i	h	h	i	i	h	
h	h	h	h	i	i	h	i	i	h	h	i	i	i	h	h	i	h	

Az összetett állításokat egyszerü állítások logikai összekötőjelekkel való összekapcsolásaként állítjuk elő. Biztosítani kell, hogy az összetett állítás igazságértéke csak a benne szereplő egyszerű állítások igazságértékétől függjön. Ez azt jelenti, hogy a logikai összekötőjelek csak logikai műveletek lehetnek. Az egy és kétváltozós logikai műveletek közül erre a célra a következőket válasszuk ki.
Logikai műveletek és logikai összekötőjelek megfeleltetése a nyelvtani összekötőkkel
negáció			“nem”, “nem igaz, hogy”
konjunkció			“és”,. “de”, “mégis”, “annak ellenére, hogy”
diszjunkció			“vagy”, (megengedő értelemben) [1], “de legalábbis”
implikáció			kb. “ha...., akkor ....” (ez a kondicionális fogalom pld.: 
				Nem igaz, hogy Mari korán kel és nem éri el a buszt =
				Ha Mari korán kel, akkor eléri a buszt.
ekvivalencia			“ ... akkor és csak akkor ...”

A logikai nyelv.
Nyelv = ABC+szintaxis+szemantika.
Természetes nyelvek esetén:
ABC: - A nyelvben használt betűk, a nyelv szavai és az elválasztójelek.
Szintaxis: - A különbözű mondatfajták szerkesztési szabályai.
Szemantika: Az a mód, ahogy a mondatokhoz a jelentésüket hozzárendeljük.

Minden tudományághoz tartozik leíró nyelv, ami lehet valamely természetes nyelv kibővítve bizonyos speciális jelekkel.

A logika esetén is szükség van valamilyen leíró  nyelvre.
A logikát leíró -logikai nyelv - feladata az állítások és a köztük lévő kapcsolatok leírása . Az összetett állítások értelmezése. 
A legegyszerűbb logikai nyelv az állítások leírásával nem foglalkozik csak az állítások közötti logikai kapcsolatok törvényszerűségeivel.

A legegyszerűbb logikai nyelv az ítélet- vagy állítás-logika nyelve. A nyelv ABC-je (jelölje V0):
- ítélet- vagy állításváltozók (az állítások szimbolizálására). Esetenként logikai változónak is nevezzük ezeket a változókat. Jelölés: X,Y,Xn...(indexezve is). Itéletváltozók halmazát Vv jelöli.
- logikai összekötőjelek: , , ,  vagy a jegyzetben még , esetleg . 
- elválasztójelek: (  )  

Az ítélet- vagy állítás-logika nyelve.a  ábécé feletti legszűkebb olyan tulajdonságú szóhalmaz, amelynek
1. Vv minden eleme egyuttal szava is.
2. ha S eleme a szóhalmaznak, akkor S is eleme.
3. ha S és T eleme a szóhalmaznak, akkor (ST) is eleme a szóhalmaznak, ahol  tetszőleges binér logikai összekötőjel.
NEM MINDEN SZÓ TARTOZIK A NYELVHEZ

Szintaxis: A nyelvtanilag helyes mondatok szerkesztési  szabályai.
Szemantika: A nyelv mondatainak értelmezése.

Az ítélet- vagy állításlogika szintaxisa:
(A nyelvtanilag helyes mondatok a jól formált formulák (jff).)
1. X ítéletváltozó jff. (prímformula)
2. Ha A, B jff-k, akkor   A,  (AB),  (AB),  (AB),  jff-k.
3.Minden jff az 1,2 véges sokszori alkalmazásával áll elő.
A NYELV MINDEN SZAVA FORMULA.

Szerkezeti indukció elve. (47. o.) L0 minden formulája T tulajdonságú.
(alaplépés) minden prímformula T tulajdonságú.
(indukciós lépés) 
ha A L0 T tulajdonságú, akkor A is T tulajdonságú
Ha A és B L0 T tulajdonságú, akkor AB is T tulajdonságú

Egyértelmű elemzés. (47. o.)
 Minden formulájára pontosan az egyik igaz
- A formula prímformula
- A formula egy egyértelműen meghatározott L0–beli formula negáltja
- A formula az egyértelműen meghatározható A és B formulákból a  logikai művelettel előállított AB formula

Logikai műveletek prioritása. Formulaszerkezet.

Részformula:.Egy formula részformulája a benne előforduló olyan összefüggő jelsorozat, amely maga is ítéletlogikai formula. 

Közvetlen részformula - legszűkebb részformula vagy egy logikai művelet hatáskörébe eső részformula.

Pontos definíció:
1. A prímformulának nincs közvetlen részformulája.
2. A A közvetlen részformulája: A. 
3. Az (AB) közvetlen részformulái az A (baloldali) és a B (jobboldali).
A formulák típusának megállapítása (negációs, diszjunkciós, konjunkciós, implikációs…).

Formula szerkezeti fája.

Zárójelelhagyás. – közvetlen részformulák ebben az esetben. 
 hatásköre tőle jobbra a vele azonos szinten lévő első logikai összekötőjelig lévő részformula.
 kétváltozós logika művelet hatásköre a tőle jobbra és balra az első nála kisebb prioritású logikai összekötőjelig lévő részformula.

Szerkezeti rekurzió elve.  (49. old.)
Pontosan egy az L0-on értelmezett F függvény van, amelynek
(alaplépés) értékeit rögzítjük minden prímformulára és megmondjuk, hogy.
(indukciós lépés) 
- a A-n felvett értéke az A-n felvett értékéből, illetve
- az  (AB)-n felvett értéke az A-n és a B-n felvett értékekből hogyan származtatható.

A B formula logikai összetettségét a szerkezeti rekurzióval definiáljuk. L(B)

1. Ha B prímformula. Akkor L(B)=0.
2. az L(B) legyen L(B)+1.
3. az L(BD) legyen L(B) + L(D)+1.

Megjegyzés: Diszjunkciós, konjunkciós formulalánc - asszociativitás - tetszőleges zárójelezéssel jff alakúvá tehető. Implikációs formulaláncra a jobbról balra zárójelezés konvenció érvényes.
Formalizálás. 
(kb. az 1. óra vége)
Szemantika: Az ítéletlogika nyelvének interpretációja egy I : Vv {i, h} függvény 
(az ítéletváltozók kiértékelése = igazságkiértékelés).
Egy n-változós Q formula változói egy I interpretációban igaz vagy a hamis értéket vehetnek fel, ezekhez a formula helyettesítési értéke hozzárendeli az igaz vagy a hamis értéket. 
Egy formula Boole-értékelése (kiértékelése) egy interpretációban BI (A) (szerkezeti rekurzió).
1. ha A primformula: BI (A) legyen I (A).
2. a BI (A) legyen  BI (A).
3. a BI (AB) legyen BI (A)  BI (B)
4. a BI (AB) legyen BI (A)  BI (B)
5. a BI (AB) legyen BI (A)  BI (B)

Egy Q formula igazságtáblája egy olyan táblázat, ahol a fejlécben a formula ítéletváltozói (prímformulák) valamilyen sorrendben és a Q formula szerepelnek. 
Az igazságtábla soraiban a vátozók alatt lévő értékkombinációk/igazságkiértékelések az ítéletlogika nyelvének I interpretációi. I: Vv{i,h}. A Q formula alatt az I interpretáció sorában a formula helyettesítési értéke BI (Q) szerepel.

Ez azt jelenti, hogy a Q n-változós formula egy {i.h}n {i,h} leképezést ír le.

Az X, Y, Z változósorrend esetén, amit bázisnak is nevezünk ezt felsorolással megadhatjuk. A formula igaz halmaza / hamis halmaza.

Példa
	X	Y	Z	XYZX	
az	i	i	i	i	
ös	i	i	h	h	
sz	i	h	i	h	
es	i	h	h	h	
in	h	i	i	i	
ter	h	i	h	i	
pre	h	h	i	i	
táció	h	h	h	i	
 
Adott bázis esetén az összes interpretáció megadható, szemantikus fával. 
Definíció. Egy n-változós szemantikus fa egy n-szintű bináris fa, ahol a szintek a bázisbeli 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 (I interpretáció) megjelenik.

Szemantikus fa az X, Y, Z logikai változókra, mint bázisra.

				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

Legyen A egy tetszőleges n-változós ítéletlogikai formula. 
Az általa leírt {i.h}n {i,h} leképezés megadása igazságtáblával a gyakorlati alkalmazásokban kivihetetlen. 
Az ítéletlogika szemantikája a felhasználásorientált tárgyalásban Az igazságértékelés. Ez egy rekurzív módszer arra, hogy egy formulához,az igazságtábla felírása nélkül, hozzárendeljük annak jelentését oly módon, hogy megadjuk minden formulafajtára a Ai és a Ah feltételt amelyeknek pontosan azok az interpretációk tesznek eleget amelyekben  I (A) igaz, illetve hamis. 
A -igazságértékelés szabályai:
1. ha A primformula (ítéletváltozó): akkor a Ai feltételt pontosan azok az interpretációk teljesítik amelyekben  I (A)=i, a Ah feltételt pedig azok amelyekben I (A)=h.
2. a  (A) i  feltételek pontosan akkor teljesülnek, ha teljesülnek a  Ah feltételek.
3. a  (AB) i  feltételek pontosan akkor teljesülnek, ha teljesülnek a Ai és a  Bi feltételek.
4. a  (AB) i  feltételek pontosan akkor teljesülnek, ha teljesülnek a  Ai vagy a Bi feltételek.
5. a  (AB) i  feltételek pontosan akkor teljesülnek, ha teljesülnek a Ah vagy a  Ai feltételek.
A  (A) h  a  (AB) h , a  (AB) h , és a  (AB) h  feltételek értelemszerűen adódnak.

A -igazságértékelés a formulatípusokhoz adja meg azokat a feltételeket a formula argumentumaira, amelyeket teljesítő interpretációkban a formula értéke igaz illetve hamis lesz.  

A kapott feltételek teljesülésének feltételeit megadva és folytatva az eljárást az eljárás befejeztével az ítéletváltozókra kapott megkapjuk az összes megfelelő interpretációt. (igaz halmaz, hamis halmaz)
Példa. 

		 (XYZX) i, ha				implikációs formula

	Xh		vagy	(YZX) i, ha		diszjunkciós formula
1. értékadás/igazságkiértékelés
konjunkciós formula     (YZ) i,   vagy	  (X) i,  negációs formula
						
2. értékadás	   Yi és Zi 		Xh    3. értékadás

	1. ág			2. ág			3. ág
	X Y Z			X Y Z			X Y Z
	h ~  ~			~  i   i			h ~  ~	

Az igaz halmaz
X	Y	Z	
i	i	i	
h	i	i	
h	i	h	
h	h	i	
h	h	h	
A formula helyettesítési értékének kiszámítása az ítéletváltozók egy adott I igazságkiértékelése mellett. Lusta és mohó stratégia az A helyettesítési értékének kiszámítására. Például az I= X=h,Y=i,Z=i interpretációra az 1. ágon kapott feltételek miatt már az első lépésben kiderül, hogy a formula helyettesítési értéke i.

A hamis halmazt a formula hamissá válás feltételeinek megkeresésével kapjuk.
		 (XYZX) h, ha			 implikációs formula

1. értékadás		Xi	és
		(YZX) h, ha		diszjunkciós formula

			(X) h és
			 (YZ)=h, ha

2. értékadás		Xi és

3. értékadás	     Y h    vagy      Z h

		bal ág		jobb. ág	
		X Y Z		X Y Z		
		 i  h  ~		 i  ~  h		

A hamis halmaz
X	Y	Z	
i	i	h	
i	h	i	
i	h	h	

Definíciók. 
-Kielégíthetőség: Egy I-interpretáció (igazságkiértékelés) kielégít egy formulát, formulahalmazt, ha a formula vagy a formulahalmaz minden eleme igaz I-ben. Ha  van ilyen I-interpretáció, akkor a formula vagy formulahalmaz kielégíthető.
- Ha egy A formulát minden I-igazságkiértékelés kielégít - tautológia vagy logikai törvény jelőlése =0A.
- Kielégíthetetlen egy formula/ formulahalmaz, ha egyetlen I-igazságkiértékelés sem elégít ki.

A következményfogalom az itéletlogikában 
Tautológiák logikai törvények.

Szemantikus következményfogalon, eldöntésprobléma, előre- és visszakövetkeztetés
Definíciók:
Ítéletlogika:
-Egy  I interpretáció kielégít egy formulát, formulahalmazt - kielégíthető.
-Minden I interpretáció kielégít egy formulát - tautológia.
-Kielégíthetőség, kielégíthetetlenség.
-Egy G formula az F={F1, F2, ..., Fn} formulahalmaznak tautológikus következménye, ha minden olyan I interpretációra amelyre I=0{F1, F2, ..., Fn} fennáll,  I=0G is fennáll. Jelölés: (F=){F1, F2, ..., Fn}=0G
-Egy G formula bármely F feltételhalmaznak következménye - G tautológia.
-Legszűkebb következmény (közös igazságtáblával) – előrekövetkeztetés.
Tétel: F-nek következménye G, akkor és csak akkor, ha az F  {G} kielégíthetetlen. Visszakövetkeztetés
Tétel: Ha F-nek következménye G1 és S-nek következménye G2,  valamint, {G1, G2}-nek következménye A, akkor az F  S-nek következménye A.
Tétel:(dedukciós) Az {F1, F2, ..., Fn}=0G  akkor és   csak akkor, ha 
		{F1, F2, ..., Fn-1}=0 (FnG))...)).
Tétel: Az	{F1, F2, ..., Fn}=0G  akkor és   csak akkor, ha 
		F1(F2(...( Fn-1(FnG))...)). tautológia.
Ez az eldöntésprobléma az ítéletlogikában.

Előrekövetkeztetés: ismert az F feltételhalmaz és keressük F lehetséges következményeit.
Megkeressük F legszűkebb következményét V-t. Következmény minden olyan G formula, amelyre VG tautológia (1. rendben logikailag igaz) vagy V igazhalmaza része G igazhalmazának.

Példa. F={ZMP, Z, P }
P	M	Z	ZMP	Z	P	következmény	
						h vagy i	
h	i	i	i	i	i	i	
						h vagy i	
Csak egy igazságkiértékelésre kielégíthető a feltételhalmaz

Visszakövetkeztetés: Az F feltételhalmaz és a B következményformula ismeretében eldöntjük, hogy B valóban következménye-e F-nek. Mivel ha F=B, akkor {F.B} kielégíthetetlen, B akkor következménye F-nek, ha minden olyan interpretációban, ahol B hamis az F kielégíthetetlen. A probléma megoldása legfeljebb az itéletlogikában átlátható.

Példa. F={ZMP, Z, P } és be kell látni, hogy M következmény. Be kell látni, hogy , ha M igaz, akkor 
{ZMP, Z, P } nem lesz kielégíthető.
Hogy minden feltételformula i legyen Z=i, P=h. Viszont ha M hamis, akkor ZMP=h lehet csak. Tehát M következménye F-nek.

Példák előre és visszakövetkeztetésre igazságtáblával

Az eldöntésprobléma megoldása szemantikai eszközökkel.

Az állítások igazságértéke.

A mindennapi életben egy állítás igazságértékét tények, megfigyelés a tapasztalat alapján állapítjuk meg. 
Ha az állítások valamilyen tudományterületről valók, akkor az állítások igazságértéke az illető tudományág kutatási eredményei alapján lesz igaz vagy hamis. Ekkor a nyelvnek az állításokat leíró része speciális, az illető tudományterület nyelve. 
Az állítások közötti logikai kapcsolatok leírására mindig a logikai összekötőjeleket használjuk. 
Formalizálás az ítéletlogikában.

Miután a matematikai logika tanulmányozása a célunk, annak érdekében, hogy a matematika logika nyelvének definíciója világos legyen nézzünk meg a matematika néhány ágához tartozó logikai leíró nyelvet.
{Gyakorlatok (ötletek) 
Formula igazságtáblájának felírása. Szisztematikus igazságértékfelsorolásra felhívni a figyelmet.
Formula igazságértékelése. Összehasonlítás az igazságtáblával. Igaz halmaz, hamis halmaz.
Logikai változó igazságértékelése, mint értékadás.
Formula helyettesítési értékének kiszámítása. BI (A)  }

Néhány matematikai diszciplína (struktúra) leíró (logikai) nyelve.

Minden esetben adott az illető diszciplína meghatározásához,  
- a értelmezési tartomány, univerzum U, vagy indivíduumhalmaz, 
az univerzumon értelmezett legszükségesebb 
- (alap)relációk (logikai függvények/leképezések Un{i,h})és 
- (alap)műveletek (matematikai függvények/leképezések, UnU). 
Ezek az illető diszciplínában az egyszerű állítások leírásának eszközei. 
< U; R; M; C>
A struktúra szignatúrája 1,2,3.
- ha R R és R: Un{i,h}, akkor 1,(R)=n 
- ha FF és F: UnU, akkor 1,(R)=n 
- a ,3 megadja C elemeinek számát.

A struktúra típusa
<U, R1, R2, …, Rn; m1, m2, …, ms; c1, c2, …, cq> felsorolással együtt az aritások sorrendhelyes felsorolása a szignatúra egy más formában való megadása.

A leíró nyelv ábécéjében
a logikai jelkészlet:az indivíduumváltozók, az egyelőségreláció neve (=), a logikai összekötőjelek és a kvantorok. Kiegészítő elemek az elválasztójelek.
A nem logikai jelkészlet a relációk, műveletek és a konstansok nevei.

Példák.
1. Az elemi aritmetika logikai nyelve (Ar. nyelv).
Univerzum: N0 

ábécé:
Műveletek:			jelölésük
0-változós (konstans)		0
1-változós (rákövetkezés)		s(x)
2-változós (összeadás, szorzás) 	+, *.
Alaprelációk:
2-változós:			=, .
Összefoglalva: N0( =, .; s, *, +, 0) a zárójelben az Ar nyelv ABC-jének  “logikán kívüli” (speciális) része.

- Indivíduum változók: x, y,...
- Logikai műveletek: , , , 
- Kvantorok: ,  
Ezek alkotják az Ar nyelv ABC-jének  “logikai” részét. 
Elválasztójelek: ( ) ,

Szintaxis:
Matematikai leképezéseket leíró kifejezések a termek. Az s, *, +, 0 univerzumelemek és  változók felhasználásával az aritmetikában ismert (általában infix) módon.
Logikai leképezéseket leíró kifejezések a formulák. 
Az atomi formulák: x=y, xy. Ezekből a , , ,  és a ,  felhasználásával állítjuk elő a formulákat. 

Példák :
Termek: x+y, x*y+z.
Formulák:
x=y			atomi
x*s(s(0))  x+s(s(0))	atomi

Logikai leképezések leírása - formalizálása:
xy =def  x=y
xy =def z(y+z)=x
x<y =def xy  xy
x osztója y-nak: xy =def  x0  z(x*z)=y
x prímszám =def x0  xs(0)  z(zx (z=s(0)  z=x)
Az a nyelv amelyben az indivíduumváltozóra lehet a kvantorokat alkalmazni elsőrendű nyelv. Kifejezőerő. Lehetséges az univerzumra vonatkozó állításokat is leírni.

2. A részhalmaz logikai nyelv (Részh. nyelv).
Univerzum: P(H), egy halmaz hatványhalmaza.
ábécé
Műveletek:
1-változós (komplementer)	x. 
2-változós (metszet, unió) 		, .
Alaprelációk:
2-változós:			
Indivíduum változók: x, y,...
Összefoglalva: P(H)( ; x, , ) a zárójelben a részhalmaz nyelv ABC-jének  “logikán kívüli” része.

- Indivíduum változók: x, y,...
- Logikai műveletek: , , , 
- Kvantorok: ,  
Ezek alkotják az Ar nyelv ABC-jének  “logikai” részét. 
Elválasztójelek: ( ) ,

Szintaxis:
Matematikai leképezéseket leíró kifejezések a termek. Az x, , ) univerzumelemek és  változók felhasználásával a halmazelméletben ismert módon.
Logikai leképezéseket leíró kifejezések a formulák. Atomi formula:  xy. Ebből a , , ,  és a ,  felhasználásával állítjuk elő a formulákat. 
Példák :
Termek: xy, xyz, xx.
Formulák:
xy		atomi
Néhány fontosabb reláció  formalizálása:
x=y =def xy  yx
xy =def  x=y
xy =def xy   xy
Műveletek definiálása alaprelációkkal -formalizálása.
x = yz =def xy   xz  v(vy   vz  vx)

A háromdimemziós Euklideszi geometria logikai nyelve (geom nyelv).
Univerzum: E a háromdimemziós Euklideszi tér pontjai, egyenesei, síkjai. Tehát itt három “fajtájú” univerzum elem létezik. 
{A, B,...}=UP a tér pontjait, 
{p, q, ...}= UE a tér egyeneseit és 
{a, b, ...} = US a tér síkjait jelölik.
Ennek megfelelően E= UP  UE  US .
Alapműveleteket nem definiálunk.
Alaprelációk  ;2-változósak, és definíciójukban szerepel, hogy melyik fajta univerzumelemek kerülhetnek az argumentumokba.
-  A=B, argumentumok csak pontok lehetnek. UP x UP {i.h}
-  Az illeszkedés relációt, pont -egyenes illetve pont sík viszonylatában definiáljuk:
1) Bq, UP x UE {i.h}, pont illeszkedik egyenesre,
2) Ba, UP x US {i.h}, pont illeszkedik síkra.

A többi reláció már ezeket a relációkat felhasználó formulákkal leírható.
Például:
Egyenes illeszkedik síkra pa.
pa. =def A(Ap Aa)
Összefoglalva:
Szemantika a három nyelvre.
Minden term által leírt matematikai leképezés és minden formulával leírt logikai leképezés leolvasható a term illetve a formula alkotóelemeinek értéktáblájából.

Összefoglalva a felsorolt matematikai struktúrák logikai nyelveinek szerkezetét:
Az univerzum az elemek fajtájának megjelölésével nem a nyelv része, hanem a struktúra értelmezési tartománya.

- a nyelvek logikai része megegyezik
- a nyelvek “logikán kívüli” része az alaprelációk és az alapműveletek, amelyeket aritásuk és fajtájuk jellemezhet

	univerzum, 	relációk		műveletek		argumentumszámok
	N0  		( =, .;		 s, *, +, 0)		(2, 2;  1;  2,  2, 0)
	P(H) 		( ; 		x, , )		( 2;  1,  2,  2)
	UP ,UE ,US	( =, Bq, Ba;		    )		( 2, 2, 2;   -   )
	<{P, E, S}; U; R; ->

A matematikai logika nyelve egy olyan nyelv, amellyel bármely matematikai struktúra szimbolizálható. E nyelv ABC-jében minden, a matematikai struktúrák nyelveiben szereplő ABC-beli elemet szimbolizál valamilyen jel.. Ezt mutatja az alábbi táblázat.

A formalizált vagy többfajtájú  nyelv és a matematikai struktúra ABC-je közötti kapcsolat.

struktúra
	struktúra
ábécé	L mat. log. nyelv
ábécé	jelölés	minőség	összefoglaló jel	
az U univerzum elemei és a fajták halmaza (k-féle)	individuum változók	individuum változók az egyes fajtákhoz rendelve	xf1,yf1, ...,
...
xfk,yfk, ...,	logikai	Tp	
alapműveletek.arg. szám (0,1...) és fajták. 	Alapműveletek nevei. 	függvény szimbólumok  (a konstansok is)
arg. szám (0,1...) és fajták.	f (ti1, ..., tin, tf), 
g(tj1, ..., tjn, tg),	
logikán	Fn	
alaprelációk
arg. szám.(1,2...)	alaprelációk nevei	predikátum szimbólumok
arg. szám.(1,2...) és fajták	P (tk1, ..., tkn), 
Q(ts1, ..., tsn,), ...	kívüli	
Pr	
egyenlőség reláció	=	az egyenlőség
predikátum	=	logikai		

A fenti táblázatban megjelenő matematikai logikai nyelv összefoglaló jelölése:
 = <Tp, Kn, Fn, Pr >, amennyiben a konstansokra megkülönböztető jelölést vezetünk be,  
 = <Tp, Fn, Pr >, amennyiben a konstansokat mint 0-argumentumos függvényt tekintjük.

A matematikai struktúrák nagyrésze egyfajtájú (lásd Ar, Részh.). Ez azt jelenti, hogy a Tp, Fn és Pr halmazban egyfajtájú elemek szerepelnek. Ez jelölési egyszerűsítést tesz lehetővé de a logika tárgyalását nem befolyásolja, hiszen a nyelv matematika specifikus része az egyszerű állításmegfogalmazás eszköze, így a többfajtájú esetben árnyaltabb biztosítandó az interpretáló struktúra megtalálását. A logika tárgyalásához a jelölési egyszerűsítés előnyei miatt az egyfajtájú nyelvet választjuk mint az egyszerű állításmegfogalmazás szimbolikus eszközét. Ez a nyelv: L= < Fn, Pr >, azzal a megjegyzéssel, hogy L-hez tartozik az indivídiuumváltozók halmaza, amelyeknek megegyezik a típusa az univerzuméval.

Egy másik jelölésrendszerben a matematikai struktúra a következő:
univerzum
          relációk	   műveletek
S= U(R1, R2,..., Rn; o1, o2,..., ok)
        ( r1, r2,  ..., rn;  s1, s2, ..., sk) a struktúra típusa (szignatúrája)
A relációk és műveletek argumentumszámai.
Példák.
1. Boole  algebra
     a)  univerzum:P(H), relációk =, , műveletek , ,   .
	P(H)( =, ,; , ,  )
	         (2,  2 ;  2,  2,  1)  típus
     b) univerzum: {T,F}, reláció , műveletek , ,  .
	{T,F}( ; , ,  )
	         ( 2 ; 1,  2,  2 )  típus
2. Elemi aritmetika
            univerzum: N, relációk =,  , műveletek 0, 1, +, *
	N(=,  ; 0, 1, +, *)
	   ( 2, 2; 0, 0, 2, 2)

A formalizált vagy egyfajtájú L mat. log. nyelv és a matematikai struktúra ABC-je közötti kapcsolat. Elsőrendű és másodrendű nyelvi elemek.
struktúra
	struktúra
ábécé	mat. log. nyelv
ábécé	jelölés	minőség		Rend		
az U univerzum elemei	individuum változók	individuum változók	x, y, xk, ...,
	logikai				
alapműveletek.
arg. számok(0,1...)  	Alapműveletek nevei. 	függvény szimbólumok
arg. számok(0,1...) 	f, g, fr,	
logikán				
alaprelációk
arg. szám.(1,2...)	alaprelációk nevei	predikátum szimbólumok
arg. szám.(1,2...) 	P, Q, Ps, ...	kívüli	0.			
		az egyenlőség
predikátum	=			1.		
		logikai 
összekötőjelek	, , , , 	logikai			2.	
		kvantorok	, 					
		predikátum (halmaz) változók	Xn, Yn, ...					

Az így tekintett L formalizált nyelv esetén a szimbólumok és a struktúrák ABC- elemeinek megfeleltetése szemléletes.  
           predikátum       függvény    szimbólumok
      L (P1, P2,..., Pn; f1, f2,..., fk)
         ( r1, r2,  ..., rn;  s1, s2, ..., sk)  Az L nyelv típusa.
relációk	   műveletek
S= U(R1, R2,..., Rn; o1, o2,..., ok)
         ( r1, r2,  ..., rn;  s1, s2, ..., sk) a struktúra típusa
L és S típusa megegyezik – S egy modellje L –nek.

Az elsőrendű logika szintaxisa:
Legyen V egy ábécé és L[V] az ábécé feletti nyelv
Szintaxis - jól formált kifejezés előállításának szabályai

Term  - (matematikai leképezés szimbolizálása)
1. Egy indivíduum változó x jól formált term (jft)
2. Ha f egy n változós függvényszimbólum és t1, t2, ..., tn  jft-ek, akkor f(t1, t2, ..., tn)  jft.
3. Minden jft az 1., 2 véges sokszori alkalmazásával áll elő.

Formula  - logikai leképezés szimbolizálása
1. . Ha P egy n változós predikátumszimbólum és t1, t2, ..., tn  jft-ek, akkor P(t1, t2, ..., tn) jól formált formula (jff). (atomi formula, primformula)
2. Ha A, B  jff-ák, akkor (A)  jff.,	(zárójeles)
A, 		jff.		(negációs formula)
(AB) 		jff., 		(konjunkciós formula)
(AB) 		jff., 		(diszjunkciós formula)
(AB) 	jff., 		(implikációs formula)

---------------------------------------------------------------------------------0-rendű formulák 
3. xA, xA   jff-ák. (kvantált formula, primformula)
------------------------------------------------------------------------------1. rendű formulák
4. Minden jft az 1., 2 és 3 véges sokszori alkalmazásával áll elő. 
A kvantorok ,   prioritása a legerősebb. A ,  hatásköre a közvetlen részformula  jobbra.
	xP(x)y(Q(x,y)P(y)zQ(y,z))	x vegyes, y kötött, z kötött

 	hatáskör		         hatáskör                                                      
			hatáskör

Definíciók. 
Egy formulában egy x változó egy előfordulása
szabad, ha nem esik x-re vonatkozó kvantor hatáskörébe 
kötött ha x-re vonatkozó kvantor hatáskörébe esik.

Egy x változó egy formulában 
- kötött változó ha x minden előfordulása kötött,
- szabad változó ha x minden előfordulása szabad, 
- vegyes változó ha x -nek va szabad és kötött előfordulása is.

Egy formula zárt, ha minden változója kötött.
Egy formula nyitott, ha legalább egy indivíduum változónak van legalább egy szabad előfordulása.
Egy formula kvantormentes, ha nem tartalmaz kvantort.
1. rendű állítások és leírásuk az L nyelven.

Def. Alapkifejezés a változót nem tartalmazó L kifejezés (alapformula, alapterm).
a)Egy atomi formula konstans argumentumokkal (alapatom)
(Egy atomi formula alapterm argumentumokkal (alapformula)
Egy atomi formulát egyébként paraméteres állításnak is neveznek.

b) Mondat egy szabad változót nem tartalmazó elsőrendű formula (minden változó  kvantált vagy  más szóval kötött).

Termhelyettesítés.

Szemantika
 a ( L-értékelés)  L nyelv I interpretációja. Ez egy 
I= <ISrt, IP. IF, ICnst> függvénynégyes, ahol
ISrt: U
IP: P PI
IF: ffI  
ICns: ccI  
Változókiértékelés. : VU.   |x|I, az U univerzumbeli (x) indivíduum.
Informális definíció. A formula valamely L(P1, P2,..., Pn; f1, f2,..., fk ) formalizált nyelven íródott, 
(ahol ( r1, r2,  ..., rn;  s1, s2, ..., sk) az L nyelv típusa).

1. lépés. Választunk egy S= U(R1, R2,..., Rn; o1, o2,..., ok)  matematikai struktúrát ,amelynek a  típusa 
( r1, r2,  ..., rn;  s1, s2, ..., sk) megegyezik a nyelvével  és a logikán kívüli szimbólumokat a megfelelő relációkkal illetve műveletekkel azonosítjuk: Pi= PiI , fk=fkI , 
ha az interpretáló struktúrának nincs leíró nyelve, vagy nem akarjuk azt használni. Ha felhasználjuk az interpretáló struktúra leíró nyelvét, akkor PiI =Ri és fkI =  ok. Ez a nyelv szimbólumainak interpretációja, ahol Ri és ok.jelentése egyértelmű. 
2. lépés. A nem kötött indivíduum változók kiértékelése  (  |x|I,) és a kifejezések helyettesítési értékeinek kiszámítása.

Formális definíció.
- Termek: 1. xs indivíduumváltozó, |xs| I,  a  (x)U ( egy változókiértékelés)
	       c konstansszimbólum |c| I,  az U-beli cI elem.
	2. |f(t1, t2, ..., tn)| I,  = fI (|t1| I,  , |t2| I,  , ..., |tn| I,  )
- Formulák:
1. |P(t1, t2, ..., tn)) | I,   =i, ha  (|t1| I,  , |t2| I,  , ..., |tn| I,  )PI   , a PI jelöli a PI reláció igazhalmazát.
 
2. |A| I,  =|A| I,  	
    |AB| I,  = |A| I,   |B| I,  
|AB| I,  = |A| I,   |B| I,  
|AB| I,  = |A| I,   |B| I,  
3. |xA| I,   =i, ha |A| I,*  =i   minden * x variánsára 
 |xA| I,  =i, ha |A| I,*  =i   legalább egy * x variánsára (A a formula törzse/matrixa)

Példa:			nyelv			struktúra nyelve
 	       L=  (=, P1, P2 ; a, b, f1, f2)	S= N(=, <, >  ; 0, 1, +, * )
		(2,  2,  2 ;  0, 0, 2, 2 )	        (2,  2,  2 ;  0, 0, 2, 2 )
term interpretációja:
|t| I,   = |f1(x, f2(x,y))) | I,   = |f1| I,   (|x| I,  , |f2| I,   (|x| I,  ,|y| I,  )) = 

		         + ( x,  * (x ,y)) = x+ x*y 
	x	y	x+ x*y	
1	1	1	2	
2	2	3	8	
3	0	4	0	

Formula interpretációja
|P1(t, f1(y, f2(x,y)))) | I,    = |P1| I,    (|t| I,   , |(f1(y, f2(x,y))) | I,   )= 

|P1| I,    (|t| I, , |f1| I,  (|y| I,, |f2| I,  (|x| I,,|y| I,))) = 

					      < (+ (x,* (x,y)),+(y,*(x,y)) = 
					     <( x+ x*y, y+ x*y) = 

Egy kvantormentes formula kiértékelése	x	y	(x+ x*y)<( y+ x*y)	
A formula minden alap előfordulását generáljuk	1	1	i	
és így minden állítás előáll	2	3	h	

Egzisztenciális formula interpretálása
|x P1(a, f1(x,x))) | I, =i, ha |P1(a, f1(x,x))) | I,* =i  legalább egy * x variánsára 
ebben az interpretációban,   ha   0<(x+x) =i legalább egy uN

Nézzük meg az értéktábláját	x	0<(x+x)	
	0	h	
	1	i	
Mivel az x=1-re a formula törzse i, ezért a
	x(0<(x+x)) formula is i.

univerzális formula interpretálása
|x P1(a, f1(b,x))) | I, = i, ha |P1(a, f1(b,x))) | I,* =i   minden * x variánsára
Nézzük meg az értéktábláját	x	0<(1+x)	
	0	i	
	1	i	
Mivel minden egészre a formula törzse i, ezért a
	x(0<(1+x)) formula értéke i.
kb. a 4. óra vége____________________________________________________

Formulakifejtés véges U felett: U={a, b, c}
xA(x)) =A(a)  A(b)  A(c) 
xA(x)) =A(a)  A(b)  A(c) 

Lehetséges interpretáló struktúrák száma adott U és adott típus mellett

Legyen  az L nyelv típusa ( r1, r2,  ..., rn;  s1, s2, ..., sk). Legyen  U az univerzum, ahol U=M. hány különböző (r1, r2,  ..., rn;  s1, s2, ..., sk) típusú struktúra létezik U felett
j=1n 2Mpj* t=1 kMMst 
Elsőrendű szemantikus fa, mint a lehetséges adott univerzum feletti ( r1, r2,  ..., rn;  s1, s2, ..., sk) típusú struktúrák megadásának eszköze. Az univerzum elemeinek felhasználásával előállítjuk az összes alapatomot, rögzítjük sorrendjüket (ez a bázis), a szemantikus fa szintjeihez ebben a sorrendben rendeljük hozzá az alapatomokat. Egy interpretáció a szemantikus fa egy ágán áll elő.
Egy formula igazságtáblája és értéktáblája.
Egy 1. rendű formula  primformulái az atomi formulák (ezek paraméteres állítások az interpretációkban) és a kvantált formulák (ezek állítások ha zártak). 
Egy 1. rendű formula  primkomponensei a formula azon primformulái, amelyekből a formula logikai összekötőjelek segítségével épül fel.
Az igazságtáblában (0. rendű logika) az első sorba az állításváltozók (ezek a formula prímkomponensei) és a formula kerülnek. A változók alá igazságértékeiket írjuk. A formula alatt a megfelelő helyettesítési értékek találhatók.
	
X	Y	Z	(ZXYZ)	
i	i	i	         i	
i	i	h	         i	
i	h	i	         i	
		és így tovább

Egy 1. rendű formula értéktáblájában az első sorba a primkomponensek és a formula kerülnek. Mivel a primformulák több esetben paraméteres állítások, ezért az interpretációban az indivíduum változók kiértékelése után válnak állításokká. Ezért az értéktábla első sorába még a formulában lévő indivíduum  változókat is felsoroljuk a primformulák elé. A indivíduum változók alá azok lehetséges kiértékelései , a  primformulák alá a megfelelő helyettesítési értékek kerülnek. A formula alatt a prímformulák értékeinek megfelelő helyettesítési értékek találhatók.

Példa.
A formula	 xP(x)yQ(w,y)P(v)zQ(w,z)
A primkomponensek:  xP(x), y(Q(w,y), P(v), zQ(w,z)). A szabad indivíduum 
változók   v, w.
Legyen az interpretáló struktúra: U={1, 2, 3}, |P| I ={1,3}, |Q| I ={(1,2),(1,3), (2,1), (2,2), 2,3)},
Ekkor |xP(x)) | I = h, a többiek paraméteres állítások.

Az értéktábla: 
v	w	|xP(x)) | I	|yQ(w,y)| I	|P(v)| I	|zQ(w,z)) | I	|xP(x)yQ(w,y)P(v)zQ(w,z)| I	
1	1	h	|yQ(1,y)|I, =i	|P| I (1)=i	zQ(1,z)=h	i    mivel a feltételrész	
1	2	h	|yQ(2,y)|I, =i	|P| I (1)=i	zQ(2,z)=i	i    hamis minden kiértékelésre	
1	3	h	|yQ(2,y)|I, =i	|P| I (1)=i	zQ(3,z)=h	i	
2	1	h	|yQ(1,y)|I, =i	|P| I (2)=h	...	i	
3	1	h	|yQ(1,y)|I, =i	|P| I (3)=i		i	
2	2	h	|yQ(2,y)|I, =i	|P| I (2)=h		i	
2	3	h	|yQ(2,y)|I, =i	|P| I (2)=h		i	
3	3	h	|yQ(2,y)|I, =i	|P| I (3)=i		i	
3	2	h	...			i	

Definíciók
Az L egy I interpretációja kielégít egy 1. rendű A formulát   (I=A)  jelentése, hogy |A| I értéke i. Ha az A formula mondat és I=A, akor azt mondjuk, hogy az S struktúra elégíti ki A-t, így  S=A . Vagyis S  modellje  A-nak.
Ha L egy I interpretációjára az  F={F1, F2, ..., Fn} formulahalmazban  |Fi| I értéke i,  minden 1in-re, akkor I kielégíti F-et. Jelölés: I= F.
Azt mondjuk, hogy F  kielégíthető ha L-hez van legalább egy I interpretáció, hogy I= F. Azt mondjuk, hogy egy G formula kielégíthető ha L-hez van legalább egy I interpretáció, hogy I= G.
Azt mondjuk, hogy egy G formula  logikailag igaz, ha G  igaz  minden lehetséges I interpretációra. Ez azt jelenti, hogy G  igaz  minden lehetséges interpretáló struktúrában. Jelölés: = G.

 Kielégíthetetlenség. Azt mondjuk, hogy G vagy F is kielégíthetetlen (nem kielégíthető) ha L-hez nincs olyan I interpretáció, hogy I= G illetve, hogy I= F. Más szóval egy G formula kielégíthetetlen ha  minden interpretációban  a G értéktáblájának minden sorában G helyettesítési értéke h(amis). Az F formulahalmaz kielégíthetetlen, ha az F közös értéktáblájában minden sorban van legalább egy eleme F-nek, amelynek a helyettesítési értéke h(amis).

A következményfogalom az 1 rendű logikában. 
Logikailag igaz formulák és tautológiák.

Szemantikus következményfogalon, eldöntésprobléma, előre- és visszakövetkeztetés

1. rendű logika:
Logikai vagy szemantikus következmény. Azt mondjuk, hogy a G formula  logikai következménye az F formulahalmaznak, ha minden olyan I interpretációra amelyre I= F a  I= G is fennáll.  Jelölés: F= G. Más szóval F= G ha egy interpretáló struktúrában az F, G közös értéktáblájában minden sorban, ahol az F elemeinek helyettesítési értéke  i(gaz), a G helyettesítési értéke is i(gaz). Jelölés: F= G vagy {F1, F2, ..., Fn}= G.

-Egy G formula bármely F feltételhalmaznak következménye - G tautológia.
Tétel: F-nek következménye G, akkor és csak akkor, ha az F  {G} kielégíthetetlen. Visszakövetkeztetés
Tétel: Ha F-nek következménye G1 és S-nek következménye G2,  valamint, {G1, G2}-nek következménye A, akkor az F  S-nek következménye A.

A következményfogalom alapján, annak eldöntése, hogy F= G elméletileg megoldható az  interpretáló struktúrákban az F1, F2, ..., Fn és G-re kapott közös értéktábla alapján. Ha  létezik legalább egy  olyan interpretáló struktúra hogy ennek a közös értéktáblának minden olyan sorában, ahol  F1, F2, ..., Fn  igaz,  G szintén igaz akkor  F=G (G  logikai következménye  F-nek). Ha G kizárólag azokban sorokban igaz ahol  F1, F2, ..., Fn igazak, akkor G a legszűkebb következménye F-nek.
4. Az A és B 1. rendű formulák  logikailag ekvivalensek ha A=B és B=A.
Tétel . G elsőrendű formula. Ha =0 G, akkor = G. (Ha G tautológia, akkor G  logikailag igaz)
Biz. Ha =0 G, akkor G  igaz a primkomponenseinek  minden igazságkiértékelésére. Tekintsük  a G egy I interpretációját, az indivíduum változók egy  kiértékelése mellett ekkor a primkomponensek igazságértéke és ezután a G helyettesítési értéke kiszámítható és  i mivel=0 G
Tétel.  Ha  F=0 G, akkor F= G.
Biz. Az F prímkomponenseinek minden az F-et kielégítő I interpretációjára (I=0 F) I kielégíti G-t is. Ha az I interpretáció kielégíti F-et, akkor  kielégíti G-t is mivel az egyidejűleg   igazságkiértékelés.

Tétel. Ha A és B  tautologikusan ekvivalens, akkor A és B  logikailag ekvivalens.
Biz. Alkalmazva a 7. tételt , az A=0B és B=0A-ből következik hogy A=B és B=A.

Tétel. (Dedukciós tétel) {F1, F2, ..., Fn}=G  {F1, F2, ..., Fn-1}=FnG
Biz. (ugyanaz, mint a 0. rendű logikában)

Tétel (Eldöntésprobléma a predikátumlogikában) 
{F1, F2, ..., Fn}=G 
= F1(F2(...( Fn-1(FnG))...)). [Vagyis F1(F2(...( Fn-1(FnG))...))  logikailag igaz].
Biz.
 Ha  {F1, F2, ..., Fn}=G,  akkor =F1(F2(...( Fn-1(FnG))...)). A 9. tétel n-szeres alkalmazása az  irányba
 Ha =F1(F2(...( Fn-1(FnG))...)), akkor {F1, F2, ..., Fn}=G. A 9. tétel n-szeres alkalmazása az   irányba.
Helyes következtetési formák.
Egy F, B pár helyes következtetési forma, ha B szemantikus következménye F-nek.
Általános érvényű ítéletlogikabeli következtetésformák (jegyzet 63. old., könyv 165)
{AB,A}=0B, modus ponens
{AB,B}=0A, modus tollens vagy kontrapozíció. stb.
Általános érvényű 1. rendű következtetésformák
xA(x)=A(t), t tetszőleges jft.
Előrekövetkeztetés és visszakövetkeztetés mint az ítéletlogikában.
A 0 és 1 rendű eldöntésprobléma megoldása szemantikai eszközökkel.

Egy n változós ítéletlogikai B formula tautológia, ha 
- hamis halmaza üres. Ez azt jelenti, hogy B kielégíthetetlen.
- az ítéletváltozók minden kiértékelésére (minden interpretációban) a helyettesítési érték i.
1. rendű n változós B formula logikailag igaz, 
-  ha minden U univerzumon, a változók minden behelyettesítése mellett kapott B’ alapformulák igazak minden, a nyelvnek megfelelő struktúrában.
-   ha B kielégíthetetlen. Egyetlen interpretációban sem igaz.
Ezek a problémák szemantikailag világosak, de megoldásuk a teljes kipróbálást tételezi fel. Algoritmusokra van szükség a megoldáshoz.

(Példák kielégíthető, kielégíthető és logikailag igaz formulákra)
4. óra vége kb.____________________

Formulák logikailag ekvivalens átalakításainak elméleti háttere. 
Biz elm előkészítése {,}
Néhány halmazelméleti fogalom. A hamaz megadása, számosság, 
halmazműveletek, hatványhalmaz.
A hálóra mint algebrai struktúrára két (ekvivalens) definíció ismert.
	a)  U (univerzum/értelmezési tartomány), R rendezési reláció  U(R;)
	b)  U (univerzum/értelmezési tartomány), két kétváltozós mûvelet. 
U(; , ).
R ésa két hálóművelet ,  kölcsönösen származtathatók egymásból.
	R-bő l  ,  mint min(x,y), max(x,y)
	, -alapján R, R definíciója 
ha (x, y)=x, akkor xRy vagy R(x,y), itt a  művelet a min(x,y),
ha (x, y)=x, akkor xRy vagy R(x,y), itt a  művelet a min(x,y),
1. x, y)=yx		2. (x, y)=yx	kommutativitás
3. (x, y) z= x(yz)	4. (x, y) z=x(yz)	asszociativitás
5. x, (xy)= x		6. x, (xy)= x		elnyelés 
hálóaxiómák
,  egymás duálisai. Hálóelméleti dualitás.

Disztributív háló – ha teljesülnek még a
7. x, (yz)= (x, y) (x, z) 8. x,  (yz)= (xy)( xz) 
disztributivitási axiómák is.

Az R, R rendezések közül a háló univerzumán csak az egyiket használjuk. 

Hálódiagram fogalma. 

Ha van minimális O és maximális I elem az univerzumban például az R rendezésre, akkor egy q univerzumelem komplementuma az a v univerzumelem, amelyre q  v=O és q  v=I.. 
Komplementumos hálóról beszélünk ha minden univerzumelemnek van legalább egy komplementuma. 
Egyértelműen komplementumos hálóról beszélünk ha minden univerzumelemnek pontosan egy komplementuma van. Ha a háló komplementumos és disztributív is, akkor bizonyítható, hogy egyértelműen koplementumos. Ekkor definiálható egy k(x) egyargumentumos mûvelet mint komplementumképzõ mûveletet, amelyre fennállnak a 
9. x  k(x)=O, 10. x  k(x)=I axiómák.
A komplementumos disztributív hálót Boole algebrának nevezik.

Példák:
Egy H halmaz P(H) hatványhalmaza a rajta értelmezett halmazelméleti metszet, unió, komplementer mûveletekre Boole algebra
Az {i, h} halmaz a rajta értelmezett konjunkció, diszjunkció és negáció műveletekre Boole algebra. (Az ítéletlogika Boole algebra)

Logikai műveletekre érvényes azonosságok.
Előkészítő definíciók: literál, azonos alapú literál, különböző literál, elemi konjunkció, -diszjunkció, teljes elemi konjunkció, -diszjunkció, konjunktív és diszjunktív normálforma (KNF, DNF), kitüntetett konjunktív és diszjunktív normálforma (KKNF, KDNF).
DeMorgan szabályok:1. ¬(XY)= XY, 2. (XY)= X¬Y
Bebizonyíthatók az axiómák alapján.

Egyszeûsítési szabályok: 1. (Xd)(Xd)= d, 2. . (Xk) (Xk)=k, ahol d elemi diszjunkció és k elemi konjunkció.

n-változós formula {i,h}n {i,h} leképezést ír le.
Művelethalmaz funkcionális teljessége.
Algoritmusok egy adott leképezést leíró KKNF és KDNF konstrukciójára.

Az egyszerűsítési szabályok.
KKNF és KDNF, valamint KNF és DNF egyszerűsítése. 
Tetszőleges formulák átírása DNF-be és KNF-be.
kb. az 5. óra vége._____________________

A logika szintaktikai alapokon való felépítése az ítéletkalkulus.
Más szóval a 0. rendű logika - ítélet vagy állításlogika bizonyításelméleti felépítése.
(Elmélet - egy axiomatizált struktúra)
Szintaktikus következményfogalon, eldöntésprobléma, előre- és visszakövetkeztetés

Definíciók:
Az ítéletlogikát leíró nyelvben itt a logikai összekötőjelekből csak a ,  párt használjuk(funkcionálisan teljes művelethalmaz).
Axiómák (axiómasémák) megadják a műveletek tulajdonságait.
1. ABA
2. (ABC) (AB) AC
3. (AB) (AB) A

Kapcsolat a szemantikával: 
Ezek az axiómák tautológiák / logikai törvények.
Tétel: Legyen G egy formula, G(X/S) az a formula, amit G-ből X változójának egy S formulával való behelyettesítésével kaptuk. Ha G tautológia, akkor G(X/S) is az.
Következmény: Az axiómákból behelyettesítéssel kapott formulák is logikai törvények - axiómának tekinthetők.
Tétel: {AB, A}=0B

-Bizonyításelméleti levezetés fogalma. G-nek F-ből való levezetése.
-Levezetési szabály  modus ponens  -  leválasztási szabály.
-Egy G formula az F={F1, F2, ..., Fn} formulahalmazból levezethető F={F1, F2, ..., Fn}0G, ez a szintaktikus következményfogalom.

Tulajdonságok
- Egy G formula bármely F feltételhalmazból levezethető - G bizonyítható 0G.
- Egy F={F1, F2, ..., Fn} formulahalmaz ellentmondásos, ha F0G és F0 G
- Egy F={F1, F2, ..., Fn} formulahalmaz nem ellentmondásos

Példa levezetésre / bizonyításra: 0AA

Tételek
Tétel: Két levezetés konkatenációja is levezetés. Ha F-ből levezethető G1 és S-ből levezethető G2,  akkor a két levezetés konkatenációja az F unió S-ből való levezetés.

Tétel: Ha F- ből levezethető G1 és S- ből levezethető G2,  valamint, {G1, G2}- ből levezethető A, akkor az 
F  S- ből levezethető A.

Tétel (dedukciós): Az {F1, F2, ..., Fn}0G  akkor és   csak akkor, ha 
{F1, F2, ..., Fn-1}0 FnG
Biz:
Tétel: Az {F1, F2, ..., Fn}0 G  akkor és   csak akkor, ha 
0F1(F2(...( Fn-1(FnG))...)). 
Ez az eldöntésprobléma a bizonyításelméletben.

kb. a 6. óra vége._____________________

Tétel: Ha  {F1, F2, ..., Fn}0G  akkor {F1, F2, ..., Fn}=0G. (Helyesség)

Tétel: Ha F- ből levezethető G, akkor az F {G} ellentmondásos.

Tétel: Ha  {F1, F2, ..., Fn}ellentmondásos, akkor kielégíthetetlen.

Tétel: Ha {F1, F2, ..., Fn}B ellentmondásos, akkor {F1, F2, ..., Fn}0B.
Tétel: Egy k-változós G formula igazságtáblájának minden sorában  X1’,X2’,...,Xk’0G’
Tétel: Ha X1’,X2’,...,Xk’0G’ és X1’,X2’,...,Xk’0G’ ,akkor X2’,...,Xk’0G’
Tétel: Ha G tautológia, akkor G bizonyítható. (Gyenge teljesség).
Tétel: Ha{F1, F2, ..., Fn}=0G, akkor  {F1, F2, ..., Fn}0G. (Teljesség) 
Gödel féle gondolatmenet
Előrekövetkeztetés és visszakövetkeztetés a bizonyításelméletben.

Az 1. rendű logika bizonyításelméleti felépítése.
Előkészítés
Definíció. Egy C formula általánosítása az a zárt formula, amely az eredeti formula szabad változóinak univerzális kvantálásával áll elő.
Helyettesítés.
 x egy h term változója, t egy jft. h(x/t) az term, amelyet t-nek x minden előfordulásába való behelyettesítével kaptunk.
 x az A formula szabad változója, t egy jft.. 
A(x/t) az a formula amelyet t-nek x minden szabad előfordulásába való behelyettesítével kaptunk.

Probléma a behelyettesített formula jelentése egy I interpretációban legyen ugyanaz, mint az I-ben interpretált 	formula  behelyettesítettje.
Más szóval ugyanazt a leképezést írják le a formulák.
Formálisan: |[A(x/t)]|I   |A|I (x/|t|I)

Ha t eleget tesz ennek a feltételnek, akkor a t termet szabad az x-be helyettesíteni.
- a t term változói nem kerülhetnek kvantor hatáskörébe.

Például y(x=y) esetében a leírt leképezés az   x
x	y(x=y) - 	
u1	y(u1=y) - h, ha U legalább 2 elemű	
u2	y(u2=y)           	
u3	...	

Legyen a helyettesítés x/y, akkor a y(x=y) formula 
1. előbb helyettesítünk - y(y=y)
Interpretálunk: |(y=y))|I  = i, bármely interpretációban,
 tehát a |y(x=y)( x/y) ) |I  = i bármely interpretációban
2. Előbb interpretálunk és utána helyettesítjük az interpretált termet:
|y(x=y) )|I  ( x/|y)|I, ), vagyis a formula y(|y)|I, =y) lesz, ami hamis.
(Példa: arra, amikor t-t szabad és amikor nem szabad x-be helyettesíteni.)
Az elsőrendű bizonyításelmélet axiómarendszere.
1-3 a 0-adrendű axiómák.
Az univerzális kvantorra vonatkozó axiómák.
4.x(AB)xAxB.  A, B elsőrendű formulák és x indivíduumváltozó.
5. AxA. Az x nem szabad A-ban
6.xAA(x/t).  a  t  term helyettesítése megengedett x -e.
Az = predikátumra vonatkozó axiómák. ,t1
7. t = t  
8. t1 =tn+1 ... tn =t2nf( t1 ,t2,...,tn)=f(tn+1,tn+2,...,t2n)
9. t1 =tn+1 ... tn =t2nP( t1 ,t2,...,tn)P(tn+1,tn+2,...,t2n)
10. Az 1-9 axiómák általánosításai.

Az axiómák logikailag igazak.
A levezetési szabály a modus ponens.
Következményfogalom, eldöntésprobléma mint nulladrendben.
Helyesség / teljesség u.úgy kezelhető.
Megjegyzés. Az egyenlőségjeles nyelvek esetén a kielégíthetőség és érvényesség vizsgálatánál a kielégíthetőséget csak az = axiómáknak eleget tevő struktúrákban kell vizsgálni.
Az érvényességhez elegendő, ha  formula csak az = axiómáknak eleget tevő struktúrákban azonosan igaz
Ez az egyik legismertebb korlátozó feltétel. A korlátozó feltételek kezelése a logikában, az alkalmazások szempontjából fontos.
Pl. 1.r. levezetésekre

szintaktikai és szemantikai tulajdonságok megfeleltetése

szemantikai tulajdonságok	szintaktikai tulajdonságok	
tautológia vagy logikailag igaz	bizonyítható	
F-nek következménye G	F-ből levezethető G	
F kielégíthetetlen	F ellentmondásos	

kb. a 7. óra vége._____________________

Döntési algoritmus, levezető eljárás egy olyan algoritmus, amely adott input adatokkal dolgozik, azokat a megfelelő szabályok szerint használja fel és a levezetési szabály szerint alakítja át és akkor áll meg amikor a kitűzött célt elérte. A megállással egy kétesélyes döntés egyik kimenetét igazolja. Azonban, ha az algoritmus nem éri el a kitűzött célt az nem feltétlenül jelenti azt, hogy  meghozta a másik eshetőségre a döntést.
A bizonyításelméleti levezetés konstrukciója egy levezető eljárás
Input: { F1, F2, ..., Fn } feltételformulák, G formula.		Levezetési szabály: modus ponens
Algoritmus: { F1, F2, ..., Fn }-ből való levezetés konstruálása.
Kitűzött cél: A levezetésben a G formula elérése.
___________________________________
Más levezető eljárások keresése.
Rezolúciós elv, az ítéletlogikában
Az eldöntésprobléma átírása megfelelő alakú formulákra.
{F1, F2, ..., Fn} =0G  akkor és csak akkor, ha =0 F1(F2(...( Fn-1(FnG))...)). 
vagy 	( F1(F2(...( Fn-1(FnG))...)))= F1F2... Fn-1FnG 	 kielégíthetetlen
Azaz {F1,F2,..., Fn-1,Fn,G} 		 kielégíthetetlen
KNFF1KNFF2...KNFFn-1KNFFn KNFG kielégíthetetlen 
ezért
{KNFF1,KNFF2,...,KNFFn-1,KNFFn, KNFG} 	kielégíthetetlen
Más szóval
a belőle kapott S klózhalmaz kielégíthetelen

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	

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

Példa	{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. 

Rezolvens fogalma, res(C1, C2) a C klóz; { C1, C2}=0 C

Def. K klózhalmazból való rezolúciós levezetés. ...

Levezetés célja ü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? Rezolúciós cáfolat.

Példa {AB, AC, AC, BC, C}-ből rezolúciós levezetés: 1.C, 2.AC, 3.A, 4.AC, 5.C, 6.
Tétel: (Helyesség) Ha a K klózhalmazból levezethető az üres klóz, akkor a K klózhalmaz kielégíthetetlen.
Biz. a { C1, C2}=0 C felhasználásával

Tétel: (Teljesség) Ha a K klózhalmaz kielégíthetetlen, akkor a K klózhalmaznak van rezolúciós cáfolata.
Biz.  Zárt szemantikus fával
Előrekövetkeztetés és visszakövetkeztetés.

Def. Levezetési fa. (Egy rezolúciós levezetés szerkezetét mutatja)

Rezolúciós stratégiák. Lineáris rezolúció (teljes), lineáris input-, egység rezolúció (nem teljes)

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

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.
Horn klózok. Horn logika.

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 K klózhalmazból, akkor K-ban 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.
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.

Teljes levezetési fa
		C

	BC		AC

	B				A

	AB			AB		AC

	A   +			B		C

	AC			BC		BC	AC  

	C			C		B		A   nem ad újat

	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)

Elsőrendű logika formuláinak logikailag ekvivalens átalakításai.
Annak igazolása, hogy egy 1. rendű formula B  logikailag igaz (=B) elképzelhető úgy is, hogy minden lehetséges struktúrában interpretáljuk  B-t és kiszámítjuk az értékét. Ha ez az érték i  minden struktúrában, akkor B logikailag igaz. Ez a B-t interpretáló lehetséges struktúrák száma miatt nem végrehajtható. Ehhez döntési algoritmust (vagy levezető rendszert) kell találni.
Az  előrekövetkeztetés és a visszakövetkeztetés az 1. rendű logikában ugyanaz, mint az ítéletlogikában.
Egy döntési algoritmust (vagy levezető rendszert) keresve az 1. rendű formulákat speciális alakba írjuk át.
Az első a  prenex forma. Jelöle Q bármely kvantort. 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.
Átírási szabályok

xA=xA	xA=xA       általános  DeMorgan szabályok 

A kvantorkiemelési szabályok
1. xA[x]B=x(A[x]B)
    “        “=      “       “   
2. xA[x]B= x(A[x]B)  
    “       “ =      “      “   
3. xA[x]xB[x]= x(A[x] B[x]) , de   -re 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]).

A prenex formába való átírás algoritmusa.
1. A logikai összekötőjelek átírása , , -ra.
2. A DeMorgan szabályok alkalmazása addig amíg a  hatásköre atomi formula nem lesz.
3. A kvantorkiemelési szabályok alkalmazása addig amíg  minden kvantor a formula elejére nem kerül (ami kvantormentes formula).

Példa.
x (yP(x,y)y (Q(y)P(x,a))) xy(P(x,y)R(x,y)
1. lépés
x (yP(x,y)y(Q(y)P(x,a))) xy(P(x,y)R(x,y))
2. lépés.
x(yP(x,y)y(Q(y)P(x,a)))xy(P(x,y)R(x,y))
x(yP(x,y) y(Q(y)P(x,a))) xy(P(x,y)R(x,y))
x(yP(x,y) y (Q(y)P(x,a))) xy(P(x,y)  R(x,y))
x(yP(x,y) y (Q(y)P(x,a))) xy(P(x,y)  R(x,y))
3. lépés. kvantorkiemelési szabályok
 x-re 
x(yP(x,y) y (Q(y)P(x,a))  y(P(x,y)  R(x,y)))
 y-re először végrehajtjuk az y/y1 helyettesítést a y-al kezdődő első részformulában és az  y/y2  helyettesítést ay al kezdődő második részformulában
x(yP(x,y) y1 (Q(y1)P(x,a))  y2 (P(x,y2)  R(x,y2)))
xy(P(x,y) y1 (Q(y1)P(x,a))  y2 (P(x,y2)  R(x,y2)))
és végül
xyy1 y2 (P(x,y) (Q(y1)P(x,a))  (P(x,y2)  R(x,y2)))
Megkaptuk a  prenex formulát.

Ha a prenex formula törzse KNF-ben vagy DNF-ben van, akkor a formula normálforma: prenex konjunktív / prenex diszjunktív formula.
A másik speciális 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, ha az A formula alakja KNF, akkor Skolem normál 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 bevezetjük 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: x  P(x,f(x))
Interpretációk
Minden emberhez van olyan nő, aki az anyja. Skolem fv. anyja(x).
Egy sokszög minden csúcsához van legalább egy hozzá legközelebbi csúcs. Skolem fv. legközelebbi(x).
Minden számhoz van nála eggyel nagyobb szám. Skolem fv.s(x), a rákövetkezési fv..

 A prenex formulák kifejtése adott véges univerzumú  U=m  interpretációban.
egzisztenciális formula
 (xA) U =A(x/u1) A(x/u2)  ... A(x/um),
Skolem formula (univerzális formula)
(xA) U=  A(x/u1) A(x/u2)  ... A(x/um) ,ahol A(x/uj)  alapformula.

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 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 törzse A  KNF alakú, akkor minden A(x/uj)  egy-egy alap  KNF, vagyis  (xA) U kifejtésében alapklózok konjunkciója. Ha a xA formula kielégíthetetlen , akkor ezen alap KNF-ák konjunkciója kielégíthetetlen , ami azt jelenti, hogy ezen  alapklózok halmaza kielégíthetetlen. Ez azt jelenti, hogy 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 .
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   [F1F2... Fn-1FnG]=S.  -t  kapjuk ami kielégíthetetlen.
Megkonstruáljuk az előbbi formula Skolem formuláját , amelyben  a törzs KNF alakú, és a klózok változóidegenek. A kvantorok bevitelével átírjuk 1 rendű klózok konjunkciójaként a formulát.
A szemantikus eldöntésprobléma új alakja a Skolem 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.
Megjegyzés: Ha csak egy adott problémát kell megoldani , ami azt jelenti, hogy a problémát leíró nyelv mellett adott az U univerzum is, akkor a klózhalmaz kielégíthetetlenségét elegendő az U univerzum feletti összes struktúrán megvizsgálni. 
Tehát tekintjük az U univerzum felett az  összes struktúrát.
S kielégíthetetlen az U felett, 
- a) ha S kielégíthetetlen 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.
Megjegyzés. Az eldöntésprobléma ekvivalens megfogalmazásai.
Logikai igazság (érvényesség) - azonosan igaz - kielégíthetetlenség
A1) F formula logikailag igaz-e (érvényes-e). Azonosan igaz-e bármely számosságon.
B1) F formula kielégíthetetlen-e. Nincs olyan struktúra, ami kielégítené.
Kielégíthetőség
A2) F formula kielégíthető-e (van-e olyan struktúra, ami kielégíti?). Ugyanis ekkor F nem azonosan igaz.
Probléma. 
- Az eldöntésprobléma vizsgálatánál milyen számosságig kell elmenni, hogy a döntést meghozhassuk? 
- Az F milyen számosságú halmazon azonosan igaz illetve kielégíthető. (Ha nem teljes általánosságban kell megoldani a problémát)
Véges számosságra két esetet mutatunk.
1.1. Az L nyelv nem egyenlőségjeles. Ha az F formula azonosan igaz n számosságú U halmazon, akkor minden nála kisebb k számosságú, nem üres W halmazon  is azonosan igaz. Legyen W ekvivalens U valamely nem üres U’ részhalmazával. Tegyük fel, hogy F nem azonosan igaz az U’-n, tehát van olyan U’(R1’, ...,Rn’; f1’, f2’,..., fk’) struktúra, amelyben F nem igaz. Legyen ez a struktúra homomorf képe az U(R1, R2,..., Rn; f1, f2, ..., fk)-nak, ahol
q(x)= x, ha xU’ és
q(x)= a U’, ha xU\U’.
 Az Rj(x1,...xr)=Rj’(q(x1), ...q(xr)) és fs(x1,...xf)=fs’(q(x1), ...q(xf)) olyan struktúra U-n, amely homomorf az U’(R1’, ...,Rn’; f1’, f2’,..., fk’) struktúrával.  Ha F nem igaz U’-n ebben a struktúrában, akkor nem lehet azonosan igaz U-n a feltétellel ellentétben.
Pl.  P(x)P(y) G(x)G(y)zG(z)  1 és 2 elemű univerzumon azonosan igaz, nagyobb számosságon nem.

1.2. Az L nyelv nem egyenlőségjeles. Az F formula kielégíthető n számosságú U halmazon, akkor kielégíthető minden nagyobb s számosságú W halmazon  is. 
Ha F nem lenne kielégíthető W-n, akkor F azonosan igaz lenne W-n, de akkor az 1.1. eset miatt F azonosan igaz lenne a kisebb számosságú U-n is. Emiatt azonban F nem lehetne kielégíthető U-n.
xy(P(x)P(y)) - 2 és nagyobb számosságon kielégíthető de egyelemű halmazon nem elégíthető ki.

2.1. Ha az L nyelv  egyenlőségjeles, akkor a fenti eredmények nem érvényesek.
Példák:
x(P(x)P(f(x))f(f(x))=x) - 2, 4,... elemű halmazon kielégíthető de 3, 5... eleműn nem. (páros - páratlan elemszámú univerzum) A feltételnek eleget tevő f(x) csak páros univerzumon definiálható úgy, hogy f(x)x. Ebben az esetben lehet P-t úgy definiálni, hogy P(x)  P(f(x)) minden x-re i legyen.
Lőwenheim-Skolem tétel. Egy F formula akkor elégíthető ki egyáltalán, ha kielégíthető legfeljebb megszámlálható halmazon.

Definíciók.
- Az L nyelv B bázisa U felett a nyelv összes alapatomjainak rendezett halmaza, vagyis a predikátumszimbólumokból az U elemeinek behelyettesítésével kapott alapatomok valamely sorozata. 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 általánosan
B={A1,      A2,           A3,      A4,           A5,             A6,            A7,      ...}

Az U feletti (1,2; ) típusú struktúra (vagy szokásos szóhasználat szerint: 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.
Olyan bináris fa, amelynek ágain az U feletti összes lehetséges - adott típusú - struktúra megjeleníthető.
 A szemantikus fa mindig egy B bázisra épül. 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 az interpretációban. 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 (interpretáció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:  K= {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 , a P(u1), Q(u1,u1) P(u1),   Q(u1,u1)}  alapklózokra a szemantikus fa zárt lesz. 
Ha K 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)

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

Megmutatjuk alaprezolúcióval, hogy  a 
xy((P(x,y)P(y,x))z(P(x,z)P(z,y)))		formula
kételemű univerzumon kielégíthetetlen (azaz nem létezik megfelelő Skolem függvény) könyv 254-257.old
Átalakítások:
xy((P(x,y)P(y,x))z(P(x,z)P(z,y)))
xy(P(x,y)P(y,x)) wv z(P(w,z)P(z,v))		változóidegenné tevés
xy(P(x,y)P(y,x)) wv(P(w,f(w,v))P(f(w,v),v))	f Skolem függvény

alappéldányok, U={a,b}

xy(P(x,y)P(y,x))-re
x	y	xy(P(x,y)P(y,x))	
a	a	1. P(a,a)	
b	b	2. P(b,b)	
b	a	3. P(b,a)P(a,b)	
a	b	ugyanaz	

wv(P(w,f(w,v))P(f(w,v),v))-re
w	v	wv(P(w,f(w,v))P(f(w,v),v))	(2)	
a	a	4. P(a,f(a,a))P(f(a,a),a))		
b	b	5. P(b,f(b,b))P(f(b,b),b))		
b	a	6. P(b,f(b,a))P(f(b,a),a))	(2)6. P(b,a)P(a,a))	
a	b	7. P(a,f(a,b))P(f(a,b),b))	(2)7. P(a,a)P(a,b))	

az f definíciói:
w	v	f(w,v)	
a	a	a                       b	
b	b	b                       a	
b	a	~              a               b	
a	b	~         a       b      a        b	
	    (1)	 (2)    (3)   (4)      (5)
	egyik sem jó
(1)-re az alaprezolúciós cáfolatok		
a,a behelyettesítésre: f(a,a)=a		b,b behelyettesítésre: f(b,b)=b	
P(a,a)		1-ből				P(b,b)		2-ből
P(a,a)		4-ből				P(b,b)		5-ből	

(2)-helyettesíttésre az alaprezolúciós cáfolat
1. P(b,a)P(a,a))		(2)6-ból
2. P(a,a)		1-ből
3. P(b,a)		rezolvens
4. P(b,a)P(a,b)	3-ból
5. P(a,b) 	rezolvens
6. P(a,a)P(a,b))		(2)7-ből
7. P(a,a)		rezolvens
8. P(a,a)

A többire ugyanígy van cáfolat. Tehát a formula kielégíthetetlen kételemű univerzumon, mivel nem létezik Skolem függvény.

Az alaprezolúciós levezetés mint kalkulus egy, csak logikai eszközöket felhasználó automatikus tételbizonyító. DE az eldöntésproblémát csak az adott univerzumra oldja meg, így csak egy adott univerzum melletti kielégíthetetlenséget lehet belátni.

Herbrand megmutatta, hogy minden elsőrendű klózhalmazhoz létezik legfeljebb megszámlálhatóan végtelen univerzum, a Herbrand univerzum, amelyre fennáll hogy 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, ahol  Fi={ alaptermek; a klózhalmazban lévő függvényszimbólumokba behelyettesítve Hi elemeit}
H = kN Hk 
Legyen a klózhalmaz:  K= {P(x),   Q(y,z) P(z),   Q(u,v)} ekkor 
H = {a}

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. 

Adott két elsőrendű klóz. Két literáljuk akkor komplemens pár, ha szimbólumról szimbólumra megegyeznek és ellenkezően negáltak. Ha találtunk olyan alaphelyettesítést, hogy egy literálpár alappéldányai komplemens párt alkotnak, akkor azt mondjuk, hogy az illető alaphelyettesítés illeszti a két literált (illesztő alaphelyettesítés). Feladat eldönteni, hogy egy literálpárra van-e illesztő helyettesítés. Megadunk egy algoritmust, amely az illesztő helyettesítést megtalálja ha ilyen létezik és megmondja azt is ha nem létezik ilyen helyettesítés.
Jelölések: W - literálhalmaz. Pl. { Q(y,z), Q(u,f(u))}
	D - a W összeférhetetlenségi halmaza (az argumentumokban balról jobbra haladva az első nem megegyező szimbólummal kezdődő termek halmaza). Esetünkben D={y,u}
j helyettesítés
Az algoritmus.
1.	k=0, W0=W, k=.
2.	Ha Wk egyelemű, akkor k illesztő helyettesítés W-re. Vége.
3.	Legyen Dk a Wk összeférhetetlenségi halmaza. Ha Dk -ban van egy vk változó és tk term, ahol vk  tk, akkor k+1 =k(vk / tk) és Wk+1 =Wk(vk / tk). k=k+1. Folyt. 2-vel.
4.	Nincs illesztő helyettesítés. Vége.

Példa.
{ P(x),  Q(y,z) P(z),  Q(u,f(u))} a klózhalmaz.
Illesszük a { Q(y,z), Q(u,f(u))} literálhalmazt.
 (y/u)(z/f(u)) az illesztő helyettesítés. A helyettesítés után a klózhalmaz:
S={1. P(x),  2. Q(u,f(u)) P(f(u)),  3. Q(u,f(u))}
A 2,3 klózoknak van (elsőrendű) rezolvense: P(f(u)). 
Elsőrendű rezolúciós levezetés egy olyan k1,k2, …,kn klózsorozat ahol kja klózhalmaznak vagy (elsőrendű) rezolvense őt megelőző két klóznak. Cél az  levezetése.

Példa. Elsőrendű rezolúciós levezetés S-ből.
k1. Q(u,f(u)).
k2. Q(y,z) P(z).  (alkalmazva a (y/u)(z/f(u)) illesztő helyettesítést)
k3. P(f(u)) a rezolvense k1,k2-nek. )), ami illeszthető a klóhalmazbeli P(x)-el. 
k4. P(x)	A helyettesítés (x/f(u))
k5. .

Egy klóz faktorizálásának nevezzük azt a lépést, amikor az azonosan negált és azonos nevű predikátumait illesztjük. Például a (P(g(z))P(v)) klóz esetén a v/g(z) helyettesítésre P(g(z)) az erdmény.
Az elsőrendű rezolúciós levezetés előállítása során a faktorizálható klózokat faktorizálni kell. Lehetséges, hogy faktorizálás nélkül egy kielégíthetetlen S klózhalmazból nem lehet elsőrendű cáfolatot kapni.

Példa
A formulák			a változóidegen klózok:
xy(A(x) B(y,y)  B(x,y))  	xy( A(x)  B(y,y)  B(x,y)) 
xy( A(x)  B(y,y)  B(x,y)) x1y1( A(x1)  B(y1,y1)  B(x1,y1)) 
x A(x)				x2 A(x2)

H = {a}, a bázis: {A(a), B(a,a)}
Az alapklózhalmaz:
{( A(a)  B(a,a)  B(a,a)), ( A(a)  B(a,a)  B(a,a)),. A(a)} az összevonások után:
 Sa={ A(a)  B(a,a) ,  A(a)  B(a,a) ,. A(a)} az összevonások után:
Alaprezolúciós levezetés			Szemantikus fa lezárás
1. A(a)
2. A(a)  B(a,a) 			A(a)			A(a)
3. B(a,a) 						 	         A(a)
4.  A(a)  B(a,a) 
5.  A(a) 		  B(a,a)		B(a,a)	
6. 
		A(a) B(a,a)	         A(a)  B(a,a)

1 rendű rezolúciós levezetés
1. A(x2)
2.  A(x)  B(y,y)  B(x,y)
3. B(y,y)  B(x,y)	rezolvens  x2/x helyettesítéssel
4.  A(x1)  B(y1,y1)  B(x1,y1)
5.  B(y1,y1)  B(x1,y1) rezolvens (1,4)  x/x1 helyettesítéssel.
A levezetés nem folytatható egynél több komplemens pár lesz.

1 rendű rezolúciós levezetés, faktorizációval
1. A(x2)
2.  A(x)  B(y,y)  B(x,y)
3. B(y,y) 	rezolvens  x2/x helyettesítéssel és x/y faktorizációval.
4.  A(x1)  B(y1,y1)  B(x1,y1)
5.  B(y1,y1)  B(x1,y1) rezolvens (1,4)  x/x1 helyettesítéssel és x1/y1 faktorizációval.
6.	(3,5)-ből y/y1 helyettesítéssel.
Az elsőrendű rezolúciós kalkulus eljárás helyes.
Ehhez meg kell mutatni, hogy az elsőrendű rezolvens logikai következménye az őseinek.

Formalizálás 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, egy köteg banán és egy majom. A banán a plafonról lóg le úgy, hogy a majom nem tudja elérni.
A probléma. El tudja-e érni 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ó

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.