Dr. Jelasity Márk Mesterséges Intelligencia I Előadás Jegyzet (2008. október 6) Készítette: Filkus Dominik Martin
Elsőrendű logika -Ítéletkalkulus : Az elsőrendű logika egy speciális esete, itt csak nullad rendű pedikátum szimbólumokat használunk. Részei: a) objektumok b) relációk c) függvény d) kvantorok Az ítéletkalkulus atomi ítéletei a relációk, amik vagy teljesülnek, vagy nem. Beleláthatunk az ítélet finomabb szerkezetébe => ha túl sok tény lehet, (pl ∞), ez fontos, mert kompakt és kifejezőbb. Szintaktika mondat
→
atom term összekötő kvantor kvantorok változók
→ → → → → →
atom | (összekötő mondat) | kvantor változó mondat | ⌐ mondat predikátum (term, …) | term = term függvény (term, …) | kvantorok | változó ∧|∨|→|↔ ∀|∃ A | B | C (nagybetűk) x | y | z (kisbetűk)
Szemantika Ítéletkalkulus egy lépése : Lehetséges világok közül választunk, ez a modell elsőrendű logika : Lehetséges világ a domain, ami a létező objektumok halmaza ( D ). Ehhez még kell egy interpretáció, ami a következő: • • •
Minden kvantorhoz rendel elemet a domainből Minden függvényhez (n változós) rendel egy Dn → D függvényt Minden predikátumnévhez (n változós) egy Dn → {igaz / hamis} függvényt
Egy fix domain-en, sok különböző interpretáció is lehet.
Kiértékelés (Igaz vagy Hamis a mondat) Kiterjesztett interpretáció: Minden változóhoz rendel egy domain elemet. Kiértékeléshez kiterjesztett interpretáció kell. Term kiértékelés: ( <= egy domain elem) • Konstans és változó : <= kiterjesztett interpretáció • Függvény F(t1,....,tn) : F -hez rendelt függvény kiértékelése a t1,...,tn termek kiértékeléseit behelyettesítve Atomi mondatok: (<= Igaz / Hamis) P(t1,..,tn) : t1,...,tn kiértékelését behelyettesítjük P kiértékelésébe Komplex mondatok: Mint az ítéletkalkulusban Kvantorok: Legyen f egy mondat, amelyben szerepel az x változó. x szabad változó, ha • f atomi mondat • <=> ⌐f1 -ben szabad változó • <=> f összetett (pl f1∧ f2) és x szabad f1-ben vagy f2-ben • f=∀ y f1 (vagy ∃ y f1) és x ≠ y x kötött változó, ha • x szerepel f-ben és nem szabad • legyen f=∀xf1(x) (x kötött változó) ekkor f kiértékelése igaz, akkor és csak akkor, ha az összes kiterjesztett interpretációban, ahol x értéke a domain minden elemét felveszi (míg a többi hozzárendelés nem változik), f1(x) igaz. • ∃ -nél ugyanez, csak elég egy igaz kiterjesztett interpretáció Logikai következmény T és f mondatok. Ekkor T |= f akkor és csak akkor, ha minden modellben és minden interpretációban, ahol T igaz értéket vesz fel, f is igaz értéket vesz fel. Megjegyzés: Ítéletkalkulusban lehetett direkt ellenőrizni (összes modell felsorolása vagy kielégíthetőség). Itt már nem lehet, végtelen lehetőség van. Megjegyzés: Az „=” operátor ugyanúgy működik mint egy predikátum, amiben az azonosság relációt rendeljük, mint interpretáció. Kvantorok kiértékelése • •
∀xf(x) = ⌐∃x ⌐f(x), stb (csak ∀ vagy ∃ is elég) ∃x∀y f(x,y) ≠ ∀y∃x f(x,y) (pl f(x,y) : x vezeti y-t)
gyakorlati megjegyzés: Egy elsőrendű logikai adatbázisban általában nem csak egy f(x1,...,x2) mondat érdekes, hanem, ha igaz, az interpretáció is. Pl ∃xP(x) -nél érdekes, hogy mi az az x ? (azaz melyik objektum ?) Példák • rokonság: a) objektumok : emberek b) predikátumok : férfi, nő (1 változós, nővér, szülő, stb) c) w-ek : Apa, Anya (lehetne kétváltozós predikátum is) tudás, pl • ∀x,y Anya(x) = y <=> Nő(y) ∧ Szülő (y,x) • ∀x,y Nagyszülő(x,y) ↔ ∃z (Szülő(x,z) ∧ Szülő (z,y)) • ∀x,y Unokatestvér(x,y) ↔ x ≠ y ∧ ∃p Szülő (p,x) ∧ Szülő (x,y) • Férfi (Péter, stb) •
matematikai példák: a) objektumok : természetes számok b) predikátumok : N(x) : x természetes szám c) függvények : S(x) : x rákövetkezője (x+1) d) kvantorok : nulla
Itt a cél az, hogy olyan axiómákat adjunk, amelyeknek lényegében csak a természetes számok a modellje. (izomorfizmus erejéig). Ez nem megy elsőrendű nyelven, mert van megszámlálhatatlan modell is a következő axiómákhoz. • • • • • •
N(0) ∀x → N(S(x)) ∀x 0 ≠ S(x) ∀x,y x ≠ y → S(x) ≠ S(y) ∀x N(x) → 0+x = x ∀x,y N(x) ∧ N(y) → S(m) + n = s(m + n)
indukciós axióma: vagy másodrendű nyelven vagy elsőrendűn, de akkor végtelensok axióma Logikai következtetés Hogyan általánosítsuk az ítéletkalkulus módszereit ? Van teljes módszer ? (igen ! Például a rezolúció) ötlet: Ítéletkalkulus következő outputmezőit „emeljük át” ehhez: a) kvantoroktól megszabadulunk b) következtetési szabályokat felemeljük (lifting) úgy, hogy a finomszerkezete (azaz változó hozzárendelése) figyelünk behelyettesításekkel popelem : a behelyettesítés szintaktikai operáció lesz.
kvantorok : • ∃xf(x) => f(c), ahol c skolem konstans szimbólum. Általában : skolemizáció: Ha y ∃ kvantorok között, és az x1,...,xn ∀-el kötött változókhoz tartozó ∀ kvantorok hatáskörében van, akkor helyettesítünk F(x1,...,xn ) skolem függvénnyel például: ∀x(∃yP(x,y)) => ∀x(P(x,F(x))) ∀xf(x) => f(x) elhagyjuk a kvantort és minden szabad változót ∀-nel kötöttnek tekintünk Megjegyzés: Logikai következmény szempontjából ekvivalens, de minden kvantorhoz új változónév kell: (pl ∀xP(x) ∧ ∀xR(x) => P(x) ∧ R(y)) Ebben az állapotban nincsenek kvantorok, csak predikátumok logikai kombinációi, ahol a termek lehetnek változók is. Lifting: P1',...,Pn', P1,...,Pn : atomok P1' ,... , Pn ' , P1∧… ∧ Pn→ q helyettesít Θ , q
Ahol Θ helyettesítés azon szabad változók helyettesítése olyan termekkel, amelyek más mondatokban előfordulnak. Például: Fekete H , Fekete x → ⌐ Hattyú x ⌐ Hattyú H ahol Θ = {x/H} Ezzel a helyettesítéssel Fekete(H), Fekete(x) -et azonos alakra hozzuk. Θ megtalálásához adható hatékony algoritmus, mely a legoptimálisabb hozzárendelést adja meg, azaz csak akkor rendel x-hez értéket, ha a másik literálban ugyanott nem változó van, hanem konstans vagy függvény.
Rezolúció Itt is ellentmondáshoz jutunk, mint az ítéletkalkulusban 1. Vegyük fel ⌐β -t : α ∧ β -ból indulunk 2. α ∧ ⌐β konjuktív normálformája kell • ⌐ -t automatikusan bevisszük • csak ∧ és ∨ marad • konstansoktól megszabadulunk • literálok klózait hozzuk létre (∧-t kivisszük)
egyetlen-szabály : két klózra l1 ∨ … ∨ l2 , m1 ∨ … ∨ mn helyettesít(Θ , l1 ∨ … ∨ li-1 ∨ li+1 ∨ … ∨ l2 ∨ m1 ∨ … ∨ mj-1 ∨ mj+1 ∨ … ∨ mn) (lifting a rezolúció szabályhoz) ahol helyettesít (Θ, li) = helyettesít (Θ, ⌐mj) Tétel A rezolúció cáfolás-teljes, azaz ha β logikai következmény, találunk bizonyítást, de ha nem, akkor nem kell bizonyítani.
Bizonyítás Hasonló mint az ítéletkalkulus, de néhány extra lépés : kihagyjuk Gödel tétele Minden ellentmondásmentes, a természetes számok elméletét tartalmazó, formális-axiomatikus elméletben megfogalmazható olyan mondat, mely se nem bizonyítható, se nem cáfolható. Előre-hátra láncolás Horn-hoz hasonló adatbázis formátum. Határozott klóz : f1∧ f2 ∧...∧ fk → fk+1, ahol fi-k atomok (pozitív literálok) Tények: pozitív literál Literálok paraméterei: ha csak konstans vagy változó, akkor DATALOG formátum (függvényt nem engedünk) Kvantorokat továbbra is úgy kezeljük, ahogy eddig ötlet: Két módus ponens-t használunk a liftingel → ugyanaz, mint az ítéletkalkulus, de 1. algoritmus kell, az összes lehetséges helyettesítés megtalálásához 2. akkor van vége, ha egy új formula és a bizonyítandó α közös alakra hozható helyettesítésnek, vagy nincs új formula (ekkor α nem logikai következmény) DATALOG adatbázison mindig megáll, de egyébként nem. Pl.: 1. N(0) 2. N(x) → N(S(x)) -ből generálva N(S(0)), N(S(S(0))), stb A logikai következmények száma végtelen, nemtudjuk mikor kell megállni Félig eldönthető, ha α nem következmény, akkor nem áll meg, ha igen, akkor leáll
A változók miatt az elsőrendű logikában a modus ponens lehetséges alakjainak előállítása NP nehéz ! Példa probléma:
D : különböző D(wa, nt) ∧ S(wa, sa) ∧ D(nt, q) ∧... stb → színezhető tények : D(piros, kék), D(piros, zöld), stb A gyakorlatban nem feltétlenül nehéz heurisztikák: pl egy f1∧...∧ f2 először azt, ami a legnehezebben kielégíthető alapvető probléma: irreleváns következtetések
=> visszafelé láncolás Ugyanaz, mint az ítéletkalkulus, csak a helyettesítésekre kell figyelni 1. A helyettesítések Θ halmaza kezdetben üres 2. Mélységi bejárással ezt a halmazt fokozatosan bővítjük, hozzáadva az új helyettesítéseket (amíg lehet) 3. A művelet sikeres, ha eljutunk a tényekig, melyek a levelekben vannak, ebben az esetben megkapjuk a behelyettesítést is. 4. A mélyésgi keresés miatt nem teljes és ismétlődő állapotok is lehetnek. Logikai programozás A logikai programozás esetében a programokat relációkkal specifikáljuk. A program futása az logikai következtetésen alapszik. Prolog: Legkiemeltebb környezet Hátrafelé láncolás, határozott klózok a tudásanyag szintaxis pl: A(x,y) ∧ B(x) → C(x) kb. c(x) :- A(x,y), B(x) Néhány kompromisszummal számolni kell: Pl.: predikátumnak van mellékhatása (input/output, stb) néhány gond például a) (1) path (X,Z) :- link (X,Z) (2) path(X,Z) :- path(X,Y), link (Y,Z) (nagybetű: változó, kisbetű: konstans) Az A → B → C gráfon végtelen ciklus következik, ha fordított sorrendben írjuk fel a szabályt ((2),(1)) ( <= mélységi keresés)
Ugyanazt az állapotot többször is elérjük, azonban lehet hatékonysági gond Sok lehetséges útvonal A-ból B-be, ezekből sok a fölösleg Végeredményeket táblázatba lehet tárolni (<= dinamikus programozás) Automatikus tételbizonyítás Nem csak határozott klózok vesznek részt, elsőrendű formulák A :- B,C A:- C,B nem mindegy a sorrend OTTER – 4 részre osztjuk a tudásbázist • támogató halmaz • pontos tények • használható axiómák • háttértudás Átírók termekhez, pl x+0 = x kontroll info pl heurisztika, keresés szabályozásához működés: rezolúció, ahol a támogató halmaz egy elemét és egy axiómát rezolválunk, a „legkönnyebb” klózt választjuk. A halmazhoz aztán klózokat adunk alkalmazás: néhány területen, algebra, számelmélet
