Programozás | Prolog » Prolog, avagy a logikai programozás

PROLOG, avagy a logikai programozás Bevezetés : Eddig imperatív nyelvekkel dolgoztunk (Pascal, C), most a deklaratív nyelvek közül a Prologot ismerjük meg. A cél nem csak egy újabb nyelv megtanulása, hanem látókörünk kiszélesítése, hogy ha egy adott problématípussal (problémaosztállyal) kerülünk szembe tudhassuk, milyen eszközök állnak rendelkezésre a feladat (probléma) megoldásakor. Például : adatbázis kezelésre Clipper, dBase az alkalmas, ugyanakkor egy szakértői rendszer megvalósításához, tudásbázisok kezelésére egy logikai programozási nyelv (pl.: PROLOG) a legmegfelelőbb (Egyéb alkalmazási területei : képkiértékelés, orvostudomány . (ahol MI fordul elő)) Az imperatív nyelvekben a probléma megoldása mindig valamilyen időbeli egymásutániságot, szekvenciát követ, ezzel szemben a logikai programozási nyelveknél a feladatot leíró tények és szabályok sorrendje nem fontos (elvben; a végeredmény meghatározása persze

itt is szekvenciálisan történik, hiszen egy számítógépen oldjuk meg a feladatot). A logikai nyelvben először megadjuk a feladatot leíró tényeket és szabályokat, majd kérdéseket teszünk fel, amelyekre a tudásbázis a fellelhető információk alapján vmilyen deduktív láncot alkotva kikövetkezteti a választ. Ez a válasz általában egy YES vagy NO, de ha "elég trükkösen" fogalmazzuk meg a kérdést ennél bővebb is lehet. A logikai programmal tehát egy Kérdés-Felelet kapcsolatot építünk fel, s megfelelően megépített rendszerben az így feltett kérdésekre kapott válaszokkal is bővíthetjük a kiinduló tudásbázist ("MI"). A logikai programnyelvekben a tényleges következtetéseket egy a fordítóprogramba épített következtetőgép végzi el, melyhez a programozó nem férhet hozzá, de erre nincs is szükség. Logikákról általában : Az embernek szüksége van az őt körülvevő világot leíró absztrakt modellek

megalkotására, melyek által az eddig megszerzett tudását összefoglalhatja/összegezheti. Ezekre azért van szükség, hogy a tapasztalatok alapján bizonyos dolgokat már kikövetkeztethessünk (diagnózisokat, prognózisokat készíthessünk), ne kelljen mindent a gyakorlatban is kipróbálni (sok idő, erőforrás, pénz megspórolható ezzel). Az ilyen modelleket nevezzük logikának, feladatuk a környező világ egy részének bizonyos aspektusból történő modellezése. Az ilyen modellalkotásra képes rendszereket formális logikai rendszernek nevezzük. Ezen rendszerek egy fajtája (része?) az axiomatikus formális rendszerek, amelyekben egy kiinduló axióma halmaz (axióma - meg nem kérdőjelezett, mindig igaznak elfogadott kijelentés/alapállítás) és a levezetési szabályok halmazát felhasználva a megfogalmazott célállításról eldönthetjük, hogy igaz-e vagy sem. A század elején azt hitték, hogy minden ilyen axiomatikus formális rendszerre igaz az

alábbi két állítás 1. helyesség : Egy axiomatikus formális rendszerben az axiómákból kiindulva a levezetési szabályokat alkalmazva (a rendszer szempontjából) " esetben érvényes (igaz) állításokat (formulákat) kapunk. Ez egy minimális kritérium a rendszerre. 2. teljesség : " a rendszer szempontjából érvényes állítás (formula) levezethető az axiómákból a szabályok segítségével Ez egy maximális kritérium a rendszerre. (ez az 1 állítás fordítottja) Ha egy adott rendszerre a 2. állítás igaz Ţ az 1 is igaz lesz, fordítva azonban koránt sincs így Azonban a 20-as 30-as években Kurt Gödel német matematikus bebizonyította, hogy a 2. állítás nem minden ilyen rendszerre igaz (ő a számelméletre bizonyította be). (Ha az 1 állítás sem lenne igaz az adott rendszerre, az azt jelentené, hogy igaz állításokból (az axiómákból) kiindulva a szabályok felhasználásával (a rendszer szempontjából) hamis állításokat is le

tudnánk vezetni Ţ a rendszer már nem lenne logika). Kiderült, hogy az olyan axiomatikus rendszerek, amelyek az elemi aritmetika (szorzás, összeadás, zárójelezés) tulajdonságait magukba foglalják már nem teljesek (nem igaz rájuk a 2. állítás) Gödel nem teljesség tétele : az elég bonyolult (a világot elég jól modellező/leíró) axiomatikus rendszerek nem teljesek (az 1. állítás igaz rájuk, a 2 már nem) elég bonyolult rendszerek : az elemi aritmetikánál bonyolultabbak. Az általunk tárgyalt logikák helyesek és teljesek is (igaz mindkét állítás Ţ elég gyenge formális rendszerek, de nem annyira, hogy ne lehetne őket használni). Logikák jellemzői általában : szintaxis : a rendszer szempontjából elfogadott/megengedett kifejezések megadásával foglalkozik hogyan írhatunk le a rendszer szempontjából jól formáltnak mondott formulákat (nem jól formált formula - a rendszer nem tud mit kezdeni vele) szemantika : a szintaktikailag

helyes formulákat miként kell értelmezni, a jelentéssel foglalkozik, és az alábbi két részből áll • interpretáció : a formula egyes elemi kijelentései mit jelentenek • kiértékelés : az elemi formulák jelentését ismerve az azokból bizonyos műveleti jelekkel felhasználásával alkotott (összekapcsolt) komplexebb formula egész milyen jelentéssel bír (ennek meghatározása a feladata) logikai ekvivalencia : ha két formuláról elmondhatjuk, hogy jelentésük/értelmük " esetben ua. logikai következmény : mikor mondhatjuk egy formuláról, hogy következménye ennek a formula halmaznak adott tényhalmazon, adott szabályokat felhasználva következik-e a megfogalmazott tétel : célállítás. Ezt bizonyítani kell rezolúció : olyan algoritmus, amely egy adott logikában automatikusan tud tételeket bizonyítani A logikai programoknál lényegében egy ilyen automatikus tételbizonyító eljárás zajlik le. A 0-adrendű predikátum kalkulus

(ítélet-, kijelentés kalkulus, propozicionális logika) Erre épül a PROLOG rendszer is. Ezen logika segítségével egyszerű logikai kijelentések (hétköznapi állítások, kötőszavakkal összekapcsolt kijelentő mondatok) között fennálló rendszert tudjuk kezelni (modellezni). A fentebb általánosan megfogalmazott kifejezések (szintaxis, szemantika, logikai ekvivalencia .) PROLOG-beli konkrét jelenései : szintaxis : • elválasztójelek : ( , ) , , - szimbólumkészlet : • logikai műveleti jelek : ¬ , Ů , Ú , ® , « (negálás, konjunkció, diszjunkció, kondicionálás, bikondicionálás) kondicionálás - ha vmi . akkor , if then, feltétel bikondicionálás - kettős kondicionálás, kondicionálás mindkét irányba • ítéletkonstansok : T , F • ítéletváltozók : p, q, r, s,. ; de ezek lehetnének szavak is v bármi más - konstrukciós szabályok : atomi formulák • " ítéletkonstans atomi formula • " ítéletváltozó atomi

formula • csak ezek (fenti kettő), semmi más (Well-Formed Formula, WFF) jól formált formulák • " atomi formula WFF • ha A és B már WFF, akkor (¬A) , (AŮB) , (AÚB) , (A®B) , (A«B) is WFF-ek • és csak ezek WFF-ek A szimbólumkészlet a logika nyelve, a jól formált formulák a nyelvtana. szemantika : - interpretáció : hogyan kell egy WFF-et értelmezni • " a formulában lévő ítéletkonstanshoz rendeljük hozzá a megfelelő logikai értéket így : T ¬ igaz, F ¬ hamis • " ítéletváltozóhoz rendeljünk hozzá szisztematikusan (" előfordulási helyén ugyanazt) egy tetszőleges logikai értéket - kiértékelés : Az ítéletváltozók és konstansok (részformulák) interpretációja után a köztük lévő logikai műveletek igazságtábláit figyelembe véve a komplex formula logikai értékének meghatározása (kiszámítása). A formulák jelentése a logikai érték, igazság érték (Igaz/Hamis) Példa : egy G := ( p Ů q

) ® ( r « (¬s) ) formula logikai értéke = ? I1 ( p, q, r, s ) = ( T, T, F, F ) implementáció esetén G ( I1 ) = F I2 ( p, q, r, s ) = ( F, T, T, F ) implementáció esetén G ( I2 ) = T Def.: Def.: Def.: Def.: egy formula kielégíthető, ha létezik olyan interpretáció, amelyben logikai értéke igaz azt az interpretációt, amelyben az adott formula igaz, a formula modelljének nevezzük egy formula érvényes, ha minden interpretációjában igaz; ez a tautológia egy formula kielégíthetetlen, ha nem létezik olyan interpretációja, amelyben igaz lenne ez a logikailag hamis állítás vagy az ellentmondás Megjegyzés : • minden érvényes formula kielégíthető • a kielégíthető formula azonban nem feltétlen érvényes is • ha egy formula érvényes, negáltja biztos kielégíthetetlen logikai ekvivalencia Def.: Az A és B formulák acsa ekvivalensek, ha logikai értékük " interpretációban egyidejűleg megegyezik (ugyanaz). Jelölése : ( A Ű

B ) Tétel: Ha A és B formulák és A ekvivalens B-vel ( A Ű B ) acsa igaz, ha (A«B) formula igaz. Biz.: (Ţ) tfh. A Ű B, azaz A és B értéke " interpretációban egyidejűleg megegyezik, de a « művelete az azonos értékekhez rendel igaz értéket. Ezekben az interpretációkban A«B formula " igaz, azaz érvényes. (Ü) tfh. A«B érvényes, azaz " interpretációban igaz, de a « igazságtábla alapján ezek pontosan azon interpretációk, ahol A és B értéke egyidejűleg megegyeznek, azaz logikailag ekvivalensek. logikai következmény Def.: is igaz. Tétel: Azt mondjuk, hogy B formula logikai következménye A-nak ( A Ţ B ), ha " interpretá- cióban ahol A igaz B Ha A és B formulák és a B logikailag következik A-ból ( A Ţ B ) acsa igaz, ha (A®B) formula érvényes (igaz). Def.: A W formula logikai következménye az A1 ,,An formulahalmaznak, ha " olyan interpre- tációban ahol A1 ,.,An igaz ott W is igaz (különben W értéke

bármi lehet) (A1 Ů . Ů An) Ţ W Megj.: Az A1 ,,An formulahalmaz elemei acsa igazak egyidejűleg, ha az (A1 Ů Ů An) formula igaz. (A szintaktika szerint csak a ( ( ( (A1 Ů A2 ) Ů A3 ) Ů ) Ů An ) alak lenne megengedett, de az Ů művelet asszociatív tulajdonsága miatt így is írhatjuk) kitérő: - a formulák az Ů művelettel kommutatív csoportot alkotnak - ugyanez igaz a Ú műveletre is - érvényes mindkét disztributív tulajdonság (?) Ţ a formulák a 0. rendű predikátumkalkulusban a Ů és Ú műveletekkel algebrai testet alkotnak (Boole test) Tétel: Ha W formula acsa logikai következménye A1 ,.,An formulahalmaznak, ha az (A1 Ů . Ů An) ® W formula érvényes (igaz) Biz.: tfh. (A1 Ů Ů An) Ţ W azaz " interpretációban ahol A1 ,,An egyidejűleg igaz ott W is igaz, de az előző megjegyzés és a definíció miatt (a definíció nem szól az A hamis esetről, csak egyetlen állapotot definiál az igazságtáblából) azt az esetet zárjuk ki,

amikor az előtag igaz és az utótag hamis az (A1 Ů . Ů An) Ţ W esetben, tehát az (A1 Ů Ů An ) ® W formula " (megengedett) interpretációban igaz (érvényes). Tétel: Biz.: tfh. (A1 Ů Ů An) ® W formula érvényes, azaz " interpretációban igaz Mivel a kondicionálás igazságtáblája szerint ezekben az interpretációkban mindenhol, ahol az előtag igaz ott az utótag is igaz, azaz a W logikai következménye a definíció alapján az (A1 Ů . Ů An) formulának, tehát a megjegyzés szerint az A1 ,,An formulahalmaznak is (hasonló) A W formula acsa logikai következménye az A1 ,.,An formulahalmaznak, ha az (A1 Ů . Ů An Ů ŘW) formula kielégíthetetlen felhasználva az előző megjegyzést (A1 Ů . Ů An) írható ( ( (A1 Ů A2) Ů ) Ů An) helyett - az előző tétel szerint (A1 Ů . Ů An) ® W - valamint " érvényes formula negáltja kielégíthetetlen és fordítva (oda-vissza igaz) Ř(A1 Ů . Ů An Ů ŘW) Ű (A1 Ů Ů An) ® W

kiinduló ekvivalencia az átzárójelezést az asszociativitás miatt tehettük meg, már csak az Ű-t kell bizonyítani "Ř(A Ů ŘW)" = "®" az igazságtábla alapján Ř(A Ů ŘW) Ű A ® W ŘA Ú Ř(ŘW) Ű ŘA Ú W az ekvivalencia baloldala a de Morgan szabály miatt igaz Ř(A1 Ů . Ů An) Ú Ř(ŘW) = Ř(A1 Ů Ů An) Ú W ami viszont ekvivalens a kiinduló ekvivalencia jobb oldalával, tehát a tételt bebizonyítottuk (azért volt elég egy irányba bizonyítani most, mert csak ekvivalens lépéseket tettünk) A tétel fogalma Def.: Az (A1 Ů . Ů An) ® W formula tétel, ahol az (A1 Ů Ů An) az előfeltétel (premisszák), és a W a következmény (konklúzió). A tétel bizonyítása annak belátása, hogy az (A1 Ů . Ů An) ® W formula érvényes Egy tétel érvényességének bizonyításához elég a tétel negáltjának kielégíthetetlenségét bizonyítani (indirekt bizonyítás). Ilyen módszerrel dolgozik a bizonyítási algoritmus is

Rezolúció Egy automatikus tételbizonyítási algoritmus, aminek inputja egy konjunktív normál formára (CNF) hozott formula. Def.: egy formula CNF-ben van, ha felírható - klózok konjunkciójaként pl. ( ) Ů ( p Ú Řq ) Ů ( ) pl. ( p Ú Řq ) - a klózok literálok diszjunkciói pl. p, q, Řp, Řq - literál = egy ítéletváltozó vagy annak negáltja Tétel: a 0-ad rendű predikátum kalkulusban minden (jól formált) formula CNF-re hozható a következő transzformációs lépéseket (ilyen sorrendben) alkalmazva. 1) (A«B) Ű (A®B) Ů (B®A) a bikondicionálás kiküszöbölése 2) (A®B) Ű ŘA Ú B a kondicionálás kiküszöbölése 3) Ř(A Ů B) Ű ŘA Ú ŘB a de Morgan szabályok alkalmazása a negáció hatáskörének Ř(A Ú B) Ű ŘA Ů ŘB leszűkítésére 4) A Ú (B Ů C) Ű (A Ú B) Ů (A Ú C) a klózok kialakítása Feladat: A1 := "Ha süt a nap, akkor Péter strandra megy." A2 := "Ha Péter strandra megy, akkor úszik."

premissza Ż A3 := "Péternek nincs lehetősége otthon úszni." A4 := "Ha süt a nap, akkor Péter nem marad otthon." konklúzió A4 logikai következménye-e az (A1 , A2 , A3) formulahalmaznak ? p := "süt a nap", q := "Péter strandra megy", r := "Péter úszik", s := "Péter otthon marad" A1 |> F1 = p®q , A2 |> F2 = q®r , A3 |> F3 = Ř(r Ů s) , A4 |> F4 = p®Řs Tehát a [( p®q ) Ů ( q®r ) Ů ( Ř(r Ů s) )] ® ( p®Řs ) formula érvényességét kell bizonyítani. (A bizonyító eljárás inputja a klózok halmaza, amit a klózok közüli Ů jel elhagyásával kapunk.) A bizonyító eljárás lépései 1. a klózhalmazból válasszunk ki két rezolválható klózt Ci = ( p Ú A ) , Cj = ( Řp Ú B ) ( két klóz rezolválható, ha tartalmaznak egy komplemens literál párt : p, Řp ) 2. a rezolúciós lépés Cij = R (Ci , Cj ) = R ( ( p Ú A ) , ( Řp Ú B ) ) = ( A Ú B ) ( ahol Cij = ( A Ú B )a

rezolvens klóz, R a rezolúciós operátor ) 3. a rezolvenssel bővítsük a kiinduló klózhalmazt, majd lépjünk vissza az 1 lépéshez Szabályok - ha A vagy B részklóz üresek (nincsenek ott) akkor a keletkező rezolvensek rendre B, A - ha A és B részklóz is üres, akkor a rezolvens egy üres klóz lesz NIL, amely a definíció szerint kielégíthetetlen, nincs modellje (a NIL egy minden interpretációban hamis konstans) Megjegyzés Ha ( A Ţ NIL ) Ű ( A ® NIL ) az Ű és a ® definíciói alapján Az ( A ® NIL ) előtagja (feltételesen) igaz (a bikondicionálás igazságtáblája alapján), és az utótagja hamis, de így az egész hamis. Ekkor az ezzel ekvivalens ( A Ţ NIL ) is hamis, tehát ez a tétel nem tétel. (Ez az indirekt bizonyítás analógiája) Tehát az eredeti formulahalmaz kielégíthetetlen, de mivel ez a kiindulónak épp a negációja, az következik, hogy az eredeti tételünk mégis igaz (bebizonyítottuk). A bizonyítási ciklus kilépési

feltétele A kiszállási feltétel a NIL klóz levezetése, mert a NIL eredetileg Ď a klózhalmaznak. Akkor vezettük le a tételt, ha felbukkan a NIL klóz. procedure rezolúció (a konjunktív normál formára hozás után) klózok := s s klóz set (klóztípus) WHILE NIL Ď klózok DO select (klózok , Ci , Cj) úgy, hogy Ci , Cj rezolválhatók legyenek Cij = R (Ci , Cj ) a rezolúciós lépés klózok := klózok Č Cij end DO end rezolúció Tétel: A rezolúció teljességének tétele. Egy kielégíthetetlen klózhalmazból kiindulva az összes lehetséges rezolvenst képezve a rezolúció algoritmusa véges sok lépésen belül levezeti a NIL klózt. - ha több klóz is van, melyiket válasszam - van-e rezolválható klózpár - az eljárás nem elég determinisztikus, ezért adminisztrálni kell melyik klózpár volt rezolválva, mely literálok szerint, így biztos le fog állni (plusz még a lenti feltétel) - ha már nincs a select-re rezolvens klózpár és még

nincs megállás, azaz nincs levezetve a NIL klóz, akkor le kell állni, az alaphalmaz nem kielégíthetetlen, a tétel nem vezethető le. (De maximum így is csak 2n interpretáció lehet, ahol n a különböző literálok száma). - az eljárásbeli klózok := klózok Č Cij lépés csak akkor jogos, ha a két halmaz ekvivalens (minden iteráció során). Bizonyítandó : tényleg ekvivalensek - a rezolúció a tétel negáltjáról bizonyítja, hogy kielégíthetetlen Az 5. oldal alján kezdett feladat rezolúciója Ř( [( p®q ) Ů ( q®r ) Ů ( Ř(r Ů s) )] ® (p®Řs) ) , a kiindulás a bizonyítandó tétel negáltja 1. 1.a 2. 2.a 3. Ř( Ř[( p®q ) Ů ( q®r ) Ů ( Ř(r Ů s) )] Ú (ŘpÚŘs) ) a jobboldali két kondicionálás kiküsz. a baloldali két kondicionálás kiküsz. Ř( Ř[( ŘpÚq ) Ů ( ŘqÚr ) Ů ( Ř(r Ů s) )] Ú (ŘpÚŘs) ) a negáció hatáskörének leszűkítése [( Řp Ú q ) Ů ( Řq Ú r ) Ů ( Ř(r Ů s) )] Ů Ř(Řp Ú Řs) . [( Řp Ú q ) Ů (

Řq Ú r ) Ů ( Řr Ú Řs )] Ů p Ů s- // ( Řp Ú q ) Ů ( Řq Ú r ) Ů ( Řr Ú Řs ) Ů p Ů saz eredmény konjunktív normál formában megj.: az egyetlen literált tartalmazó klózok az ún egységklózok (p, s) A rezolúció kiinduló klózhalmaza tehát : ( Řp Ú q ) , ( Řq Ú r ) , ( Řr Ú Řs ) , p , s rezolúciós lépések 1. ( Řp Ú q ) , ( Řq Ú r ) = ( Řp Ú r ) 2. ( Řq Ú r ) , ( Řr Ú Řs ) = ( Řq Ú Řs ) 3. ( Řr Ú Řs ) , ( Řp Ú r ) = ( Řs Ú Řp ) 4. ( Řs Ú Řp ) , p = Řs 5. Řs , s = NIL tehát, mivel levezettünk egy minden interpretációban hamis klózt, a kiinduló formula hamis, a negáltja viszont igaz. A tételt bebizonyítottuk A bizonyítási algoritmus javítható oly módon, hogy a felesleges adminisztráció nélkül (a már vmilyen literál szerint rezolvált klózpárok feljegyzése) fejeződhessen be. Ehhez azonban a kiinduló klózhalmazt speciálissá kell tenni (Horn klózok alkossák). Def.: A legfeljebb egy pozitív

literált (pl.: p,q) tartalmazó klózokat Horn klózoknak nevezzük ( Řp Ú Řq Ú Řr Ú . Ú Řs Ú t ) ez egy Horn klóz, az egyetlen pozitív literál a t ( ( Řp Ú Řq Ú Řr Ú . Ú Řs ) Ú t ) átzárójelezhető ( Ř( p Ů q Ů r Ů . Ů s ) Ú t ) a de Morgan azonosság szerint ( p Ů q Ů r Ů . Ů s ) ® t a tételre hasonlít, de itt csak pozitív literálok szerepelhetnek előfeltétel/premissza következmény/konklúzió Ez a szabály modellje : ha az előfeltételek teljesülnek, akkor a t következmény is teljesül. Def.: A pozitív literált tartalmazó Horn klózt definitnek nevezzük, az azt nem tartalmazót (csak negatív literálból állót) negatív Horn klóznak nevezzük. Az egyetlen pozitív literálból álló Horn klózt pozitív egységklóznak nevezzük, ami modellje a ténynek. (A tény csak egyetlen literált tartalmaz, és az pozitív) A PROLOG Horn klóz logikát használ, mást nem is lehet megadni, csak szabályt ill. tényt Gyakorlatilag

az ilyen csak Horn klózokat alkalmazó következtetési algoritmus is alkalmazható minden problémára. A Horn klózok rezolúciós algoritmusa procedure HK rezolúció (a konjunktív normál formára hozás után) klózok := s s klóz set (klóztípus) WHILE NIL Ď klózok DO select (klózok , p , C) ahol p egy ítéletváltozó (pozitív literál), azaz pozitív egységklóz, és C egy Řp-t tartalmazó tetszőleges Horn klóz C = R ( p , C ) a rezolúciós lépés klózok := ( klózok { C } ) Č { C } end DO end HK rezolúció Miért jobb ez mint az eredeti rezolúció ? Az éppen vizsgált C klózból minden iteráció során törlök egy literált, tehát a C klóz mindig kisebb lesz, mint az eredeti, amit ki is veszek az iteráció során az eredeti klózhalmazból (csak a rövidebb marad benn). Azaz a klózok halmaza nem bővül, de az is garantálva van, hogy az algoritmus nem választhatja ki ugyanazt a klózpárt kétszer (ua. literál szerint) Miért terminál véges

lépés múlva ? - a klózok halmaza az iterációk során nem bővül - kétszer ugyanaz a klózpár nem kerül kiválasztásra, mert hosszuk a rezolúciós lépés során mindig csökken egy literállal és az eredeti klóz kikerül a klózhalmazból - továbbá a klózok száma, valamint a klózok hossza véges (előbb-utóbb biztos elfogynak) A kilépési feltétel - elfogynak a rezolválható klózok (a tételt nem tudtuk bebizonyítani) - az algoritmus levezeti a NIL klózt (a tételt bebizonyítottuk) n Az iterációk számának felső becslése : i=1 tartalmazó klózok hosszait összegzem. S klózhosszi , ahol csak az 1 literálnál többet Jogos-e a klózok := ( klózok { C } ) Č { C } lépés ? Megmarad-e a két halmaz ekvivalenciája ? klózok Ű ( klózok { C } ) Č { C } ekvivalenciát kell bizonyítanunk Biz.: Mivel C logikai következménye C-nek (mert C-t úgy kapom, hogy C-ből elhagyok egy literált, ami diszjunkcióval kapcsolódott a többihez. C = Řp Ú C

minden interpretációban, ahol C igaz ott C is igaz) , ezért a ( klózok { C } ) Č { C } és a klózok Č { C } klózhalmazok ekvivalensek. Így a tranzitivitás miatt az általános rezolúciós algoritmusra vezettük vissza. A PROLOG-ban nem csak 0-ad rendű formulák kezelhetők, 1. rendű logikai következtetési rendszer Az 1. rendű predikátum kalkulus A1 := "Van olyan páciens, aki minden doktorban megbízik." A2 := "A kuruzslókban egyetlen páciens sem bízik meg." A3 := "Egyetlen doktor sem kuruzsló." A finomságokat a minden " és a létezik $ univerzális és egzisztenciális kvantifikációk jelentik. szintaxis : • elválasztójelek : ( , ) , , - szimbólumkészlet : • logikai műveleti jelek : ¬ , Ů , Ú , ® , « • ítéletkonstansok : T , F • ítéletváltozók : p, q, r, s . • individuum konstansok (egyének) : a, b, c . • individuum változók : x, y, z . • függvény szimbólumok : f, g, h . •

predikátum szimbólumok : P, Q, R . • kvantorok : " ,$ - term : • minden individuum konstans term • minden individuum változó term • ha t1 . tn termek és f függvény egy n argumentumú függvény szimbólum, akkor az f ( t1 , . , tn ) is term • és csak ezek termek - atomi formulák : • minden ítéletkonstans atomi formula • minden ítéletváltozó atomi formula • ha a P egy m argumentumú predikátum szimbólum és t1 . tn termek, akkor a P ( t1 , . , tn ) is term • és csak ezek atomi formulák - WFF : szemantika : - interpretáció : - kiértékelés : • minden atomi formula WFF • ha A és B WFF, akkor ¬A, ¬B, (AŮB), (AÚB), (A®B), (A«B) is WFF • ha A WFF és az x egy individuum változó akkor " x A, $ x A is WFF • és csak ezek WFF-ek • rendeljük a formula minden T-jéhez és F-jéhez rendre logikai igaz és hamis értékeket • az ítéletváltozókhoz tetszőlegesen, de szisztematikusan rendeljünk hozzá egy-egy logikai

értéket • definiáljunk egy U alaphalmazt, amit tárgyalási univerzumnak (individuum tartománynak) nevezünk • a formulákban szereplő összes individuum konstanshoz rendeljünk hozzá az U halmaz egy-egy elemét • ha van egy n argumentumú függvény szimbólum a formulában, akkor rendeljünk hozzá egy f : Un |> U típusú leképezéseket (Un = U n-edrendű direkt szorzata) • a formulában lévő m argumentumú P predikátum szimbólumhoz rendeljünk P : Un |> { T, F } típusú leképezéseket (az igazság függvény lényegében a predikátum!) • ha az A és B részformulák a formulában, akkor az őket összekötő logikai műveleti jelek igazságtáblái alapján ¬A, (AŮB), (AÚB), (A®B), (A«B) kiértékelhetők • ha A részformula és x individuum változó " x A igaz, ha U miden x elemére az A formula igaz. $ x A igaz, ha létezik U-ban (legalább egy) olyan x elem, melyre az A formula igaz. logikai ekvivalencia és következmény A

kielégíthetőségről, kielégíthetetlenségről, érvényességről, logikai ekvivalenciáról, logikai következményről szóló definíciók, tételek és bizonyítások teljes mértékben megegyeznek a 0-ad rendű predikátum kalkulusnál leírtakkal. Bővebben lásd ott A definíciókban előforduló minden interpretációban kitétel problémát okoz, mert az 1. rendű predikátumoknak végtelen sok interpretációja lehetséges, hiszen amikor az U halmazt vesszük annak bármely eleme lehet (a 0-ad rendű predikátumoknál nem jelentett problémát, mert csak véges számú interpretáció volt lehetséges) Ţ nehezen lehet így a tételeket bizonyítani. A rezolúciót azonban ebben az esetben is lehet alkalmazni ! (Robinson 50-es évek USA) A formulákat itt is klózformára kell hozni (itt Skolem standard forma). Kikötés : - a formulákban nincs szabad változó (minden változó kötött) - nincsenek redundáns kvantorok Klóz formára hozás lépései 1. A

bikondicionálások («) és kondicionálások (®) kiküszöbölése 2. A negáció hatáskörének redukálása - ¬ ( ¬A ) Ű A - ¬ ( A Ů B ) Ű ¬A Ú ¬Bde Morgan szabály - ¬ ( A Ú B ) Ű ¬A Ů ¬B // . - ¬ ( " x A ) Ű $ x ( ¬A ) - ¬ ( $ x A ) Ű " x ( ¬A ) 3. A változók standardizálása, ha különböző kvantorok által kötött különböző részformulákban lévő változókat nevezzük át. Pl : " x A ( x ) Ů $ x B ( x ) -ből " x A ( x ) Ů $ y B ( y ) 4. Az egzisztenciális kvantorok ( $ ) kiküszöbölése - $ x A ( x ) Ű A ( a ) , a változó helyett egy konstans. Ahol a az U halmaz azon eleme, amelyre A igaz.Ez az a az ún Skolem konstans - " x $ y A ( x, y ) Ű " x A ( x, f (x) ) (minden x-hez létezik min. egy olyan x-től függő y, amire A igaz)Ez az f (x) az ún. Skolem függvény Az egzisztenciális kvantorokat ( $ ) balról jobbra küszöböljük ki sorban úgy, hogy azonosítunk minden lépésben egy $ y A ( y )

alakú részformulát, és azon változókat, amelyeket egzisztenciális kvantor ( $ ) köt, és a " kvantor hatáskörébe tartoznak rendre helyettesítjük a Skolem függvényükkel így : " x1 . " xn ( $ y A ( y , x1 , , xn ) ) Ű " x1 " xn A ( f ( x1 , , xn ) , x1 , , xn ) Ha az univerzális kvantorok ( " ) hatásköre nagyobb a szükségesnél, akkor toljuk jobbra ezeket a formulában. pl. " x ( $ y1 P ( y1 ) Ů $ y2 Q ( x , y2 ) ) Ű " x [ P ( f (x) ) Ů Q ( x , g (x) ) ] ô $ y1 P ( y1 ) Ů " x $ y2 Q ( x , y2 ) Ű P ( a ) Ů " x Q ( x , g (x) ) Mivel a P predikátum szimbólum nem függ az x indivduum változótól, az első sorban feleslegesen írtuk egy függvényt f (x), ezért jobb a második sor szerinti felírás. 5. Prenex formára hozás Mivel a formulában már csak az univerzális kvantorok (") vannak, ezek kivehetők a formula elé, tehát ezután a formula a következőképpen néz ki : " x1 .

" xn A ( x1 , , xn ) 6. Klózok kialakítása A Ú (B Ů C) Ű (A Ú B) Ů (A Ú C) 7. Az univerzális kvantorok (") elhagyása 8. Konjunkciók elhagyása (ez már egy klózhalmaz) 9. A klózokban szereplő változók átnevezése, hogy két különböző klóz ne tartalmazza ugyanazon változókat. Tétel Egy formula klóz formája acsa kielégíthető, ha az eredeti formula is kielégíthető Skolem tétel 0. rendű esetben Ci = p Ú Ci , Cj = ¬p Ú Cj -ből R ( Ci , Cj ) = ( Cj Ú Cj ) Egy literál 1. rendű esetben P ( t1 , , tn ) , ¬P ( t1 , , tn ) jellegű predikátum szimbólumokból állhat, ahol t1 , , tn termek Ci = P ( x ) Ú Ci , Cj = ¬P ( f (x) ) Ú Cj 1. rendű esetben A probléma 1. rendű esetben csak az, hogy az R ( Ci , Cj ) milyen eredményt ad különböző argumentumok esetén. Egyesítés (unifikáció) Def.: Helyettesítésnek nevezzük azt a { v1 / t1 , . , vn / tn } halmazt, ahol a vi -k (1 Ł i Ł n) páronként különböző

változók, és ti -k termek és vi ą ti . Az üres helyettesítés jele : Ć Def.: Ha az A formula és az a = { v1 / t1 , . , vn / tn } helyettesítés, akkor Aa -t A egy példányának nevezzük, amelyet úgy kapunk, hogy A-ban vi változókat (1 Ł i Ł n) ti termekkel helyettesítjük. pl.: A = P ( x , f (x) , y ) Def.: a = { x / a , y / g (b) } Aa = P ( a , f (a) , g (b) ) Legyenek a = { x1 / t1 , . , xn / tn } és b = { y1 / u1 , , ym / um } helyettesítések Ekkor ezek ab kompozícióján a következő helyettesítést értjük : ab = { x1 / t1 b , . , xn / tn b , y1 / u1 , , ym / um } amelyekből törlendő minden olyan xi / ti b (1 Ł i Ł n), ahol xi = ti b illetve azon yj / uj (1 Ł j Ł m), ahol yj Î { x1 , . , xn } pl.: a = { x / f (y) , y / z } b = { x / u , y / b , z / y } ab = { x / f (b) , y / y , x / u , y / b , z / y } { y / y , x / u , y / b } Tehát ab = { x / f (b) , z / y } lesz a végső kompozíció. Def.: Ha A1 , . , An formulák, akkor az a (nem

egyértelműen meghatározott) helyettesítést egyesítő helyettesítésnek (egyesítőnek) nevezzük, ha A1 a = . = An a Def.: A d helyettesítés az a1 , . , an egyesítők legáltalánosabb egyesítőjének nevezzük, ha minden ai -hez létezik olyan ai helyettesítés, hogy ai = dai . Def.: Az A1 , . , An formulák különbségi halmazát úgy kapjuk, hogy balról jobbra haladva a formulákban azonosítjuk azt a pozíciót, amelyen a formulák először eltérnek egymástól. Az ezen pozíción kezdődő részformulák képzik A1 , . , An különbségi halmazát pl.: P ( x , g ( f ( y , z ) , x ) ) P(x,g(a,g(y,z))) P(x,g(a,b)) - az eltérés kezdőpontja, tehát a D különbség halmaz D = { a , f ( y , z ) } Egy formula legáltalánosabb helyettesítőjének megkeresése procedure egyesítés d := 0 NemEgyesíthető := FALSE WHILE not (|H| or NemEgyesíthető ) DO D := különbségi halmaz select (D , v , t) ahol vĎt változó, és t term IF { v , t } = Ć THEN

NemEgyenlő := TRUE ELSE d:=d{v/t} , H:=H{v/t} end IF end DO end egyesítés A ciklus kilépési feltétele, hogy elfogyjanak az egyesíthető predikátumok, vagy a H halmaz elemszáma egyre csökkenjen. Minden iterációban megszabadul egy változótól Pld.1: az egyesítési algoritmusra (a cél nem a H halmaz egyesítése elsősorban, hanem ezen halmaz d legáltalánosabb egyesítőjének megtalálása) H = { Q ( f (a) , g (x) ) , Q ( y , y ) } a kiinduló halmaz 1. iteráció D = { f (a) , y } d = { y/f (a) } H = { Q ( f (a) , g (x) ) , Q ( f (a) , f (a) ) } 2. iteráció D = { g (x) , f (a) } de ez már nem egyesíthető Pld.2: H = { P ( x , u , f (g (x)) ) , P ( a , y , f (y) ) } a kiinduló halmaz 1. iteráció 2. iteráció 3. iteráció D={x,a} d = { x/a } H = { P ( a , u , f (g (a)) ) , P ( a , y , f (y) ) } D={u,y} d = { x/a , u/y } H = { P ( a , y , f (g (a)) ) , P ( a , y , f (y) ) } D = { g (a) , y } d = { x/a , u/g (a) , y/g (a) } H = { P ( a , g (a) , f (g (a)) ) , P (

a , g (a) , f (g (a)) ) } így a két predikátum ekvivalens lett, tehát egyesíthetők. A H halmaz legáltalánosabb egyesítője pedig d A rezolúció algoritmusa (1. rendű logika esetén) procedure rezolúció (a konjunktív normál formára hozás után) klózok := s WHILE NIL Ď klózok DO select (klózok , Ci , Cj) úgy, hogy Ci , Cj rezolválhatók legyenek Cij = R (Ci , Cj ) a rezolúciós lépés klózok := klózok Č Cij end DO end rezolúció Tehát az algoritmus menete megegyezik a 0. rendű logikánál leírtakkal, de két dolgot másképp kell értelmezni, finomítani kell a 0. rendűhöz képest : - Mit jelent a Ci , Cj rezolválhatósága ? - Az R rezolúciós művelet mit is csinál valójában ? Def.: Azt mondjuk, hogy a Ci , Cj klózok rezolválhatók, ha létezik r és s előfordulási szám, valamint Ci , Cj felírható a következő alakban : Ci = P ( t11 , . , t1n ) Ú Ú P ( tr1 , , trn ) Ú Ci Cj = P ( u11 , . , u1n ) Ú Ú P ( us1 , , usn ) Ú Cj (n a

predikátumok argumentumszám, meg kell hogy egyezzen; t,u tetszőleges termek), és az ezeket tartalmazó H halmaz (elemei a komplemens literálpárok) egyesíthető. H = { P ( t11 , . , t1n ) , P ( tr1 , , trn ) , P ( u11 , , u1n ) , P ( us1 , , usn )} Legyen ekkor a H halmaz legáltalánosabb egyesítője d, ekkor Cij = R (Ci , Cj ) = Cid Ú Cjd Példa: A1 := "Van olyan páciens, aki minden doktorban megbízik." premissza premissza A2 := "A kuruzslókban egyetlen páciens sem bízik meg." konklúzió A3 := "Egyetlen doktor sem kuruzsló." formalizálás predikátumok (igazságfüggvények kialakítása) P (x) = páciens (x) D (x) = doktor (x) M (x,y) = megbízik (x,y) K (x) = kuruzsló (x) A1 |> F1 = $ x ( P (x) Ů " y ( D (y) ® M (x,y) ) ) A2 |> F2 = " x ( P (x) ® " y ( K (y) ® ¬ M (x,y) ) ) A3 |> F3 = " x ( D (x) ® ¬ K (x) ) A tétel ( F1 Ů F2 ) ® F3 Ű ¬ ( F1 Ů F2 Ů ¬ F3 ) a logikai következménynél

leírt 3. tétel alapján A tétel negáltja F1 Ů F2 Ů ¬ F3 ennek kielégíthetetlenségét akarjuk bizonyítani Klóz formára hozás 9 lépésben 1. ® kiküszöbölése F1 = $ x ( P (x) Ů " y ( ¬ D (y) Ú M (x,y) ) ) F2 = " x ( ¬ P (x) Ú " y ( ¬ K (y) Ú ¬ M (x,y) ) ) ¬ F3 = ¬ [ " x ( ¬ D (x) Ú ¬ K (x) ) ] 2. negáció hatáskörének redukálása F1 = $ x ( P (x) Ů " y ( ¬ D (y) Ú M (x,y) ) ) F2 = " x ( ¬ P (x) Ú " y ( ¬ K (y) Ú ¬ M (x,y) ) ) F3 = $ x ( D (x) Ů K (x) ) 3. változók standardizálása F1 = $ x ( P (x) Ů " y ( ¬ D (y) Ú M (x,y) ) ) F2 = " z ( ¬ P (z) Ú " w ( ¬ K (w) Ú ¬ M (z,w) ) ) F3 = $ s ( D (s) Ů K (s) ) 4. egzisztenciális kvantorok kiküszöbölése F1 = P (a) Ů " y ( ¬ D (y) Ú M (a,y) )a - Skolem konstans F2 = " z ( ¬ P (z) Ú " w ( ¬ K (w) Ú ¬ M (z,w) ) ) F3 = D (b) Ů K (b) b - Skolem konstans 5. Prenex formára hozás (univerzális kvantorok

kiemelése)F1 Ů F2 Ů F3 " y " z " w [ P (a) Ů ( ¬ D (y) Ú M (a,y) ) ] Ů [ ¬ P (z) Ú ( ¬ K (w) Ú ¬ M (z,w) ) ] Ů [ D (b) Ů K (b) ] 6. 7 Klózok kialakítása + univerzális kvantorok elhagyása P (a) Ů ( ¬ D (y) Ú M (a,y) ) Ů [ ¬ P (z) Ú ¬ K (w) Ú ¬ M (z,w) ] Ů D (b) Ů K (b) 8. Konjunkciók elhagyása az így kapott halmaz már a rezolúció kiinduló halmaza P (a) ¬ D (y) Ú M (a,y) ¬ P (z) Ú ¬ K (w) Ú ¬ M (z,w) D (b) K (b) A rezolúció menete 6. = 1 és 3 (P,¬P) { z/a } ¬ K (w) Ú ¬ M (a,w) 1. P (a) 2. ¬ D (y) Ú M (a,y) 7. = 2 és 6 (M,¬M) { w/y } ¬ D (y) Ú ¬ K (y) 8. = 4 és 7 (D,¬D) { y/b } ¬ K (b) 3. ¬ P (z) Ú ¬ K (w) Ú ¬ M (z,w) 4. D (b) 9. = 5 és 8 (K,¬K) NIL 5. K (b) Megj1 a rezolúciós algoritmus nem determinisztikus, mert - nincs meghatározva, mely klózokat válasszuk, ha több lehetséges is van, - mely literálok szerint rezolváljunk, ha több lehetséges komplemens is van; - a lehetséges rezolválandó

literálok száma (r,s előfordulási szám) sem meghatározott. Az algoritmus determinisztikussá tehető rezolúciós stratégiák alkalmazásával. Megj2 - Ha az algoritmussal bizonyítandó tétel érvényes, azt véges lépésen belül biztos levezeti, - de ha a tétel kielégíthetetlen volt, semmi garanciát nem biztosít arra, hogy valamikor is leálljon (az interpretációk végtelen száma miatt). A véges lépésszám időtartamára nem lehet becslést adni nagy formulák esetén. A fentiekben gyakran használt rövidítések jelentése: " - minden (csak a 4. oldalig) acsa - akkor és csak akkor tfh - tegyük fel, hogy Ď - nem eleme Î - eleme based on the PROLOG lab lectures perfomed by Andrew Takáts created by Calden in the year of 1996 minimized by eszpee in year mentioned above