Automatikus tételbizonyítás

Automatikus tételbizonyítás előadások Várterész Magda Kádek Tamás

Created by XMLmind XSL-FO Converter.

Automatikus tételbizonyítás: előadások Várterész Magda Kádek Tamás

Created by XMLmind XSL-FO Converter.

Table of Contents 1. Előszó ............................................................................................................................................. 1 2. Bevezetés ........................................................................................................................................ 2 1. Az elsőrendű nyelv szintaxisa ............................................................................................... 2 2. Az elsőrendű nyelv klasszikus szemantikája ....................................................................... 13 3. Logikai kalkulusok .............................................................................................................. 22 3. Helyettesítések .............................................................................................................................. 25 1. Változók helyettesítése termekkel ....................................................................................... 25 2. Illesztő helyettesítés ............................................................................................................ 35 3. Feladatok ............................................................................................................................. 46 4. Normálformák .............................................................................................................................. 48 1. Konjunktív és diszjunktív normálformák ............................................................................ 48 2. Prenex alakú formulák ........................................................................................................ 50 3. Skolem-normálforma .......................................................................................................... 53 4. Elsőrendű klózok ................................................................................................................. 58 5. Feladatok ............................................................................................................................. 59 5. Frege stílusú kalkulus ................................................................................................................... 61 1. A predikátumkalkulus ......................................................................................................... 61 2. Feladatok ............................................................................................................................. 69 6. Gentzen kalkulusai ....................................................................................................................... 70 1. A természetes levezetés ....................................................................................................... 70 2. A szekventkalkulus ............................................................................................................. 81 3. Feladatok ............................................................................................................................. 94 7. A rezolúciós kalkulus ................................................................................................................... 96 1. A Herbrand-univerzum és az elsőrendű klózhalmazok ....................................................... 96 2. Az alaprezolúció ............................................................................................................... 111 3. Az elsőrendű rezolúció ...................................................................................................... 119 4. Rezolúciós levezetési stratégiák ........................................................................................ 137 4.1. 1. A teljes szintek módszere ................................................................................. 137 4.2. 2. A törlési stratégia .............................................................................................. 138 4.2.1. Befoglalási algoritmus ............................................................................. 139 5. Feladatok ........................................................................................................................... 142 Hivatkozások .................................................................................................................................. 144

iii Created by XMLmind XSL-FO Converter.

List of Tables 3.1. ................................................................................................................................................... 33 4.1. asszociativitás ............................................................................................................................ 48 4.2. kommutativitás .......................................................................................................................... 48 4.3. disztributivitás ........................................................................................................................... 48 4.4. idempotencia .............................................................................................................................. 48 4.5. elimináció (elnyelés) .................................................................................................................. 48 4.6. De Morgan törvényei ................................................................................................................. 49 4.7. kiszámítási törvények ................................................................................................................ 49 4.8. logikai jelek közötti összefüggések ........................................................................................... 49 4.9. kétszeres tagadás ........................................................................................................................ 49 4.10. negáció az implikációban ........................................................................................................ 49 4.11. kvantoros De Morgan-törvények ............................................................................................. 51 4.12. kvantorok egyoldali kiemelése, ............................................................................................... 51 4.13. kvantorok kétoldali kiemelése ................................................................................................. 51 4.14. kvantorhatáskör-átjelölés, ........................................................................................................ 51 7.1. ................................................................................................................................................... 97 7.2. ................................................................................................................................................... 98 7.3. ................................................................................................................................................. 100 7.4. ................................................................................................................................................. 104 7.5. ................................................................................................................................................. 104 7.6. ................................................................................................................................................. 104 7.7. ................................................................................................................................................. 112 7.8. ................................................................................................................................................. 116 7.9. ................................................................................................................................................. 123 7.10. ............................................................................................................................................... 123 7.11. ............................................................................................................................................... 134 7.12. ............................................................................................................................................... 135 7.13. ............................................................................................................................................... 136 7.14. ............................................................................................................................................... 137

iv Created by XMLmind XSL-FO Converter.

Chapter 1. Előszó Informatikus hallgatók számára megkerülhetetlen a matematikai logika tanulmányozása. A felsőoktatási intézmények tantervei tartalmazzák is a logika informatikában fontos fejezeteinek oktatását. A Debreceni Egyetem Informatikai Karán már az alapképzés során tanítjuk (a logika nyelvészeti tárgyalásmódja keretei között) a logikai nyelvek szintaxisát, klasszikus szemantikáját. Mesterképzésben pedig sort kerítünk a logikai kalkulusok és a logikai programozás alapjainak megtanítására. Logika könyvek és tankönyvek sora segíti a tanulást, mégsincs könnyű dolga a hallgatónak. A tanulási folyamat során (tapasztalataink szerint) zavarja a hallgatót a különböző könyvek szóhasználatában és jelölésrendszerében való lényeges eltérés és a példák hiánya. Jelen munkában a logikai kalkulusokról a mesterképzésben elsajátítandó ismereteket foglaltuk össze. A tananyag a DE IK programtervező informatikus hallgatóinak képzése során szerzett tapasztalatokat felhasználva alakult ki. A gyökerek Dragálin Albert professzor (1941-1998) matematikai logikából és mesterséges intelligenciából az 1990-es években tartott debreceni előadásaiból indulnak. Felhasználtuk Pásztorné Varga Katalin (ELTE, egyetemi docens) 1998 és 2010 között Debrecenben tartott előadásait és a 2003-ban a jelen tankönyvírók egyikével írt monográfiáját. A példák és feladatok egy része a szerzőknek Robu Judittal (BabesBolyai Egyetem, egyetemi docens) 2010-ben írt feladatgyűjteményéből való. Természetesen felhasználtunk más, az irodalomban felsorolt forrást is. Az olvasótól elvárjuk az alapképzés során elsajátított logikai tananyag ismeretét, a logikai nyelvek szintaxisával és klasszikus szemantikájával kapcsolatos fontos fogalmak és tételek tudását. Témánkat tanulmányozhatja kizárólag ebből az anyagból, ugyanakkor erősen ajánljuk előadások látogatását, vagy az irodalomban felsorolt könyvek forgatását. Észrevételeiket szívesen vesszük a [email protected] címen. Debrecen, 2014. március 15. A tananyag összeállítói

1 Created by XMLmind XSL-FO Converter.

Chapter 2. Bevezetés Jelen tananyag olvasójáról feltesszük, hogy az elsőrendű logikai nyelv szintaxisával és klasszikus szemantikájával kapcsolatos alapvető fogalmakat és fontos tételeket ismeri. A könyvben használt fogalommegnevezések és jelölések tisztázására röviden mégis sort kerítünk. A bevezető fejezet elolvasása egyúttal segíti a korábban tanult és jelen tankönyvben szükséges logikai ismeretek felidézését is. Logikai alapozó kurzusokon gyakran a többfajtájú elsőrendű logikai nyelv kerül bevezetésre. A logikai kalkulusokat ugyanakkor most egyfajtájú nyelv segítségével tárgyaljuk, így a bevezetésben sem esik szó a többfajtájú nyelvekről.

1. Az elsőrendű nyelv szintaxisa Egy (egyfajtájú) elsőrendű logikai nyelv ábécéje először is tartalmaz ún. logikán kívüli betűket: ezeket a

(2.1)

három halmazból álló rendszerrel adjuk meg. • a nyelv konstansszimbólumainak halmaza. • Az

halmaz elemei függvényszimbólumok . Minden

-hez tartozik egy

természetes szám, az

függvényszimbólum aritása. • A

halmaz elemei predikátumszimbólumok . Minden

-hez rendelünk egy

természetes számot, a


Bevezetés

predikátumszimbólum aritását. A

aritású predikátumszimbólumot propozicionális szimbólumnak (állítás szimbólumnak) is szoktuk nevezni. Egy elsőrendű logikai nyelvben megszámlálhatóan végtelen sok (individuum)változó áll rendelkezésünkre:

(ezekre gyakran az

betűkkel hivatkozunk). Az ábécé tartalmaz még logikai jeleket: a

negáció ,

konjunkció ,

diszjunkció ,

implikáció összekötő jeleket és az

univerzális és

egzisztenciális kvantorokat . (A továbbiakban jelölje

mindig a

és a

logikai összekötő jelek valamelyikét,

pedig valamelyik kvantort.) Használhatjuk még a

zárójeleket és a vesszőt.


Bevezetés

A

ábécé feletti elsőrendű logikai nyelv termek és formulák ( logikai kifejezések ) halmaza. A nyelv termjeinek halmaza az a legszűkebb

halmaz, melynek • minden konstansszimbólum (

elemei) és változó eleme, és • ha

egy

aritású függvényszimbólum és

elemei

-nek (azaz termek), akkor az

szó is eleme

-nek (term). A nyelv formuláinak halmaza az a legszűkebb

halmaz, melynek • minden

alakú szó eleme (azaz formula, ún. atomi formula ), ha

egy


Bevezetés

aritású predikátumszimbólum és

rendre termek (elemei

-nek), továbbá • ha

és

elemei

-nek (formulák) és

változó, akkor az

alakú szavak szintén elemei

-nek (formulák). Egy elsőrendű logikai nyelvben egyetlen konstansnak és változónak sincs közvetlen résztermje , az

term közvetlen résztermjei pedig a

termek. Egy atomi formulának nincs közvetlen részformulája ,

egyetlen közvetlen részformulája

,

bal oldali közvetlen részformulája 5 Created by XMLmind XSL-FO Converter.

Bevezetés

, jobb oldali közvetlen részformulája

,

közvetlen részformulája

.(

-ban a

-re kvantoros előtagként hivatkozunk, és azt mondjuk, hogy ebben az előtagban a kvantor az

változót nevezi meg.) Egy

term résztermjeinek halmaza a legszűkebb olyan halmaz, melynek

eleme, és ha egy term eleme, akkor eleme a term összes közvetlen résztermje is. Egy

formula részformuláinak halmaza az a legszűkebb halmaz, melynek

eleme, és ha egy formula eleme, akkor eleme a formula összes közvetlen részformulája is. Konstansszimbólum és változó szerkezeti fája egyetlen, a szimbólumot tartalmazó csúcsból áll. Ez a csúcs a fa gyökere.

szerkezeti fájának gyökere

, a gyökér


Bevezetés

darab gyermeke rendre

szerkezeti fáinak gyökerei. Atomi formula szerkezeti fája egyetlen ezt a formulát tartalmazó csúcsból áll, ami a fa gyökere.


, a gyökér egyetlen gyermeke az

szerkezeti fájának gyökere.


, a gyökér bal oldali gyermeke az

, jobb oldali gyermeke a

szerkezeti fájának gyökere.


, a gyökér egyetlen gyermeke az

szerkezeti fájának gyökere. Legyenek az

és az

függvények a következők:


Bevezetés

(2.2)

(2.3)

funkcionális összetettsége ,

logikai összetettsége . Egy formulában egy logikai jel hatásköre a formulának azon részformulái közül a legkisebb logikai összetettségű, amelyekben az adott logikai jel is előfordul. Egy formula fő logikai jele az a logikai jel, melynek hatásköre maga a formula. A formulák leírásakor használhatunk rövidítéseket. Például ha néhány formulából újabbat ugyanolyan módon gyakran készítünk, a szerkesztés módjára új (összekötő) jelet vezethetünk be. A külső zárójeleket elhagyhatjuk. A logikai összekötő jelekhez, a kvantorokhoz és a bevezetett jelekhez erősorrendet rendelhetünk. Ennek megfelelően, a jelek értelmezését a formulában az alábbi – az erősebbtől a gyengébb felé haladó – sorrendnek megfelelően végezzük el: 1. kvantorok (

,

), 2. negáció (

), 3. konjunkció (

) és diszjunkció (

), 4. implikáció (


Bevezetés

), 5. bevezetett jelek. Egy formulában egy változónak kétféle előfordulását különböztetjük meg. Az

változó egy adott előfordulása az

formulában kötött , ha egy, az

-et megnevező kvantor hatáskörében van. Az

változó előfordulása szabad , ha nem kötött. Egy kvantor a kvantoros előtagban megnevezett és a hatásköre közvetlen részformulájában ennek a változónak a még szabad előfordulásait tesz kötötté (köti). Egy változóelőfordulás kötöttségének meghatározása: • Egy atomi formulában minden változó-előfordulás szabad. • Az

formulában egy változó-előfordulás pontosan akkor kötött, ha ez az előfordulás vagy

-ban van és már

-ban kötött, vagy

-ben van és már

-ben kötött. • A

formulában egy változó-előfordulás pontosan akkor kötött, ha ez az előfordulás már

-ban kötött. • A


Bevezetés

formulában

minden előfordulása kötött. Ha

egy előfordulása

-ban még szabad volt, akkor ezt az előfordulást a

formulában a

kvantor köti. Egy, az

-től különböző változó valamely előfordulása

-ban pontosan akkor kötött, ha már

-ban is kötött volt. Egy változót a formula paraméterének nevezünk, ha van a formulában szabad előfordulása. Egy

formula paramétereinek a halmazára

-val hivatkozunk. A

formulában a

kvantor által kötött

változó átnevezéséről beszélünk, amikor a


Bevezetés

kvantoros előtagban

helyett egy másik, mondjuk

változót nevezünk meg, majd

-ban az

változó minden szabad előfordulását

-ra cseréljük ki (a kapott formulát jelöljük

-nal), és így a

formulát kapjuk. A

formulából szabályosan végrehajtott kötött változó átnevezéssel kapjuk a

formulát, ha

-ban az

nem paraméter, és az

változó egyetlen

által kötött előfordulása sem tartozik egyetlen


Bevezetés

-t kötő kvantor hatáskörébe sem. Az

formula az

formula variánsa (vagy

és

egymással kongruens formulák ) ha egymástól csak kötött változók szabályosan végrehajtott átnevezésében különböznek. Jelölése:

. Annak eldöntése, hogy két formula egymás variánsa-e: • Egy atomi formula csak önmagával kongruens. • pontosan akkor, ha

és

. • pontosan akkor, ha

. • pontosan akkor, ha minden

-re, mely különbözik

és


Bevezetés

összes (kötött és szabad) változójától,

.

2. Az elsőrendű nyelv klasszikus szemantikája Egy

ábécé feletti elsőrendű logikai nyelv

interpretációját ( modelljét vagy algebrai struktúráját ) olyan

(2.4)

négyes határozza meg, melyben • az

individuumok (objektumok) nem üres halmaza (univerzuma), • a

függvény minden

konstansszimbólumhoz egy

individuumot rendel, • az

függvény minden

aritású függvényszimbólumhoz olyan


Bevezetés

függvényt rendel, melynek értelmezési tartománya

, és értékeit

-ból veszi fel, azaz

• a

függvény pedig olyan, hogy ha a

predikátumszimbólum aritása

és

, akkor

predikátum (

vagy

értéket felvevő, ún. logikai értékű függvény). Ha

propozicionális szimbólum, akkor

vagy

, vagy

.


Bevezetés

Legyen az elsőrendű nyelv univerzuma

. Bővítsük ki a nyelvet az univerzum objektumait jelölő új konstansszimbólumokkal:

(2.5)

ahol

-t a

halmazból úgy kapjuk, hogy minden

objektumhoz rendelünk egy új – általunk

-val jelölt – konstansszimbólumot. Egy olyan

(2.6)

függvényt, amely az elsőrendű nyelv véges sok változójához

-beli új szimbólumot rendel,

-értékelő helyettesítésnek nevezünk.

a

logikai kifejezés értékelése , ha

. Ha


Bevezetés

a

logikai kifejezés értékelése, akkor a

kifejezést úgy nyerjük, hogy

-ban a paraméterek minden szabad előfordulását a

által hozzájuk rendelt új konstansszimbólumokkal helyettesítjük. A kibővített nyelv paramétermentes ( zárt ) logikai kifejezéseit értékelt kifejezéseknek nevezzük. Legyen

a nyelv egy interpretációja. Egy értékelt term értéke

-ben az alábbi – rekurzív definícióval megadott –

-beli objektum. (Egy

term

-beli értékét

-mel fogjuk jelölni.) • Ha

és

, akkor

.


Bevezetés

• Ha

az

-hoz rendelt új

szimbólum, akkor

. • Ha

egy értékelt term, ahol a

termek értékei

-ben rendre

, és

, akkor

(2.7)

Egy

értékelt formula értéke

-ben (jelölése:

) a következő, rekurzív definícióval megadott érték: 17 Created by XMLmind XSL-FO Converter.

Bevezetés

• Ha

egy értékelt atomi formula, ahol a

termek értékei

-ben rendre

, és

, akkor

(2.8)

• Ha

és

értékei rendre

és

, akkor

pontosan akkor, ha

és

;


Bevezetés

pontosan akkor, ha

vagy

;

pontosan akkor, ha

vagy

. Egyébként

. • Ha

értéke

, akkor

pontosan akkor, ha

, egyébként

.

•


Bevezetés

• A

értékelt formula igaz az

interpretációban, ha

, egyébként a

formula hamis

-ben. Egy elsőrendű nyelv egy

formulája kielégíthető , ha van a nyelvnek olyan interpretációja és

-nak olyan

értékelése, amely mellett

igaz, egyébként

kielégíthetetlen (vagy logikai ellentmondás ). Egy elsőrendű nyelv egy

formulája logikai törvény , ha a nyelv bármely interpretációjában és

bármely

értékelése mellett 20 Created by XMLmind XSL-FO Converter.

Bevezetés

igaz. Jelölése:

. Az

és

elsőrendű formulák logikailag ekvivalensek , ha a nyelv minden

interpretációjában és a formulák minden közös

értékelése mellett

és

azonos igazságértékű. Jelölése:

. Legyen

elsőrendű formulák (premisszák) egy halmaza és

egy elsőrendű formula (konklúzió). Azt mondjuk, hogy

következménye a

-beli formuláknak, ha a nyelv minden olyan interpretációjában és a

-beli és a


Bevezetés

formulák tetszőleges olyan közös

értékelése esetén, mely mellett a

-beli formulák mind igazak, ott

is igaz. Jelölése:

Elsőrendű formulák egy

halmaza kielégíthető , ha van olyan interpretáció és a

-beli formuláknak olyan közös értékelése, mely mellett minden

-beli formula épp igaz, egyébként a

formulahalmaz kielégíthetetlen .

3. Logikai kalkulusok A logika fő feladata a következtetések helyességének vizsgálata és helyes következtetési szabályok megalkotása. Az előző szakaszban fel is idéztük a következményrelációnak a klasszikus elsőrendű logika szemantikai alapfogalmaira támaszkodó definícióját. Ugyanakkor ez a definíció nem ad gyakorlati útmutatást arra vonatkozóan, hogyan ellenőrizhetjük egy következtetés helyességét. Jelen tananyagban több olyan mechanikus, csak a logikai nyelv szintaxisát használó szabályrendszerrel ismerkedünk meg, melyek gépiesen alkalmazhatók a következményreláció vizsgálatára. Leibniz már a XVIII. század elején remélte, hogy a tudósok hosszas viták helyett hamarosan ki fogják tudni számolni, kinek van igaza. Az elképzelés megvalósítása felé az első lépések mégis csak a XIX. század végén indultak. Frege ekkor dolgozott ki egy tisztán szintaktikai felépítésű logikai rendszert, egy logikai kalkulust . Egy logikai kalkulus a logikai nyelv megadása mellett a ,,szintaktikai következményreláció'', a levezethetőség definícióját tartalmazza. Ehhez első lépésben megadjuk a kalkulus alapformuláit és levezetési szabályait . A második lépés a levezethetőség fogalmának kialakítása. Egy

formulahalmazból levezethető a


Bevezetés

formula (jelölése:

) • ha

alapformula, vagy

, • illetve ha van olyan levezetési szabály, mely

-t előállítja, és az(ok) a formula(ák), amely(ek)ből ez a levezetési szabály

-t előállítja, az(ok)

-ból levezethető(ek). A levezethetőségi relációt tehát az alapformulák és a levezetési szabályok segítségével definiáljuk. Tehát ha változtatunk az alapformulákon vagy a levezetési szabályokon, más lesz a levezethetőségi reláció is. Sokféle logikai kalkulust felépíthetünk. Két kalkulust akkor tekintünk ekvivalensnek , ha azonos logikai nyelvhez kötődnek, és pontosan akkor lesz

az egyikben, amikor a másikban is. Egy elsőrendű logikai nyelv klasszikus szemantikájában definiált következményreláció és a nyelvre épülő valamely logikai kalkulus levezethetőségi relációja között szoros kapcsolatot várunk el. Azt mondjuk, hogy a logikai kalkulus helyes , ha

esetén mindig

. A logikai kalkulus pedig teljes , ha

esetén mindig

. Egy kalkulus adekvát , ha helyes is, teljes is.


Bevezetés

Egy logikai rendszer megalkotásakor gyakran először egy szemantikai rendszert definiálunk, majd megkísérlünk ehhez legalább helyes, de ha lehet, adekvát logikai kalkulust szerkeszteni.


Chapter 3. Helyettesítések 1. Változók helyettesítése termekkel Definíció Egy olyan függvényt, amely az elsőrendű nyelv véges sok változóján van értelmezve, és minden változóhoz termet rendel, termhelyettesítésnek nevezünk. Üres a termhelyettesítés, ha az értelmezési tartománya üres (jele:

). Ha a

termhelyettesítés értelmezési tartománya

és

minden

-ra

,

-t megadhatjuk a

(3.1)

táblázattal vagy a

felsorolással.

jelölje azt a termhelyettesítést, melyre


Helyettesítések

és minden

esetén

. Vezessük be továbbá a

jelölést a

kifejezés szerkezetétől és a

termhelyettesítéstől függő logikai kifejezésre: 1. ha

, akkor

, 2. ha

változó, akkor

, 3. , 4. , 5. , 6.


Helyettesítések

, 7. . Vegyük észre, hogy az értékelő helyettesítések is termhelyettesítések, és ha

a

kifejezés értékelése, a

kifejezés éppen a

-beli paraméterek szabad előfordulásainak a

-val hozzájuk rendelt konstansszimbólumokkal való helyettesítésnek eredményeképpen kapott értékelt kifejezés. Ugyanakkor nem minden

kifejezés és

termhelyettesítés esetén lesz alkalmas

a logika céljai számára. Hogy csak ezekkel a

kifejezésekkel foglalkozhassunk, vezessünk be néhány fogalmat. A

termhelyettesítés megengedett a

kifejezés számára, ha minden

esetén


Helyettesítések

minden

-beli szabad előfordulása kívül esik a

term valamennyi változóját megnevező kvantor hatáskörén. Definíció

megengedettsége

számára

szerkezete szerint: 1. Termek és atomi formulák számára minden termhelyettesítés megengedett. 2. számára egy termhelyettesítés megengedett, ha megengedett

számára. 3. számára egy termhelyettesítés megengedett, ha megengedett

és

számára is. 4. számára egy

termhelyettesítés megengedett, ha a. egyetlen

változó esetén sem fordul elő


Helyettesítések

a

termben, b. pedig megengedett

számára. Példa A

formula számára az

(3.2)

termhelyettesítés megengedett, az

(3.3)

termhelyettesítés pedig nem megengedett, mert a helyettesítendő szabad előfordulású

az

-et kötő

hatáskörében van, és a helyére beírandó

termben is előfordul az

változó.


Helyettesítések

Legyen

egy kifejezés és

egy termhelyettesítés. Konstruáljunk meg egy

-val kongruens olyan

formulát, amely számára

megengedett. Ekkor a

kifejezés a

termhelyettesítés

-ban való szabályos végrehajtásának eredménye. Jelölése:

. Definíció

meghatározása

szerkezete szerint: 1. Ha

term vagy atomi formula, akkor

. 2. 30 Created by XMLmind XSL-FO Converter.

Helyettesítések

3. 4. a. Ha egyetlen

változó esetén sem fordul elő a

termben

, akkor

. b. Ha van olyan

változó, hogy

paraméter

-ben, akkor válasszunk egy új változót – például

-t –, mely nem fordul elő sem

-ban, sem

termjeiben, és

(3.4)

Példa A

formulában az 31 Created by XMLmind XSL-FO Converter.

Helyettesítések

(3.5)

termhelyettesítés szabályos végrehajtásának eredménye a

(3.6)

formula. Definíció Legyenek

(3.7)

egy nyelv termhelyettesítései.

és

kompozícióján a

(3.8)

termhelyettesítést értjük, ahol

(3.9)

Példa Legyenek

(3.10)

termhelyettesítések. Ekkor


Helyettesítések

(3.11)

és

(3.12)

A példa mutatja, hogy a kompozíció művelete egy nyelv termhelyettesítéseinek halmazán nem kommutatív. Tétel Egy elsőrendű logikai nyelv tetszőleges

,

és

termhelyettesítései esetén

Table 3.1. (a kompozíció asszociatív)

(1) (2)

(

neutrális elem) Azaz a kompozíció műveletével a termhelyettesítések halmaza neutrális elemmel rendelkező félcsoport. Lemma Legyenek

és

egy nyelv termhelyettesítései. Ekkor tetszőleges

logikai kifejezés esetén


Helyettesítések

(3.13)

Definíció Legyenek

és

termhelyettesítések. Az

helyettesítés általánosabb a

-nál, ha van olyan

termhelyettesítés, hogy

. Példa Az

(3.14)

helyettesítések esetén

általánosabb a

helyettesítésnél, mert

, ahol

(3.15)


Helyettesítések

2. Illesztő helyettesítés Definíció Legyen

és

két azonos predikátumszimbólummal kezdődő atomi formula. Az olyan

termhelyettesítést, amelyre

(3.16)

-t és

-t egymáshoz illesztő helyettesítésnek nevezzük.

az

és

atomok legáltalánosabb illesztő helyettesítése , ha

és

minden illesztő helyettesítésénél általánosabb. Példa A

és a

atomoknak egy illesztő helyettesítése:


Helyettesítések

(3.17)

legáltalánosabb illesztő helyettesítése:

(3.18)

Az illesztő helyettesítés fogalmát kiterjeszthetjük:

legyen az azonos predikátumszimbólummal kezdődő

(

) atomi formulák halmaza.

illesztő helyettesítése

minden atompárját illeszti egymáshoz. Definíció Vizsgáljuk

elemeit párhuzamosan, szimbólumonként balról jobbra haladva. Álljunk meg annál az első szimbólumnál, amelyik nem minden atomban egyezik meg. Az ezen a pozíción kezdődő résztermek

halmazát

különbségi halmazának nevezzük. Példa Legyen

(3.19)


Helyettesítések

különbségi halmaza

(3.20)

Robinson algoritmusa véges sok lépésben meghatározza

legáltalánosabb illesztő helyettesítését, ha van ilyen, illetve jelzi, ha nem illeszthetők egymáshoz

atomjai. 1. ,

,

. 2. Ha

egyetlen atomot tartalmaz, akkor sikeresen vége:

a

legáltalánosabb illesztő helyettesítése. Egyébként határozzuk meg

különbségi halmazát:

-t. 3. Ha van

-ban olyan


Helyettesítések

változó és

term, hogy

nem fordul elő

-ban, akkor a 4. lépéssel folytatjuk. Egyébként

atomjai nem illeszthetők egymáshoz. Vége. 4. ,

. (Megjegyezzük, hogy

.) 5. , és a 2. lépéssel folytatjuk. Példa Döntsük el az illesztő algoritmussal, hogy illeszthetők-e a

(3.21)

halmaz atomi formulái egymáshoz. 1. ,

. 2. .


Helyettesítések

3. egy változó,

egy, a

-t nem tartalmazó term. 4. .

(3.22)

5. 6. egy változó,

egy, az

-et nem tartalmazó term. 7. .

(3.23)

8. . 9.


Helyettesítések

egy változó,

egy, az


(3.24)

11. -ban egyetlen atom van, így

a legáltalánosabb illesztő helyettesítés

-re. Példa Vizsgáljuk meg, hogy illeszthetők-e egymáshoz a

(3.25)

halmaz atomi formulái. 1. ,

. 2. . 3. 40 Created by XMLmind XSL-FO Converter.

Helyettesítések

egy változó,

egy, az


(3.26)

5. . 6. A

-ben nincs változó, ezért az algoritmus azzal az eredménnyel fejeződik be, hogy

atomjai nem illeszthetők. Az illesztő helyettesítés fogalmát másképp is általánosíthatjuk:

legyen az

(3.27)

páronként azonos predikátumszimbólummal kezdődő atomi formulák halmaza. Keressük a minden pár atomjait egymáshoz illesztő helyettesítést. Képezzük a

-beli párok atomjaiból a

(3.28)


Helyettesítések

formális egyenlőséghalmazt. A formális egyenlőséghalmazba bizonyos szabályok alapján bekerülhetnek termek formális egyenlőségei, illetve ki is kerülhetnek a halmazból formális egyenlőségek. Egy csupa változó - term párokból álló

(3.29)

formális egyenlőséghalmaz kiszámított alakú , ha

, amikor

, és

(

). Az előbbi kiszámított alakú formális egyenlőséghalmaz által meghatározott termhelyettesítés

(3.30)

Herbrand algoritmusa véges sok lépésben meghatározza

legáltalánosabb illesztő helyettesítését, ha van ilyen, illetve jelzi, ha nem illeszthetők egymáshoz

párjainak atomjai. 1. ,

. 2. Ha

kiszámított alakú, akkor sikeresen vége: az általa meghatározott helyettesítés

legáltalánosabb illesztő helyettesítése. Egyébként válasszunk ki egy


Helyettesítések

formális egyenlőséget

-ból. 3. . 4. Ha

alakja • , ahol

változó, vagy

, ahol

konstansszimbólum, akkor tovább az 5. lépésre. • , ahol

változó,

összetett term,

. • , ahol

konstansszimbólumok, akkor


Helyettesítések

atomjai nem illesztők egymáshoz. Vége. • , ahol

függvényszimbólumok, akkor


függvényszimbólum, vagy

, ahol

predikátumszimbólum, akkor

. • , ahol

, akkor


, akkor


Helyettesítések

formális egyenlőségeiben elvégezzük az

helyettesítést, majd

. 5. , és a 2. lépéssel folytatjuk. Példa Döntsük el Herbrand algoritmusával, hogy illeszthetők-e a

(3.31)

halmaz atomi formulái egymáshoz.

(3.32)

Kiszámított alakú formális egyenlőséghalmazt kaptunk, így a legáltalánosabb illesztő helyettesítés

-re:

. Példa Döntsük el Herbrand algoritmusával, hogy illeszthetők-e a


Helyettesítések

(3.33)

halmaz atomi formulái egymáshoz.

(3.34)

3. Feladatok 1. Határozzuk meg, hogy mely helyettesítések megengedettek a következő formula számára, majd végezzük el a szabályos helyettesítést.

(3.35)

(3.36)

2. Bizonyítsuk be, hogy • ha a

kifejezésben nincs

-beli változókat megnevező kvantor, akkor

megengedett

számára. • ha a

helyettesítő termekben nincs változó, akkor


Helyettesítések

megengedett minden kifejezés számára. 3. Határozzuk meg az alábbi termhelyettesítések kompozícióját.

a. és

b. és

4. Döntsük el Robinson és Herbrand algoritmusaival, hogy illeszthetők-e a következő halmazok atomi formulái egymáshoz. • • • • • • 5. Határozzuk meg, hogy amikor a Robinson-algoritmus véget ér, milyen összetettségűek lesznek a

(3.37)

halmaz egymáshoz illesztett atomjaiban a termek. 6. Írjunk programot, amely Herbrand vagy Robinson algoritmusát alkalmazva megkeresi egy atomhalmaz legáltalánosabb illesztő helyettesítését.


Chapter 4. Normálformák 1. Konjunktív és diszjunktív normálformák Definíció Az atomi formulákat és a negáltjaikat literáloknak nevezzük. Elemi konjunkciónak tekintünk minden literált, továbbá egy elemi konjunkció és egy literál konjunkcióját. Elemi diszjunkciók szintén a literálok, továbbá egy elemi diszjunkció és egy literál diszjunkciója. A konjunktív normálformájú formula egy elemi diszjunkció, vagy egy konjunktív normálforma és egy elemi diszjunkció konjunkciója, a diszjunktív normálformájú formula egy elemi konjunkció, vagy egy diszjunktív normálforma és egy elemi konjunkció diszjunkciója. Tétel Az elsőrendű logikai nyelv minden kvantormentes formulájához konstruálható vele logikailag ekvivalens konjunktív és diszjunktív normálformájú formula. Definíció Egy formulával ekvivalens konjunktív normálformájú formulát a formula konjunktív normálformájának , a vele ekvivalens diszjunktív normálformájú formulát a formula diszjunktív normálformájának nevezzzük. A normálformára hozás lépései: 1. A logikai jelek közötti összefüggések alapján a formulába minden implikációs részformula helyett vele ekvivalens diszjunkciót írunk. 2. De Morgan törvényeivel elérjük, hogy negáció csak atomi formulákra vonatkozzon. 3. A disztributivitást felhasználva addig alakítjuk a formulát, hogy a konjunkciók és diszjunkciók megfelelő sorrendben kövessék egymást. 4. Végül esetleg egyszerűsítünk. Felhasználható ekvivalenciák:

Table 4.1. asszociativitás

Table 4.2. kommutativitás

Table 4.3. disztributivitás

Table 4.4. idempotencia

Table 4.5. elimináció (elnyelés)


Normálformák

Table 4.6. De Morgan törvényei

Table 4.7. kiszámítási törvények (

)

Table 4.8. logikai jelek közötti összefüggések

Table 4.9. kétszeres tagadás

Table 4.10. negáció az implikációban

Példa Hozzuk a

(4.1)

formulát normálformára. 1. Eltávolítjuk az implikációkat:


Normálformák

(4.2)

2. Elérjük, hogy negáció csak atomokra vonatkozzon:

(4.3)

3. Felhasználjuk a disztributivitást; az eredmény konjunktív normálforma:

(4.4)

4. Egyszerűsítünk:

(4.5)

5. Tovább egyszerűsítünk; az eredmény egyszerre konjunktív és diszjunktív normálforma:

(4.6)

2. Prenex alakú formulák Definíció Egy

alakú formulát, ahol a

kvantormentes formula, prenex alakú formulának nevezünk.

a prenex alakú formula magja . Példa A

,a

és a


Normálformák

formulák prenexformulák, viszont a

formula nem prenexformula. Tétel Egy elsőrendű logikai nyelv tetszőleges formulájához konstruálható vele logikailag ekvivalens prenex alakú formula. Definíció Egy formulával ekvivalens prenex alakú formula a formula prenex alakja. A prenex alakra hozás lépései: 1. A formulában a kötött változók szabályos átnevezésével elérjük, hogy a kötött változók nevei különbözzenek a formula paramétereitől, és bármely két különböző kvantor más-más változót nevezzen meg a kvantoros előtagban. Az így nyert, az eredeteivel kongruens, így az eredetivel ekvivalens formulát az eredeti változóiban tiszta alakjának nevezzük. 2. Alkalmazzuk De Morgan kvantoros törvényeit és a kvantorkiemelésre vonatkozó logikai törvényeket, amíg a formulánk prenex alakú nem lesz. Felhasználható ekvivalenciák:

Table 4.11. kvantoros De Morgan-törvények

Table 4.12. kvantorok egyoldali kiemelése,

Table 4.13. kvantorok kétoldali kiemelése

Table 4.14. kvantorhatáskör-átjelölés,


Normálformák

Példa Hozzuk a

(4.7)

formulát prenexalakra. 1. Változóiban tiszta alakra hozás:

(4.8)

2. De Morgan törvényeinek alkalmazása:

(4.9)

3. Kvantorkiemelés:

(4.10)

4. Kvantorkiemelés:

(4.11)

Ha a magot normálformára akarjuk hozni, akkor célszerű előbb eltüntetni az implikációkat, és a negációkat az atomi formulák elé vinni. Ekkor (újabb) lehetőségek adódhatnak a kvantorok kétoldali kiemelésére vonatkozóan. 1. Az implikációk átírása:

(4.12)


Normálformák

2. A kétszeres tagadás és De Morgan törvényeinek alkalmazása:

(4.13)

3. Az egzisztenciális kvantor kétoldali kiemelésére vonatkozó ekvivalencia alkalmazása:

(4.14)

4. Változóiban tiszta alakra hozás:

(4.15)

5. Most már mindegyik kvantor kiemelhető:

(4.16)

6. A formula magja diszjunktív normálforma, de átírható konjunktív normálformába, ha az a további feldolgozás szempontjából úgy célszerű:

(4.17)

3. Skolem-normálforma A

prenexformulában csak univerzális kvantorok vannak. Az ilyen

alakú formulák fontosak lesznek később. Definíció Univerzális Skolem-formulának nevezzük az olyan prenexformulát, amelynek a prefixumában csak univerzális kvantor szerepel. Ha a Skolem-formula magja konjunktív normálforma, akkor a formulát Skolemnormálformának nevezzük. Tétel Tetszőleges


Normálformák

formulához konstruálható olyan univerzális Skolem-formula, mely pontosan akkor kielégíthetetlen, ha

kielégíthetetlen. Prenexformula ,,átírása'' univerzális Skolem-formába: 1. Új Skolem-szimbólumok bevezetése: A

(4.18)

prenexformula prefixumában legyen az első egzisztenciális kvantor a

-edik kvantor. • Ha

, akkor minden olyan interpretációban és

értékelés esetén (

), amely mellett

igaz, az interpretáció

univerzumában van legalább egy

( Skolem-konstans ), hogy a

formula igaz lesz. Ez azt jelenti, hogy ha kibővítjük az elsőrendű nyelvünket egy új

konstansszimbólummal, akkor az előbbi interpretációt kiegészítve azzal, hogy

-t egy Skolem-konstanssal interpretáljuk, az új, bővebb nyelv olyan interpretációját kapjuk, melyben


Normálformák

is igaz. • Legyen most

. Egy

interpretációban valamely

értékelés mellett (

)a

(4.19)

formula pontosan akkor igaz, ha az

változókat bármilyen – az interpretáció univerzumából vett – elemekkel értékelve mindig van legalább egy elem

-ban, amellyel pedig az

változót értékelve a

formula igaz. Azaz minden

elem

-eshez tartozik legalább egy

, hogy


Normálformák

(4.20)

igaz. Legyen

(4.21)

egy függvény, amely minden

-hez egy ilyen

értéket rendel. Ezt a függvényt Skolem-függvénynek nevezzük. Bővítsük ki az elsőrendű nyelvünket egy új

aritású

függvényszimbólummal. Ha most az

interpretációt úgy egészítjük ki, hogy

-et egy ilyen Skolem-függvénnyel interpretáljuk, az új, bővebb nyelv olyan interpretációját kapjuk, melyben a

(4.22)

formula igaz. 2. Az egzisztenciális kvantor elhagyása:

prefixumából elhagyjuk a

kvantoros előtagot, és a formula magjában elvégezzük az

, illetve az


Normálformák

termhelyettesítést. A kapott

(4.23)

illetve

(4.24)

formula az eredeti formulában szereplő első egzisztenciális kvantort már nem tartalmazza. Ezzel a lépéssel az eredeti formulával a kielégíthetőség szempontjából egyenértékű formulát kaptunk a kibővített nyelvben. a. Egyrészt minden olyan interpretációban, amelyben az eredeti formula valamely értékelés mellett igaz volt, az új függvényszimbólumot (konstansszimbólumot) interpretálhatjuk egy Skolem-függvénnyel (Skolemkonstanssal) úgy, hogy az értékelés mellett igaz lesz az átalakított formula is. b. Ha pedig az eredeti formula minden interpretációban, minden értékelés mellett hamis volt, azaz kielégíthetetlen, akkor az átalakított formula is az lesz, mivel ekkor nincs Skolem-függvény (konstans) egyetlen interpretáló struktúrában sem. 3. Az új Skolem-szimbólumok bevezetésének és a kvantoreliminálásnak a lépéseit végrehajtjuk a soron következő egzisztenciális kvantorra, amíg minden egzisztenciális kvantort el nem hagytunk. Példa Írjuk át Skolem-normálformába a

(4.25)

prenex-konjunktív formulát. A két egzisztenciális kvantor a prefixum első két kvantora, ezért két Skolemkonstansszimbólumot kell bevezetnünk. Jelöljük az

-tól különböző két új konstansszimbólumot

és

-vel.


Normálformák

(4.26)

4. Elsőrendű klózok Definíció Az elsőrendű klóz pedig egy olyan zárt univerzális Skolem-formula, amelynek a magja elemi diszjunkció. Egy Skolem-normálforma magja konjunktív normálforma. Ha egy zárt

Skolem-normálformára ,,visszafelé'' alkalmazzuk a konjunkcióra vonatkozó kétoldali kvantorkiemelési szabályt, akkor elsőrendű klózok konjunkcióját kapjuk.

legyen ezen klózok halmaza. Világos, hogy

pontosan akkor kielégíthetetlen, ha

kielégíthetetlen. Példa Az előző példában kapott Skolem-normálformában alkalmazzuk a kvantorkiemelésre vonatkozó ekvivalenciát ,,visszafelé'':

(4.27)

Hozzuk a formulát változóiban tiszta alakra:

(4.28)

Mivel egy elsőrendű klóz minden változója univerzálisan kvantált, az elsőrendű klózhalmazokban a klózok prefixumait nem tüntetjük fel. Tehát a fenti elsőrendű klózhalmazt így adjuk meg:


Normálformák

(4.29)

Példa Írjuk át Skolem-normálformába a

(4.30)

prenexformulát. Először írjuk át a formula magját konjunktív normálformába:

(4.31)

A Skolem-függvények függvényszimbólumot:

egyváltozósak,

vezessünk

be

az

elsőrendű

nyelvbe

jelölésükre

két

új

-et és

-t. A Skolem-normálforma:

(4.32)

Elsőrendű klózok konjunkciójaként felírva a formulát:

(4.33)

A változóiban tiszta elsőrendű klózhalmaz pedig:

(4.34)

5. Feladatok 1. Hozzuk konjunktív és diszjunktív normálformára a következő formulákat. a. 59 Created by XMLmind XSL-FO Converter.

Normálformák

b. c. d. 2. Határozzuk meg az alábbi formulák prenex alakját. a. b. c. d. 3. Írjunk olyan programot, amelyik előállítja egy elsőrendű formula prenex alakját. 4. Határozzuk meg az alábbi formulák univerzális Skolem-normálformáját. a. b. c. d.


Chapter 5. Frege stílusú kalkulus A modern logika egyik első nagy eredménye Gottlob Frege (1848-1925) német matematikus logikai rendszere. Bár Frege a rendszere felépítése során minden lépést szemantikai okokkal indokolt, nem hozott létre olyan szemantikai felépítést logikájához, mint amit a Bevezetésben megadtunk. Frege logikai rendszere szintaktikai felépítésű rendszer, kalkulus volt. A fejezetben egy a Frege rendszeréhez stílusában hasonló predikátumkalkulust mutatunk be.

1. A predikátumkalkulus Definíció Az

,

és

szimbólumok. • A predikátumkalkulusalapsémái : 1. 2. 3. 4. 5. 6. 7. 8. 9. 10. 11. 12. 13. 14.


Frege stílusú kalkulus

• A predikátumkalkuluslevezetési szabályai :

(5.1)

Ha az

és

szimbólumokat egy elsőrendű logikai nyelv formuláival helyettesítjük,

a nyelv változója,

pedig term, akkor az alapsémákból alapformulákat kapunk, a levezetési szabályok segítségével pedig egy vagy két (vonal feletti) formulából levezetünk egy (vonal alatti) harmadikat. Tétel • A predikátumkalkulus alapformulái logikai törvények. •

. • Ha

és

akkor

Definíció A fomulafa és magasságának induktív definíciója: 1. Minden

formula 62 Created by XMLmind XSL-FO Converter.


magasságú formulafa, melyben

alsó formula, és nincs nála feljebb levő formula. 2. Ha

és

magasságú olyan formulafák, melyben az alsó formulák

és

alakúak, akkor az

(5.2)

alakzat is formulafa. A nyert formulafában

az alsó formula, melynél

és

minden formulája feljebb van. A formulafa magassága pedig

. 3. Ha



magasságú olyan formulafa, amelyben az alsó formula

, akkor az

(5.3)

alakzat is formulafa.

alsó formula, melynél

minden formulája feljebb van, és a formulafa magassága

. 4. Minden formulafa az 1–3. szabályok véges sokszori alkalmazásával áll elő. A formulafában azok a formulák, melyeknél nincs feljebb levő, vagy alapformulák, vagy ún. hipotézisek . Definíció A levezetésfa egy formulafa, melyben ha

-ból az általánosítás szabályával akarjuk a

-t nyerni, akkor

nem paraméter egyetlen, a

-nál feljebb levő hipotézisben sem. Példa Jellemezzük az alábbi formulafát:



magasságú formulafa alsó formula:

alapformula:

hipotézis:

Definíció A

véges formulahalmazból az

formula levezethető , ha van olyan levezetésfa, melyben

alsó formula, és a hipotésisek mind elemei

-nak. (Jelölése

, az alakzat neve szekvencia .) Ha

üres, akkor

hipotézismentesen vezethető le a kalkulusban (jelölése

). Példa Bizonyítsuk be, hogy

.



Tétel [A predikátumkalkulus helyessége.] Ha

, akkor

. Bizonyítás A

szekvenciát megalapozó levezetésfa magassága szerinti indukcióval bizonyítunk. Legyen a levezetésfa magassága

. 1. esetén • vagy alapformula

, ekkor

, így nyilván

is. • vagy

, azaz hipotézis, ekkor minden olyan interpretációban és értékelés mellett, amikor minden hipotézis igaz, nyilván

is igaz, tehát

. 2. Az indukciós feltevésünk szerint legyen igaz az állítás minden

-nél nem magasabb levezetésfa esetén.



3. Legyen most

. Ha a

szekvenciát megalapozó levezetésfát • a modus ponens levezetési szabállyal nyertük: a

és

szekvenciákat megalapozó, legfeljebb

magasságú levezetésfákból. Az indukciós feltevés miatt ekkor igaz az állítás, tehát

és

. De minden olyan interpretációban és értékelés mellett, amikor a

-beli hipotézisek mind igazak, ezek szerint igazak ezen interpretációkban és értékelések mellett az

és az

formula is, így a

formula is. Tehát

is. • az általánosítás szabályával nyertük,

tehát



alakú: az

magasságú levezetésfa, amiből nyertük, a

szekvenciát alapozza meg, ahol

. Az indukciós feltevés miatt ekkor igaz az állítás, tehát

. De minden olyan interpretációban és értékelés mellett, amikor a

-beli hipotézisek mind igazak, ezek szerint igaz ezen interpretációkban és értékelések mellett az

is. Mivel

,a

-beli formulákat igazzá tevő értékelésekben

-et bárhogy lehet értékelni, így az

is

bármilyen értékelése esetén igaz, tehát a

is. Ezért

. Ezzel a tételt bebizonyítottuk. Tétel [A predikátumkalkulus teljessége.] Ha



, akkor

. A tétel legismertebb bizonyítását Leon Henkin (1921-2006) amerikai matematikus adta meg (ez például [Smullyan]-ben is megtalálható).

2. Feladatok 1. Bizonyítsuk be, hogy

. 2. Bizonyítsuk be, hogy

.


Chapter 6. Gentzen kalkulusai A predikátumkalkulusban egy levezetés megkonstruálása gyakran nagyon kényelmetlen. Egyszerű formulák levezetése is lehet hosszadalmas, ráadásul a levezetések nem nagyon hasonlítanak a szokásos érvelésekre. 1934ben Gerhart Gentzen (1909-1945) német logikus olyan levezetési rendszert dolgozott ki, mely szabályai a Frege stílusú kalkulusokénál jóval közelebb állnak a gyakorlatban használt érvelés lépéseihez. Gentzen saját rendszerét a Frege stílusú rendszerekkel szembeállítva a természetes levezetés kalkulusának nevezte. Tágabb értelemben természetes levezetési rendszereknek szokták nevezni a Gentzen eredeti kalkulusához közel álló, de azzal nem tökéletesen megegyező levezetési rendszereket is. Ezek közös jellemzője, hogy bár használhatnak alapformulákat is, alapvetően mégis levezetési szabályokra épülnek. Most megadjuk a klasszikus elsőrendű logika egy olyan természetes levezetési rendszerét, mely nagyon közel áll Gentzen eredeti kalkulusához. A predikátumkalkulushoz hasonlóan ez a rendszer is helyes és teljes, tehát bizonyos értelemben sem nem több, sem nem kevesebb annál. Az alapvető különbség a hipotézisektől a levezetendő formuláig való eljutás módjában áll. Hogy megkönnyítsük a levezethetőségi reláció fennállásának igazolását, levezetési sémákra vonatkozó segédszabályok egy egész rendszerére támaszkodunk. A segédszabályok állításokat jelölnek: ha adva van(nak) a vonal feletti szekvenciá(ka)t megalapozó predikátumkalkulusbeli levezetésfa(ák), akkor megkonstruálható a vonal alatti szekvenciát megalapozó levezetésfa is. Segítségükkel a predikátumkalkulusbeli levezethetőség igazolható a levezetés tényleges megkonstruálása nélkül. Továbbá a természetes levezetés technikájának szabályai szoros analógiát mutatnak a matematikai érvelés gyakorlatával, ami megkönnyíti a szekvenciák igazolását. A természetes levezetés technikája mellett Gentzen kidolgozott egy másik - ún. szekventekkel dolgozó kalkulust is. A szekventkalkulus is igen kényelmesen használható, mivel a levezetési szabályok egyszerűen és a levezetendő szekventben szereplő formulák szerkezete által meghatározott sorrendben alkalmazhatók.

1. A természetes levezetés Definíció Az

,

és

szimbólumok. • Az azonosság törvénye

(6.1)

• Strukturális szabályok


Gentzen kalkulusai

(6.2)

• Logikai szabályok

(6.3)

(6.4)

Ha az 71 Created by XMLmind XSL-FO Converter.

Gentzen kalkulusai

és a

szimbólumokat elsőrendű formulákkal, a

és

szimbólumokat formulák multihalmazaival helyettesítjük,

a nyelv változója és

term, akkor predikátumkalkulusbeli levezethetőségre vonatkozó állításokat nyerünk. Az azonosság törvénye – egyedül itt nincs vonal – például azt állítja, hogy bármely

formulahalmazból és az

formulából mint hipotézisekből levezethető a predikátumkalkulusban

. Az állítás bizonyítása egyszerű: egyetlen formulából, az

-ból álló levezetésfa bizonyítja. A strukturális szabályok igazolása is nagyon egyszerű. A bővítés és a szűkítés szabálya esetén a vonal feletti szekvenciát megalapozó levezetés egyúttal a vonal alatti szekvenciát megalapozó levezetés is. A vágás szabályát a dedukció-tétel részletes bizonyítása után vizsgáljuk meg. Tétel [Dedukció-tétel.] Ha

akkor

Bizonyítás A



Gentzen kalkulusai

. 1. esetén • vagy alapformula

, vagy

, ekkor

így

• vagy

. De ekkor

2. Az indukciós feltevésünk szerint legyen igaz az állítás minden

-nél nem magasabb levezetésfa esetén. 3. Legyen most

. Ha a

szekvenciát megalapozó levezetésfát • a modus ponenssel nyertük

és



Gentzen kalkulusai

magasságú levezetésfákból. Az indukciós feltevés miatt ekkor igaz az állítás, tehát

és

.

Tehát

• az általánosítás szabályával nyertük,

tehát

alakú. Az

magasságú levezetésfa, amiből nyertük, a

szekvenciát alapozza meg, ahol

. Az indukciós feltevés miatt ekkor igaz az állítás, tehát

.


Gentzen kalkulusai

Tehát

Ezzel a tételt bebizonyítottuk. A vágás szabályára visszatérve: a dedukciós tétel szerint ha

, akkor

. Ekkor viszont a

-t és a

-t igazoló levezetések konkatenációja megalapozza

-t. A logikai szabályok igazolása sem nehéz. Néhány szabály bizonyításának ötletét vázoljuk. 1. Az implikáció bevezetésének szabálya épp a dedukciós tétel. 2. Az implikáció eltávolításának a szabálya: Ha adottak a

és a

állításokat megalapozó levezetések, a kettő konkatenációja után alkalmazható a modus ponens, és így épp

-nek egy, a

-ból való levezetését állítottuk elő.


Gentzen kalkulusai

3. A diszjunkció bevezetése: Ha adott

-ból

-nak a levezetése, akkor az

alapformulát beírva a levezetésbe alkalmazhatjuk a modus ponenst, és máris megkaptuk a

-ból az

egy levezetését. 4. A diszjunkció eltávolítása: Ha adottak a

és a

állításokat megalapozó levezetések, akkor a dedukciós tétel miatt elkészíthető a

és a

állításokat megalapozó levezetések is. Ezt a két levezetést konkatenáljuk, és írjuk le az

(6.5)

alapformulát. Kétszer alkalmazva a modus ponenst megalapoztuk, hogy

. Írjuk be a levezetésbe a vonal alatti szekvenciából az

hipotézist, és ha most újból alkalmazzuk a modus ponenst, megkapjuk a

-t megalapozó levezetést. 5. Az univerzális kvantor bevezetésének szabálya éppen az általánosítás szabálya. 76 Created by XMLmind XSL-FO Converter.

Gentzen kalkulusai

6. Az univerzális kvantor eltávolításának szabálya: Ha adott a

szekvenciát megalapozó levezetés, akkor a

alapformulát beírva a levezetésbe alkalmazhatjuk a modus ponenst, és máris megkaptuk

egy levezetését

-ból. 7. Az egzisztenciális kvantort bevezető szabály: Ha adott a

szekvenciát megalapozó levezetés, akkor írjuk be az

alapformulát a levezetésbe, és alkalmazzuk a modus ponenst. Így

-ból levezettük

-t. 8. Az egzisztenciális kvantor eltávolításásának szabálya: A

szekvenciát megalapozó levezetésből a dedukciós tétel miatt elkészíthető a

szekvenciát megalapozó levezetés is. Ebből az általánosítás szabálya miatt – mivel

–

adódik. Ha most a levezetésbe beírjuk a

alapformulát (lényeges, hogy


Gentzen kalkulusai

), alkalmazhatjuk a modus ponenst. Ezzel megkapjuk a

egy levezetését

-ból. A dedukciós tétel újbóli alkalmazásával pedig igazoltuk, hogy

. A gyakorlatban a természetes technikai szabályokat inkább ,,alulról felfelé'' szoktuk alkalmazni: amikor igazolni kell egy vonal alatti állítást, elegendő bebizonyítani, hogy a vonal feletti állítások igazak. Ekkor világosan látható, hogy a felsorolt szabályok elég jól tükrözik a matematikusok által széles körben használt bizonyítási módszereket. • Például a diszjunkció eltávolítása megfelel az esetelemzés módszerének . Ha le kell vezetni

-ből

-t, akkor az esetelemzés a következőképpen történik: ha

igaz, akkor vagy

, vagy

igaz, ezért elegendő két esetet megvizsgálni. Külön-külön le kell vezetni

-ból

-t és

-ből

-t.


Gentzen kalkulusai

• A negáció bevezetése a matematikai gyakorlatban az indirekt bizonyítás , azaz az ellentmondáshoz való visszavezetés módszere . Hogy bebizonyítsuk

-t, elegendő – feltéve, hogy

teljesül – ellentmondáshoz jutni, vagyis egy

-t kiválasztva

-ból levezetni

-t és

-t is. Példa Bizonyítsuk be természetes technikával, hogy

(6.6)

Felvetődhet az a kérdés is, hogy ha egy formulahalmazból a predikátumkalkulusban levezethető egy formula, akkor ezt be tudjuk-e mindig bizonyítani csupán a természetes levezetés technikájával. Tétel Ha

, akkor ez belátható a természetes technikával. Bizonyítás A



Gentzen kalkulusai

. 1. esetén

• vagy alapformula, ekkor

belátható a természetes technikával (ezeket a bizonyításokat az olvasóra bízzuk), így – a bővítés szabálya alapján –

is bizonyítható természetes technikával. • vagy hipotézis, azaz eleme a

formulahalmaznak, akkor a

az azonosság törvénye. 2. Az indukciós feltevésünk szerint legyen igaz az állítás minden


. Ha a

szekvenciát megalapozó levezetésfát • a modus ponens levezetési szabállyal nyertük

és


magasságú levezetésfákból. Az indukciós feltevés miatt ekkor ezek a szekvenciák megalapozhatók természetes technikával. Az implikáció eltávolításának a szabályával pedig a


Gentzen kalkulusai

-t is bizonyítottuk. • az általánosítás szabályával nyertük a

szekvenciát megalapozó

magasságú levezetésfából. Az indukciós feltevés miatt ez a szekvencia megalapozható természetes technikával. Ekkor az univerzális kvantor bevezetésének szabályával a

-t is bizonyítottuk. Ezzel a tételt bebizonyítottuk. Ezzel beláttuk azt is, hogy a természetes levezetés kalkulusa ekvivalens a predikátumkalkulussal, így bebizonyítottuk adekvátságát a klasszikus elsőrendű szemantikával. Tétel [A természetes levezetés helyes és teljes.]

pontosan akkor látható be természetes levezetéssel, ha

. Példa Bizonyítsuk be a természetes levezetés segítségével, hogy a

(6.7)

formula logikai törvény.

2. A szekventkalkulus Definíció Legyenek


Gentzen kalkulusai

elsőrendű formulák. Ekkor a

(6.8)

formulát szekventnek nevezzük. Jelölése

(6.9)

vagy rövidebben

, ahol

az

és

a

formulák multihalmazai. A

szekvent tehát egy speciális alakú formula: implikáció, melyben az implikáció bal oldalán a

formuláinak konjunkciós, a jobb oldalán a

formuláinak diszjunkciós láncformulája áll. Ha a szekventben

üres, az implikáció bal oldalán a

törvényt, ha


Gentzen kalkulusai

üres, az implikáció jobb oldalán a

kielégíthetetlen formulát kell elképzelni. Ha

és

formulák, akkor az

jelölés az

szekventet hivatkozza. Példa Határozzuk meg, hogy az alábbi szekventek mint formulák hogyan adhatók meg: 1. (üres) szekvent a

formulát, azaz logikai ellentmondást ír le. 2. szekvent a

, azaz a

formulát jelöli. 3. Az

szekvent jelentése az

, azaz a

formula.


Gentzen kalkulusai

4. jelentése

. 5. jelentése pedig

. Világos, hogy ha egy

formulát szekventté szeretnénk alakítani, azaz elő akarjuk állítani azt a szekventet, ami épp az

formulát írja le, csak egy

jelet kell elé írni:

. Definíció

,

,

,

,

és

szimbólumok.


Gentzen kalkulusai

• A szekventkalkulus alapsémája:

(6.10)

• A szekventkalkulus levezetési szabályai:

(6.11)

(6.12)

(6.13)

Ha az

és

szimbólumokat egy ítéletlogikai nyelv formuláival, a


Gentzen kalkulusai

és

szimbólumokat pedig formulák multihalmazaival helyettesítjük, az alapsémából alapszekventeket kapunk, a levezetési szabály segítségével pedig egy vagy két (vonal feletti) szekventből levezetünk egy (vonal alatti) harmadikat.

a nyelv változója és

term. Tétel • Minden alapszekvent által leírt formula logikai törvény. • A szekventkalkulus egy levezetési szabályában a vonal alatti alakú szekvent pontosan akkor logikai törvény, ha a vonal feletti szekvent vagy szekventek is logikai törvények. (Tehát a szekventkalkulus levezetési szabályai megfordíthatóak.) A tétel bizonyítása gyakorló feladat. Definíció A szekventkalkulusbeli levezetésfa és a levezetésfa magassága a következő: 1. A kalkulus minden alapszekventje egy (egyetlen szekventből álló) levezetésfa, ez a szekvent lesz a levezetésfa gyökere. A levezetésfa magassága 1. 2. Ha

magasságú olyan levezetésfa, amelynek gyökere a szekventkalkulusbeli levezetési szabályban épp vonal feletti szekvent, akkor a levezetési szabállyal a vonal alatti

szekventet előállítva

(6.14)

is levezetésfa, ahol az

szekvent a kapott levezetésfa gyökere, és a levezetésfa magassága


Gentzen kalkulusai

. 3. Ha

és

rendre

és

magasságú olyan szekventkalkulusbeli levezetésfák, melyek gyökerei valamely levezetési szabályban épp vonal feletti szekventek, akkor előállítva a levezetési szabállyal a vonal alatti

szekventet,

(6.15)

is levezetésfa a kalkulusban, amelyben az

szekvent lesz a levezetésfa gyökere, és a levezetésfa magassága

. 4. Minden levezetésfa az 1–3. szabályok véges sokszori alkalmazásával áll elő. Példa A szekventkalkulusban az alábbi fa 3 magasságú levezetésfa, melynek gyökere a

szekvent:


Gentzen kalkulusai

A szekventek mellett zárójelek között megadtuk azt a levezetési szabályt, melyet alkalmazva a szekvent előállt. Definíció Azt mondjuk, hogy az

szekvent a szekventkalkulusban bizonyítható , ha van olyan szekventkalkulusbeli levezetésfa, melynek

a gyökere. Jelölése:

. Az alábbi tétel bizonyítását az olvasóra bízzzuk. Tétel [A szekventkalkulus helyessége.] Ha az

szekvent bizonyítható a szekventkalkulusban, akkor a

formula logikai törvény. Példa A

szekvent a szekventkalkulusban a következő – 6 magasságú – levezetésfával bizonyítható:


Gentzen kalkulusai

Példa A

(6.16)

szekvent (ahol

) a szekventkalkulusban a következő levezetésfával bizonyítható:

A gyakorlatban a szekventkalkulus levezetési szabályait is ,,alulról felfelé'' szoktuk alkalmazni: amikor bizonyítani szeretnénk egy

szekventet, megpróbáljuk a bizonyító levezetésfát a gyökeréből (

-ből) kiindulva ,,alulról felfelé'' haladva felépíteni. Ehhez keresni kell az épülő levezetésfa minden nem alapszekvent leveléhez olyan levezetési szabályt a kalkulusban, mely segítségével a levél előállhat, és a levezetési szabálynak megfelelő vonal feletti szekvent(ek)et be kell írni a készülő levezetésfába ezen levél szülőjeként (szüleiként). A szekventkalkulus levezetési szabályainak megfordíthatósága miatt lényegtelen, hogy az alkalmazható levezetési szabályok közül melyiket választjuk. 89 Created by XMLmind XSL-FO Converter.

Gentzen kalkulusai

Most foglalkozzunk azzal a kérdéssel, hogy vajon a szekventkalkulus ekvivalens-e a predikátumkalkulussal, azaz igaz-e, hogy egy

szekvent pontosan akkor bizonyítható a szekventkalkulusban, amikor

hipotézismentesen levezethető a predikátumkalkulusban. Ha ugyanis a két kalkulus ekvivalens, akkor a szekventkalkulus teljes kalkulus is. Lemma Ha

a predikátumkalkulus alapformulája, akkor

bizonyítható a szekventkalkulusban. Bizonyítás A bizonyítást konstruktív módon végezzük el, a predikátumkalkulus alapsémáiból előállított formulák esetén rendre megkonstruáljuk a megfelelő szekvent levezetését. • Az 1. sémából előállított alapformula esetén a levezetés

• A 2. sémából előállított alapformula esetén a levezetés:


Gentzen kalkulusai



A többi alapformula esetén a levezetés megadását az olvasóra hagyjuk, a lemmát így bizonyítottnak tekinthetjük. Lemma A predikátumkalkulus levezetési szabályai elérhetők a szekventkalkulusból. Bizonyítás Azaz ha

és

bizonyíthatóak a szekventkalkulusban, akkor

is az, továbbá ha

bizonyítható, akkor

is,


Gentzen kalkulusai

• Az olvasóra bízzuk annak bizonyítását, ha

, akkor

is. Ha

,a

levezetési szabály megfordíthatósága miatt

is. Ekkor alkalmazva a szekventkalkulus vágás szabályát kapjuk, hogy

. • Ha

bizonyítható, így alkalmazva a

szabályt

is bizonyítható. Ezzel az állítást beláttuk. Tétel Ha

hipotézismentesen levezethető a predikátumkalkulusban, akkor

bizonyítható a szekventkalkulusban, azaz ha

, akkor

. Bizonyítás A 92 Created by XMLmind XSL-FO Converter.

Gentzen kalkulusai


. 1. esetén

a predikátumkalkulus alapformulája, ekkor

. 2. Az indukciós feltevésünk szerint legyen igaz az állítás minden


. Ha a

szekvenciát megalapozó levezetésfát • a modus ponens levezetési szabállyal nyertük

és


magasságú levezetésfákból, az indukciós feltevés miatt

és

bizonyíthatók a szekventkalkulusban. De a modus ponens elérhető a szekventkalkulusból. • az általánosítás szabályával nyertük a 93 Created by XMLmind XSL-FO Converter.

Gentzen kalkulusai

szekvenciát megalapozó

magasságú levezetésfából, az indukciós feltevés miatt

bizonyítható. De az általánosítás szabálya elérhető a szekventkalkulusból. Ezzel a tételt bebizonyítottuk.

3. Feladatok 1. Bizonyítsuk be természetes technikával, hogy az alábbi szekvenciák megalapozhatók. • • • • 2. Bizonyítsuk be természetes technikával, hogy az alábbi következményrelációk fennállnak. a. b. c. d. 3. Készítsük el a természetes technika ekvivalenciajelre vonatkozó levezetési szabályait. (

) 4. Készítsük el a szekventkalkulus ekvivalenciajelre vonatkozó levezetési szabályait. 5. Bizonyítsuk be, hogy az alábbi szekventek bizonyíthatók a szekventkalkulusban. Mit bizonyítottunk ezzel a szekvent által meghatározott formulákról? • • •


Gentzen kalkulusai

• • 6. Bizonyítsuk be, hogy

pontosan akkor kielégíthetetlen, ha az

szekvent bizonyítható. 7. Bizonyítsuk be, hogy

pontosan akkor, ha az

(6.17)

szekvent bizonyítható. 8. Bizonyítsuk be a szekventkalkulus segítségével a következményreláció fennállását. a. b. c.


Chapter 7. A rezolúciós kalkulus 1. A Herbrand-univerzum és az elsőrendű klózhalmazok Definíció Legyen

elsőrendű klózhalmaz, továbbá a

-ban szereplő függvényszimbólumok halmaza

, konstansszimbólumok halmaza

.A

klózhalmaz Herbrand-univerzumán az alábbiakban definiált

halmazt értjük: 1. Legyen

2. Legyenek továbbá, ha

rendre

, ahol

. 3. Végül legyen


A rezolúciós kalkulus

Herbrand-bázisa a

-beli termekből épített zárt atomok halmaza. Példa Legyen

. Mivel

-ban nincs konstansszimbólum, ezért legyen

egy tetszőleges szimbólum.

.

-ban függvényszimbólum sincs, ezért

(7.1)

A klózhalmaz Herbrand-bázisa pedig

(7.2)

Példa Legyen

. Ekkor

Table 7.1.

...



.

Herbrand-bázisa

(7.3)

Példa Legyen

. Ekkor

Table 7.2.

Definíció Egy

klózhalmaz

leíró nyelve Herbrand-interpretációinak nevezzük és

-vel jelöljük a nyelv olyan interpretációit, melyek univerzuma éppen

, • minden



konstansszimbólumhoz

a

univerzumelemet (önmagát) rendeli, és • minden

aritású

függvényszimbólumhoz

hozzárendeli azt az

műveletet, amelyikre minden

esetén

(7.4)

Egy

elsőrendű klózhalmaz Herbrand-interpretációi tehát csak a

-ban előforduló predikátumszimbólumok interpretálásában különböznek. Ezért világos, hogy

egy

Herbrand-interpretációját a következő módon is leírhatjuk: legyen



Herbrand-bázisa és legyen

(7.5)

Ekkor a

Herbrand-interpretációt az

literál-halmaz egyértelműen megadja. Példa A

klózhalmaz Herbrand-univerzuma:

(7.6)

Herbrand-bázisa:

(7.7)

Néhány Herbrand-interpretáció:

Table 7.3. = = =

Az alábbi ábrán bejelöltük az

Herbrand-interpretációkat.



Definíció A

klózhalmaz

leíró nyelvének legyen

valamely

univerzum feletti interpretációja. Az

-nek megfelelő Herbrand-interpretáció

-nak egy olyan

Herbrand-interpretációja, amelyre teljesül, hogy van olyan

(7.8)

függvény, hogy a



zárt atom pontosan akkor igaz

-ban, amikor a (,,neki megfelelő'')

atom az

(7.9)

értékelés mellett igaz

-ben . Könnyen belátható, hogy egy elsőrendű klózhalmaz nyelvének tetszőleges interpretációjához van megfelelő Herbrand-interpretáció. Legyen

. Legyen a

a következőképpen definiálva: • ha

, akkor a

-ban szereplő extra konstanshoz

rendeljen tetszőleges

-beli elemet, • minden

(egyúttal



) konstansszimbólum esetén

legyen az

-beli elem, • az

alakú

-beli elemek esetén

legyen a

-beli elem. Példa Legyen

. Legyen

a következő:

, az

interpretációja

, a predikátum- és függvényszimbólumokhoz pedig az alábbi reláció- és művelettáblákkal definiált relációkat és műveleteket rendeli

. 103 Created by XMLmind XSL-FO Converter.


Table 7.4.

Table 7.5.

Table 7.6.

Herbrand-univerzuma:

(7.10)

Herbrand-bázisa:

(7.11)

Ekkor a

megfeleltetés:

(7.12)



Az

-nek megfelelő Herbrand-interpretáció:

(7.13)

Példa Legyen

. Vegyük észre, hogy

leíró nyelve az előző példabeli leíró nyelvtől csak abban különbözik, hogy ebben nincs konstansszimbólum. Interpretáljuk

nyelvét az

interpretációval, ami csak annyiban különbözik

-től, hogy konstansszimbólumot nyilván nem kell interpretálnia. Most a

megfeleltetés során

-hoz bármely univerzumelem hozzárendelhető. Tartsuk meg a többi Herbrand-univerzumbeli elemre az előző példabeli megfeleltetést. • Ha

, akkor az

-nek megfelelő Herbrand-interpretáció a fenti

. • Ha



, az

-nek megfelelő Herbrand-interpretáció

(7.14)

Tétel Ha egy

interpretáció kielégít egy

elsőrendű klózhalmazt, akkor az

-nek megfelelő Herbrand-interpretáció is kielégíti

-t. Bizonyítás A definíció szerint ha

az

-nek megfelelő Herbrand-interpretáció, akkor van olyan

függvény, hogy minden

esetén az

a

-hez ugyanazt az igazságértéket rendeli, mint az



a

atomhoz az

(7.15)

értékelés mellett. Tétel Egy

elsőrendű klózhalmaz akkor és csak akkor kielégíthetetlen, ha

-t nem elégíti ki a Herbrand-univerzuma feletti egyetlen Herbrand-interpretáció sem. Bizonyítás 1. Tegyük fel, hogy

kielégíthetetlen. Ekkor

-t nem elégítheti ki (semmilyen univerzum felett) egyetlen interpretáció sem, így egyetlen Herbrandinterpretáció sem. 2. Tegyük fel, hogy

ugyan kielégíthetetlen az általa meghatározott Herbrand-univerzumon, de

nem kielégíthetetlen, azaz van olyan

univerzum és

interpretáció, amely

-t kielégíti. Legyen



a

-nek megfelelő Herbrand-interpretáció. Az előző tétel miatt

kielégíti

-t, pedig

a Herbrand-univerzum feletti interpretáció. Ellentmondásra jutottunk, tehát ha

kielégíthetetlen a Herbrand-univerzumán, akkor

kielégíthetetlen. Egyik tétel sem áll fenn, ha

nem elsőrendű klózhalmaz. Vagyis, ha

zárt formulák tetszőleges halmaza, akkor általában nem igaz, hogy

kielégíthetetlenségének vizsgálata esetén elég lenne

-át csak a Herbrand-struktúrákkal interpretálni. Példa Legyen

.A

kvantoros formulája nem elsőrendű klóz.

Herbrand-univerzuma:



,

Herbrand-bázisa:

.A

formulahalmazt egyik Herbrand-interpretáció sem elégíti ki. Azonban

kielégíthető, hiszen az az

feletti

interpretáció, melyben

,

és

, kielégíti

-át. Definíció Legyen

egy klóz,

pedig

Herbrand-univerzuma. Legyen a



(7.16)

termhelyettesitésben

. Ez a helyettesítés

egy, a Herbrand-univerzum feletti értékelése. A

formulát a

klóz egy

feletti alappéldányának nevezzük. Példa A

klózhalmaz klózainak Herbrand-univerzum feletti alappéldányai:

(7.17)

Tétel [Herbrand tétele] Egy

elsőrendű klózhalmaz akkor és csak akkor kielégíthetetlen, ha a

klózai Herbrand-univerzum feletti alappéldányainak van véges, itt kielégíthetetlen részhalmaza. Példa 1. Legyen



. Az

elsőrendű klózhalmaz kielégíthetetlen, mert

Herbrand-univerzum feletti alappéldányainak

(7.18)

egy véges kielégíthetetlen részhalmaza. 2. A

kielégíthetetlen, mert

Herbrand-univerzum feletti alappéldányainak

(7.19)

egy véges, kielégíthetetlen részhalmaza. Ezek az alappéldányok az

(7.20)

értékelés mellett álltak elő.

2. Az alaprezolúció Ha Herbrand tételét szeretnénk felhasználni egy klózhalmaz kielégíthetetlenségének vizsgálatára, a klózhalmaz Herbrand-univerzum feletti alappéldányai halmazában kell keresnünk kielégíthetetlen, véges részhalmazt. Egy elsőrendű klóz alappéldányai zárt literálok elemi diszjunkciói, tehát maguk is klózok. Ebben a szakaszban most csak ilyen klózokkal dolgozunk: zárt atomok és negáltjaik elemi diszjunkcióival. Nevezzük őket alapklózoknak . Egy atomot és negáltját komplemens literálpárnak fogjuk nevezni. Definíció Legyen a

és



alapklózokban az egyetlen komplemens literálpár

és

.A

klózt a

klózpár rezolvensének , az

és

literálokat pedig a kirezolvált literáloknak nevezzük. Ha

és

, rezolvensük az üres klóz (

). Példa Vizsgáljunk most meg néhány klózpárt, van-e rezolvensük.

Table 7.7. klózpár

rezolvens

(a) (b)

nincs komplemens literálpár

(c)

nincs komplemens literálpár

(d)

két komplemens literálpár van

(e)

Tétel Legyenek 112 Created by XMLmind XSL-FO Converter.


és

, ahol

és

az egyetlen komplemens literálpár.

. Bizonyítás Ha

és

, akkor nincs a

klózhalmazt kielégítő interpretáció, tehát igaz az állítás. Egyébként a

klózhalmazt kielégítő tetszőleges interpretáció 1. vagy olyan, hogy

igaz benne, de

hamis (

), 2. vagy olyan, hogy

igaz benne, de



hamis (

). Mivel az

interpretáció kielégíti a

klózhalmazt, azaz itt a

és a

klózok igazak, de

hamis, ezért

igaz, tehát igaz

is. Hasonlóképpen láthatjuk be, hogy az

interpretációkban pedig

igaz. Tehát mind

, mind

kielégíti a

klózt. 114 Created by XMLmind XSL-FO Converter.


Definíció Egy

alapklózhalmazból a

klóz rezolúciós levezetése egy olyan véges

klózsorozat, ahol minden

-re 1. vagy

, 2. vagy van olyan

, hogy

a

klózpár rezolvense, és klózsorozat utolsó tagja,

, éppen a

klóz. Példa Próbáljuk meg az üres klózt levezetni a



(7.21)

klózhalmazból. A levezetés bármelyik

-beli klózzal indítható.

Table 7.8. [

] [

] [ 1, 2 rezolvense ]

[

] [ 2, 4 rezolvense ] [ 3, 5 rezolvense ]

[

] [ 6, 7 rezolvense ]

[

]



[ 8, 9 rezolvense ] [ 5, 10 rezolvense ]

Lemma Legyen

tetszőleges alapklózhalmaz és a

klózsorozat rezolúciós levezetés

-ból. Ekkor

minden

-re következménye az

klózhalmaznak, azaz

. Bizonyítás 1. A levezetés első klóza,

, biztosan eleme

-nak, tehát

. 2. Tegyük most fel, hogy minden

-re igazoltuk már, hogy



. 3. Belátjuk, hogy

-re is igaz az állítás. Ha

, akkor

. Ha

valamely

klózok rezolvense, akkor az előző tétel miatt

. Az indukciós feltevés miatt

és

. Ebből

. Tétel [A rezolúciós kalkulus helyessége.] Legyen

tetszőleges alapklózhalmaz. Ha

-ból levezethető az üres klóz, akkor

kielégíthetetlen. Bizonyítás Tegyük fel, hogy van olyan

interpretáció, ami kielégíti 118 Created by XMLmind XSL-FO Converter.


-t. Az előbbi lemma szerint egy

-ból való rezolúciós levezetésbeli bármely

klózra

, tehát

kielégíti a rezolúciós levezetés minden klózát is. De az üres klóz kielégíthetetlen, tehát nem lehet eleme a levezetésnek. Így tehát ha

-ból levezethető az üres klóz, akkor

kielégíthetetlen. Tétel [A rezolúciós kalkulus teljessége.] Ha a

véges alapklózhalmaz kielégíthetetlen, akkor

-ból levezethető az üres klóz.

3. Az elsőrendű rezolúció Példa Legyen két elsőrendű klóz a

(7.22)

és

pontosan egy komplemens literálpárt tartalmaz. Ha a magjaikat az alapklózokhoz hasonlóan rezolválnánk, a



(7.23)

klózhoz jutnánk. Lássuk be, hogy

(7.24)

Ha

kielégíti a

és

klózokat, a

és

formulák

-ben minden értékelés mellett igazak. Tehát ha egy értékelés mellett

-ben

hamis, akkor ott

igaz, és ha

hamis, akkor

igaz. Mivel minden értékelés mellett



igazsága esetén

hamis és fordítva, így minden értékelés mellett vagy a

, vagy az

igaz, és így

. Ha ilyen módon képezve elsőrendű klózok rezolvensét szeretnénk ezt rezolúciós levezetési szabályként alkalmazni, akkor igazolni kell általánosan is a példabeli állítást. Tétel Legyenek most

és

olyan elsőrendű klózok, melyek pontosan egy komplemens literálpárt tartalmaznak, azaz

és

magjai

(7.25)

alakúak, ahol

és

a komplemens literálpár. Legyen a



klóz magja

. Ekkor

. Bizonyítás Tegyük fel, hogy az

interpretáció kielégíti a

elsőrendű klózhalmazt. Kövessük az előző gondolatmenetet. Az

interpretációban tetszőleges értékelés mellett vagy

és

, vagy

és

igaz. Azaz

-ben

igaz. Észrevehetjük, hogy komplemens párt ugyan nem tartalmazó két elsőrendű klóz Herbrand-univerzum feletti alappéldányaiban mégis lehet komplemens pár. Példa

(7.26)



Egyik klózpárban sincs komplemens literálpár. Alaprezolúcióval vizsgáljuk meg, hogy a klózhalmaz kielégíthetetlen-e. A Herbrand-univerzum:

(7.27)

Egy alaprezolúciós levezetés:

Table 7.9. [

] [

,

]

[

,

]

Tegyünk egy új változót a kiválasztott alapklózokban az

helyébe.

Table 7.10. [



] [

]

[

]

Ez a levezetés a

(7.28)

klózhalmazból való egy elsőrendű rezolúciós levezetés. Ezt a klózhalmazt úgy kaptuk az eredetiből, hogy az elsőrendű klózok magjaiban az atomi formulákban a változók helyébe olyan termeket helyettesítettünk, amelyek azonos alapú literálokat eredményeztek. Ezzel a – logikában egyébként nem megengedett – helyettesítéssel (illesztő helyettesítés) • kapott elsőrendű klózhalmaz alappéldányai között az eredeti klózhalmaz egymással komplemens litárokat tartalmazó alappéldányai megjelennek, de ilyen literálokat nem tartalmazó alappéldányok közül sok kiszűrődik, • miközben a klózhalmaz kielégíthetősége megőrződik. Tétel Legyen

a

elsőrendű klóz magja. Tegyük fel, hogy

(7.29)

Legyen



tetszőleges termhelyettesítés

leíró nyelvében, és

(7.30)

Ekkor tetszőleges olyan

Herbrand-interpretációban, amelyben

igaz, a

klóz is igaz. Bizonyítás Tegyük fel, hogy a

Herbrand-interpretációban a

klóz, azaz

igaz. Ekkor

a Herbrand-interpretációbeli minden értékelés mellett igaz, azaz

Herbrand-univerzum feletti alapklózai

-ban igazak. Nyilván

-nak a



feletti alappéldányai mind

feletti alappéldányai is, hisz a

termek jelennek meg az

változók helyett

-ben. Ezek a termek viszont, ha a változóik helyére Herbrand-univerzumbeli elemeket helyettesítünk, szintén Herbrand-univerzumbeli elemek lesznek, és így

alappéldányaiban is előfordulnak. Definíció Legyen

egy

elsőrendű klózban előforduló legalább két azonos alapú egyformán negált literál alapjainak halmaza. Ha

atomjai illeszthetők egymáshoz és

a

legáltalánosabb illesztő helyettesítése, akkor a

magú klózt a

klóz faktorának nevezzük. Ha a faktor egységklóz, akkor

egységfaktorának hívjuk.



Példa Legyen

. A két

-vel kezdődő atom legáltalánosabb illesztő helyettesítése a

(7.31)

Ennek megfelelően a

(7.32)

klóz a

klóz faktora. Definíció Legyenek

és

változóikban tiszta klózok. Legyenek

és

magjai rendre

és

alakúak, ahol

és



ellentétesen negált literálok. Ha az

és az

literálok alapjai illeszthetők egymáshoz, legyen

a legáltalánosabb illesztő helyettesítésük. Ekkor a

és

klózok bináris rezolvense a

magú klóz. Definíció A

és a

klózok elsőrendű rezolvense a következő bináris rezolvensek valamelyike: 1. a

és a

klózok bináris rezolvense, 2. a

klóz és a

klóz egy faktorának a bináris rezolvense,



3. a

klóz egy faktorának és a

klóznak a bináris rezolvense, 4. a

klóz egy faktorának és a

klóz egy faktorának a bináris rezolvense. Példa Legyen

(7.33)

Mivel

mind

-ben, mind

-ben előfordul, a

-ben átnevezzük. Ezután

. A rezolváláshoz válasszuk az

(7.34)

literálokat. Alapjaik legáltalánosabb illesztő helyettesítése:



. Így tehát a

és a

klózok bináris rezolvense

(7.35)

ahol a

és a

literálok szerint rezolváltunk. Példa Legyen

(7.36)

A

faktorának magja

.

faktorának és

-nek bináris rezolvense a

klóz. Ennélfogva a

és a



klózok egyik elsőrendű rezolvense

. Tétel Legyen

a

és

elsőrendű klózok elsőrendű rezolvense. Ekkor

. Bizonyítás

és

változóikban tiszta klózok. Jelöljük

és

elsőrendű rezolvensét – utalva a rezolvensképzés módjára – a következőképpen:

(7.37)

Egy korábban bizonyított tétel miatt, ha az

Herbrand-interpretáció kielégíti

-t, akkor



kielégíti a

klózhalmazt is. Az a két literál, amely szerint rezolváltunk, a

és

klózokban komplemens literálpár, így

(7.38)

Ez viszont azt jelenti, hogy

. Definíció Egy

klózhalmazból való elsőrendű rezolúciós levezetés elsőrendű klózok egy olyan véges

sorozata, ahol minden

-re 1. vagy

, 2. vagy van olyan

, hogy

a



és

klózok elsőrendű rezolvense. Tétel [Elsőrendű rezolúciós kalkulus helyessége.] Ha egy

klózhalmazból van az üres klóznak elsőrendű rezolúciós levezetése, akkor

kielégíthetetlen. Bizonyítás Tegyük fel, hogy van az üres klóznak elsőrendű rezolúciós levezetése

-ból:

. Tegyük fel ugyanakkor, hogy van olyan

interpretáció, mely kielégíti a

klózhalmazt. Ezért ha a rezolúciós levezetésben

,

kielégíti

-t. Ha pedig a rezolúciós levezetésben

a

és

klózok elsőrendű rezolvense 133 Created by XMLmind XSL-FO Converter.


és

kielégíti a

és

klózokat, akkor

kielégíti a

rezolvensüket is. Ezért indukcióval könnyen látható, hogy

-nek ki kellene elégítenie a

klózhalmazt is. De

, az üres klóz pedig kielégíthetetlen, tehát

-nak is kielégíthetetlennek kell lennie. Példa A

(7.39)

klózhalmazból szerkesszünk meg egy elsőrendű rezolúciós levezetést:

Table 7.11.

[



]

[

faktorizáció,

]

A faktorizáció az elsőrendű rezolúciós elv lényeges eleme, alkalmazása nélkül az elsőrendű rezolúciós eljárás nem lenne teljes. Példa Adott a következő formulahalmaz:

(7.40)

A formulák alapján kapott klózhalmaz:

(7.41)

1. A Herbrand-univerzum:

. A Herbrand-bázis:

.A

feletti alapklózhalmaz:

. Alaprezolúciós levezetés:

Table 7.12.



[ 1, 2 rezolvense ]


2. Elsőrendű rezolúciós levezetés

-ból, faktorizáció nélkül:

Table 7.13.

[ 1, 2 rezolvense ]

[ 1, 4 rezolvense ]

A levezetés nem folytatható, mivel nincs olyan klózpár, amely egyetlen komplemens literálpárt tartalmazna. Így az üres klózt nem kapjuk meg. 3. Rezolúciós levezetés

-ból, faktorizációval: a. Alkalmazzuk

klózaira a

legáltalánosabb illesztő helyettesítést.

(7.42)



b. A levezetés

-ból:

Table 7.14.

[ 1, 2 rezolvense ]


Tétel [Elsőrendű rezolúciós kalkulus teljessége.] Ha egy

elsőrendű klózhalmaz kielégíthetetlen, akkor

-ból van az üres klóznak rezolúciós levezetése.

4. Rezolúciós levezetési stratégiák 4.1. 1. A teljes szintek módszere Legyen

tetszőleges klózhalmaz. A teljes szintek módszere a következőképpen állítja elő a levezetéshez a rezolvenseket:

1. ,

. 2. Ha

, sikeresen vége. Egyébként



és folytassuk a 2. lépéssel. Ezzel a módszerrel sok egyforma klóz jelenik meg a rezolvensek között, sőt olyan rezolvens klózok is a klózhalmazba kerülhetnek, amelyekre a továbblépésben biztosan nincs szükség. E problémák megoldására született meg a törlési stratégia.

4.2. 2. A törlési stratégia Minden

esetén az

klózhalmazból el kell hagyni a fölösleges klózokat: a tautológiákat és azokat, amelyeket más klózok ,,tartalmaznak''. Definíció Jelölje

és

rendre a

és a

klózok literáljainak halmazát. Egy

klóz befoglalja a

klózt, ha van olyan

termhelyettesítés, hogy

.



a befoglalt klóz. Példa Legyen

és

. Ekkor

és

. Ha

, akkor

.

, tehát

befoglalja

-t. A tautológiákat és a befoglalt klózokat meg kell találni. A tautológiákat a faktorizáció segítségével fedhetjük fel. A befoglalási teszt azonban nem olyan egyszerű.

4.2.1. Befoglalási algoritmus Legyenek

és

klózok. Legyen

, ahol



a

-ben előforduló változók és

sem

-ben, sem

-ben elő nem forduló különböző konstansszimbólumok. Tegyük fel, hogy

. 1.

,

,

, 2. Ha

, akkor vége:

befoglalja

-t. Egyébként

(7.43)



3. Ha

üres, akkor vége:

nem foglalja be

-t. Egyébként

, és folytatás a 2. lépéssel. Példa Befoglalja-e

a

-t?

(7.44)

változói az

és a

. Legyen

. Ekkor

(7.45)

1. ,



. 2. Mivel

, azt kapjuk, hogy

(7.46)

3. Mivel

és az

, az eljárást folytatva kapjuk, hogy

. 4. Mivel

, az eljárásnak vége:

befoglalja

-t.

5. Feladatok 1. Határozzuk meg az alábbi klózhalmazok valamely rezolúciós cáfolatát. • •

2. Igazoljuk, hogy a



(7.47)

formulahalmaz nem elégíthető ki. 3. Elsőrendű rezolúciós kalkulussal igazoljuk, hogy az alábbi formulák logikai törvények. • • • • •


Hivatkozások Symbolic Logic and Mechanical Theorem Proving. Chang Chin-Liang and Lee Richard Char-Tung. Academic Press. NewYork and London. 1973. Bevezetés a matematikai logikába. Albert Dragálin and Szvetlána Búzási. 1986. Matematikai logika. Miklós Ferenczi. Műszaki Könyvkiadó. Budapest. 2002. First-Order Logic and Automated Theorem Proving. Melvin Fitting. Springer-Verlag. 1990. Logic for Computer Science: Foundations of Automatic Theorem Proving. Jean Gallier. Wiley. 1986. Matematikai logika példatár. Tamás Kádek, Judit Robu, and Magda Várterész. Kolozsvári Egyetemi Kiadó. Kolozsvár. 2010. A matematikai logika alkalmazásszemléleltű tárgyalása. Katalin Pásztorné Varga and Magda Várterész. Panem. Budapest. 2003. Bevezetés a modern logikába. Imre Ruzsa and András Máté. Osiris Kiadó. Budapest. 1997. First Order Logic. Raymond Smullyan. Springer-Verlag. 1968.


Colophon A tananyag a TÁMOP-4.1.2.A/1-11/1-2011-0103 számú Gyires Béla Informatika Tananyag Tárház projekt keretében készült. A tananyagfejlesztés az Európai Unió támogatásával valósult meg.


Automatikus tételbizonyítás

Recommend Documents