19. tétel: Logikai reprezentáció

Az elsőrendű predikátumkalkulus jellemzése: szintaxis, szemantika, logikai következmény, konjuktív normálforma. Tételbizonyítás rezolúcióval. Rezolúciós stratégiák. Válaszadás rezolúcióval

Az elsőrendű predikátumkalkulus (ERP) nyelve az MI feladatok reprezentálásához megfelelő. Igaz-hamis állítások megfogalmazása, lehetséges a „létezik” és a „minden” fordulatok kifejezése. Az ERP egy formulájának végtelen sok implementációja lehetséges az alaphalmazon, az alaphalmazon értelmezett függvények és predikátumok tetszőleges választásának segítségével.

Egy formula:

Érvényes, ha minden interpretációban igaz;

Kielégíthető, ha valamely interpretációban igaz, azaz létezik modellje;

Kielégíthetetlen, ha minden interpretációban hamis értékű, azaz nincsen modellje;

ekvivalens egy formulával, ha minden interpretációban azonos az igazságértékük.

ERP szintaxisa:

elválasztójelek: (), [], {}

logikai műveleti jelek: ~, &, v, , 

kvantorok: univerzális (), egzisztenciális ()

elemváltozók (individuum változók): x, y, z, …

elemkonstansok (individuum konstans): a, b, c, …

függvényszimbólumok: f, g, h,

ítéletváltozók: p, q, r, …

ítéletkonstansok: T, F (igaz-hamis)

predikátumszimbólumok (predikátumok: logikai függvények): P, Q, R … (vagy jellegzetes szavak is jelölhetik)

A jelkészlet elemeiből kifejezések építhetőek fel. A kifejezéseknek három osztályát különböztethetjük meg:

term:

minden elemkonstans

minden elemváltozó

ha t(1) … t(n) term és f egy n-argumentumú fgv.szimbólum, akkor f(t(1) … t(n)) is term.

atomi formula:

minden ítéletváltozó

minden ítéletkonstans

ha t(1) … t(n) term és P egy n-argumentumú pred.szimbólum, akkor P(t(1) … t(n)) atomi formula.

formula:

minden atomi formula

ha A és B formula, akkor (~A), (A&B), (AvB), (AB), (AB) is formula

ha A formula, x változó, akkor (MINDENx)A, (LÉTEZIKx)A kifejezések formulák.

Precedencia sorrend a zárójelek feloldásához:

, , ~, &, v, , 

pl:

P(x): x egy páciens * D(y): y egy doktor * K(y): y egy kuruzsló * M(x,y): x megbízik y-ban

Ekkor a formalizált állítások:

F1: Létezik olyan páciens, aki minden doktorban megbízik.

(x)[P(x) & (y)(D(y)  M(x,y))]

F2: Minden páciensre igaz, hogy egy kuruzslóban sem bízik.

(x)[P(x)  (y)(K(y)  ~M(x,y))]

F3: Minden doktorra igaz, hogy nem kuruzsló.

(x)[D(x)  ~ K(x)]

ERP szemantikája:

A formulák az interpretáció és a kiértékelés segítségével kapnak jelentést.

Az interpretáció során először az értelmezés alaphalmazát (individuum-tartományát, legyen ez D) választjuk meg, majd a formula szimbólumaihoz hozzárendeléseket végzünk:

minden konstansszimbólum D egy elemét kapja,

minden n argumentumú fgv.szimbólumhoz rendeljünk hozzá egy
Dn  D leképezést,

minden n argumentumú predikátumszimbólumnak feleltessünk meg egy Dn  (T,F) leképezést.

Az interpretált formula kiértékelése (~A, A&B, AvB, AB, AB, (x)A, (x)A) az igazságtáblázatok segítségével történik.

Logikai következmény:

Egy W formula az A1, A2, … An formulák logikai következménye, ha minden olyan interpretációban, amelyben A1&A2&…&An igaz, a W formula is igaz.

Tétel: A W formula akkor és csak akkor logikai következménye az A1, A2, … An formuláknak, ha az A1&A2&…&An&~W kielégíthetetlen.

ERP tételbizonyítási eljárása a rezolúció:

formalizáljuk a tétel állításait,

klóz formák képzése (előfeltételek és a következmény negáltja),

a klózhalmazból levezetjük az üres klózt (a klózhalmaz kielégíthetetlenségének belátása).

(A tételbizonyítás során a következmény negáltját vesszük, kialakítjuk a klózhalmazt, és a kapott klózhalmaz kielégíthetetlenségét bizonyítjuk.)

A klóz forma kialakításához a következő transzformációs lépések szükségesek:

ekvivalencia és implikáció kiküszöbölése,

negáció hatásának csökkentése,

változók standardizálása,

egzisztenciális kvantor kiküszöbölése (Skolem-konstansok ((x)P(x) helyett P(a)) és Skolem függvények ((x)(y)P(x,y) helyett (x)P(x,g(x)), ahol g(x) minden x-hez a megfelelő y-t rendeli) segítségével),

prenex formára hozás, ( kvantor kiemelése – az így kapott formulában (x1) … (xn)A(x1 … xn) az A részformula a formula mátrixa)

klózok kialakítása, a mátrix konjuktív normálformájának kialakítása,

univerzális kvantorok elhagyása,

konjukciók elhagyása (klózhalmaz kialakítása),

változók átnevezése.

Konjuktív normálforma: klózok konjukciója (&).

Klóz: literálok diszjunkciója (v), illetve egyetlen literál is klózt alkot.

Literál: ítéletkonstans, ítéletváltozó vagy annak negáltja.

Az 1. – 6. lépések a Skolem-normálformára hozás lépései.

A klózhalmaz elemeiből a cáfolati gráf építhető fel. Ennek levelein klózok ülnek, melyek, ha komplemens literálpárt tartalmaznak, összevonhatóak: legyen pvA és ~pvB két klóz. Ezek rezolválhatóak, ha egyetlen komplemens literálpárt (jelen esetben p) tartalmaznak. A rezolválás következménye az AvB literál = az eredeti klózpár rezolvense. A rezolvens klózpárral bővítve a klózhalmazt, a kielégíthetőségi tulajdonság nem változik.

Az összevonások segítségével érhetjük el az üres klózt, azaz a tétel bizonyítását. A rezolúció folyamata az ERP-ben nem mindig egyértelmű, szükséges az egyesítési algoritmus:

Helyettesítés: véges {v1/t1 … vn/tn} halmaz, ahol vi-k különböző változók, ti-k term-ek.

Egy helyettesítés () egyesítő, amennyiben A1 = … An (Ai: formula).

Az {A1 … An} halmaz egyesíthető, ha létezik hozzá egyesítő.

Így a rezolválhatóság fogalma az ERP-ben kibővül: két klóz akkor rezolválható, ha alkalmas helyettesítéssel egyesíthető.

Rezolúciós stratégiák:

A rezolúció során használt klózpárok kiválasztásához kínál megoldásokat.

Egy stratégia teljes, ha a kielégíthetetlen klózhalmazból levezethető az üres klóz.

Minden más esetben a stratégia nem teljes.

szélességi (szintenként építi fel a rezolúciós gráfot, azaz: először képezzük az összes lehetséges rezolvenst, majd abból, a II. szinten képezhető összes lehetséges rezolvenst… - a stratégia teljes; kevésbé hatékony, noha a legrövidebb cáfolati utat is megmutatja)

lineáris input stratégiája (a rezolválás során fontos, hogy az egyik szülő a kiindulási klózhalmaz eleme legyen – nem teljes, de egyszerű és hatékony, a gyakorlatban sokszor használják; pl. prolog nyelvben)

ősre korlátozott stratégia (kiindulási klózhalmaz-beli az egyik szülő vagy a rezolúcióban levő klózpár egyike a másik őse – a lineáris input „gyengített” változata, ez teljes stratégia)

támogató halmaz stratégiája (eredeti célállítás negáltjából származó klózokból választjuk mindig a rezolválás egyik szülőjét)

egység klóz stratégiája (csak olyan rezolvensek képezhetők, melyek egyike egységklóz, azaz egyetlen literálból áll – a leghatékonyabb a többivel összevetve, de nem teljes, ezért általában egy másik, teljes stratégiával együtt alkalmazzák).

Válaszadás rezolúcióval:

Sok feladat reprezentálható bizonyítandó tétel formájában. Az ilyen alkalmazások során bizonyos tények, ismeretek alapján keressük a konkrét választ, azaz feladat annak az elemnek is a megadása, mely a feladatot kielégíti.

A gyakorlatban a megoldást a cáfolati gráf segítségével állíthatjuk elő. A célállítás negáltjához adva a célállítást, a cáfolati gráf struktúráját követve, felépíthető a bizonyítási gráf, amelyben az üres klóz helyén a keresett válasz jelenik meg.

Egy lehetséges feladat, melyre megoldást kínálhat a rezolúció:

Ha Fifi mindenhova követi Jánost, és János a parkban van, akkor hol található Fifi?

Az előfeltételek és a célállítás:

F1: (x)[H(János,x)  H(Fifi,x)]

F2: H(János,park)

F3: (x)H(Fifi,x)

MESTERSÉGES INTELLIGENCIA (MI)

Zak

2002-06-20T11:24:00

Peter Szamoskozi