Tehát most a célunk az, hogy egy következtető rendszert adjunk meg, ami elsőrendű logikai formulák egy Σ halmazára és egy F célformulára ha Σ⊨F igaz, akkor arra előbb-utóbb rájön, ha meg nem következmény, akkor nem jön ki azzal a válasszal, hogy "következménye".
(Olyan algoritmus matematikailag igazoltan nincs, ami arra is garantáltan rájönne, hogy
nem
következménye egy formula egy másiknak, itt a legjobb amit remélhetünk, az az, hogy vagy rájön az algoritmus, hogy nem következmény, vagy végtelen ciklusba esik.)
Erre a problémára (ezen a kurzuson) kétféle rezolúciós algoritmust fogunk nézni: az egyiknek a neve "alap rezolúció" lesz, a másiké meg (ravasz módon) "elsőrendű rezolúció". Mindkettő, hasonlóan az ítéletkalkulus-beli változatukhoz, arra lesz jó, hogy egy input formulahalmazról megmutassa, hogy
kielégíthetetlen, azzal, hogy levezeti belőle az üres klózt.
Ugyanúgy, ahogy a ítéletkalkulus rezolúciós algoritmusához is egy ottani normálformára (CNF-re) kellett hozni az inputot, itt is: ezt a normálformát zárt Skolem (ejtsd: Szkólem) alaknak hívják.
Ebben a posztban megnézzük, hogy
hogyan hozunk egy formulát zárt Skolem alakúra, az eredmény "magját" pedig CNF-re, a következőben pedig
bebizonyítjuk, hogy amit csinálunk, az jó lesz, ha az input kielégíthetetlenségét akarjuk bizonyítani. (Ez most
nem lesz ekvivalens az inputtal, amit gyártunk, de "majdnem". Ezt a következőből megértjük.)
Tehát, induljunk ki egy formulából, az algoritmust példán keresztül is visszük végig. Legyen mondjuk ez:
∀x(∃yp(f(x),y) →r(x)) ∧ ∃x∀y(p(y,f(x))∨q(z)) ∧ ¬q(z) ∧ ∀z¬r(z).
|
-
Elimináljuk a → és ↔ konnektívákat a szokásos
F→G≡¬F∨GF↔G≡(¬F∨G)∧(F∨¬G)azonosságokkal.
Most ennek az eredménye ezen a formulán az egyetlen → konnektíva kiütése után:
∀x(¬∃yp(f(x),y) ∨r(x)) ∧ ∃x∀y(p(y,f(x))∨q(z)) ∧ ¬q(z) ∧ ∀z¬r(z) -
Kiigazítás: Átnevezzük a változókat, hogy különböző kvantor előfordulások különböző változókat kössenek le, és ne legyen olyan változó sem, ami szabadon is és kötötten is előfordul. A szabad változókat nem nevezhetjük át.
Ennek egy módja pl (ha az input formulánkban amúgy nincsenek indexelve a változók), hogy indexeljük az összes kötött változót, akár 1-től kezdve sorfolytonosan, minden egyes kvantornál növelve az indexet, akár változónként külön-külön indexet vinni, mindegy, csak ne legyen névütközés.
Arra persze figyeljünk oda, hogy ha egy kvantor mellett álló változót átnevezünk valamire, akkor pontosan azokat a változóelőfordulásokat kell átneveznünk ugyanerre, melyeket ez a kvantorelőfordulás köt.
A munkaformulánkon ennek a lépésnek ez lesz (pl) az eredménye:
∀x1(¬∃y2p(f(x1),y2) ∨r(x1)) ∧ ∃x3∀y4(p(y4,f(x3))∨q(z)) ∧ ¬q(z) ∧ ∀z5¬r(z5)Itt most minden kvantorelőfordulás egy közös indexet növelt. Látszik, hogy a z az egyetlen változó, mely előfordul szabadon is, de azt kétszer teszi. Nem baj. -
Prenex alakra hozás: ennek a lépésnek az a célja, hogy az összes kvantor a formula elejére kerüljön. Ezt tehetjük pl. a következő kvantorkihúzási azonosságokkal, amik akkor igazak, ha a formula kiigazított:
(QxF)∙G≡Qx(F∙G)F∙(QxG)≡Qx(F∙G)¬∃xF≡∀x¬F¬∀xF≡∃x¬FHa ezeket a szabályokat alkalmazgatjuk a munkaformulánkon, akkor ilyesmi lépéseket kapunk:
∀x1(¬∃y2p(f(x1),y2) ∨r(x1)) ∧ ∃x3∀y4(p(y4,f(x3))∨q(z)) ∧ ¬q(z) ∧ ∀z5¬r(z5)∀x1(∀y2¬p(f(x1),y2) ∨r(x1)) ∧ ∃x3∀y4(p(y4,f(x3))∨q(z)) ∧ ¬q(z) ∧ ∀z5¬r(z5)∀x1∀y2(¬p(f(x1),y2) ∨r(x1)) ∧ ∃x3∀y4(p(y4,f(x3))∨q(z)) ∧ ¬q(z) ∧ ∀z5¬r(z5)
és ezen a ponton van négy formulánk éselve, mindnek az elején kvantorok, kihozzuk mindet:∀x1∀y2∃x3∀y4∀z5((¬p(f(x1),y2) ∨r(x1)) ∧ (p(y4,f(x3))∨q(z)) ∧ ¬q(z) ∧ ¬r(z5))
Egy másik módszer, ami kézzel végrehajtva gyorsabb kicsit, ha az ember átlátja a formulát (programmal mindenképp gyorsabb, ha a formulánkat fában reprezentáljuk):
- fogjuk az eredeti kigazított, nyílmentesített formulát
- a benne levő kvantált változókat balról jobbra, az eredeti deklarációs sorrendben kötjük le
- egy változót lekötő kvantor "megfordul" (∃-ből ∀ lesz és fordítva), ha páratlan sok ¬ jel hatáskörébe esik; ha pároséba, akkor nem fordul meg
- végül, a formula magját (így hívják a prenex formuláknak azt a részformuláját, amelyikben már épp nincs kvantor) úgy kapjuk, hogy az eredeti formulából kitöröljük a kvantorokat.
∀x1(¬∃y2p(f(x1),y2) ∨r(x1)) ∧ ∃x3∀y4(p(y4,f(x3))∨q(z)) ∧ ¬q(z) ∧ ∀z5¬r(z5)a sorrend x1, y2, x3, y4, z5 lesz; három negálás van a formulában, nincsenek egymásba ágyazva, így ezt most egyszerű látni, hogy csak az ∃y2 az egyetlen kvantált változó, aki páratlan sok (egy) negálás belsejében van, így ő az egyetlen, aki megfordul. A kvantor prefix tehát ∀x1∀y2∃x3∀y4∀z5 lesz. Utánaírjuk a formulánkat úgy, hogy kitöröljük a kvantorokat éééés:
∀x1∀y2∃x3∀y4∀z5((¬p(f(x1),y2) ∨r(x1)) ∧ (p(y4,f(x3))∨q(z)) ∧ ¬q(z) ∧ ¬r(z5))yep, ugyanaz lett, mint az előbb. -
Skolem alakra hozás: ennek a lépésnek a célja, hogy csak ∀-kvantorok maradjanak a formulában (és persze maradjon prenex alakban). Az előző lépések ekvivalens átalakítások voltak, ez már nem lesz az. Ahogy csináljuk:
- kiindulunk a prenex, kiigazított alakból
- minden egyes ∃y-ra
- kitöröljük az ∃y-t a formula elejéről
- és y minden előfordulásának helyébe a magban egy f(x1,…,xn) termet írunk
- ahol is f egy teljesen új függvényjel (amit Skolem függvénynek is hívnak), amit most generáltunk -- ha egyszerre több formulát hozunk Skolem alakra, akkor meg kell nézni, hogy egyikben sem szerepelhet! Ha több Skolem függvényjelet generálunk, akkor mind egymástól is különböző kell legyen!
- az x1,…,xn változók pedig azok, akik az y előtt (attól balra) vannak ∀ kvantorral kötve a formulában.
nézzük ezt a munkaformulánkon, itt tartunk:
∀x1∀y2∃x3∀y4∀z5((¬p(f(x1),y2) ∨r(x1)) ∧ (p(y4,f(x3))∨q(z)) ∧ ¬q(z) ∧ ¬r(z5))sok dolgunk nincs ezzel most, egyetlen ∃ kvantor van benne, ami x3-at köti. Keresünk egy új függvényjelet, amit még nem használunk, ez pl most lehet g (f viszont nem), és függni fog x1-től és y2-től, mert azok vannak x3 előtt univerzálisan deklarálva. Tehát, töröljük a ∃x3 részt és a formulában x3 minden előfordulása helyébe g(x1,y2)-t írunk:
∀x1∀y2∀y4∀z5((¬p(f(x1),y2) ∨r(x1)) ∧ (p(y4,f(g(x1,y2)))∨q(z)) ∧ ¬q(z) ∧ ¬r(z5))
ez így most kész is, a formula Skolem alakú. -
Lezárás: ennek a lépésnek a célja, hogy ne legyen szabad változónk. Ezt úgy érjük el, hogy minden x szabad változóelőfordulás helyébe egy új, x-től függő konstanst, pl. cx-et írunk. Szintén fontos, hogy a konstans új legyen, itt viszont ha több formulában is szerepel szabadon ugyanaz az x, akkor mindegyikben ugyanazt a cx-et kell írjuk a helyébe!
Folytatva az előző példánkat: z az egyetlen szabadon előforduló változó, ő kétszer is szerepel, helyére bekerül a cz konstans:
∀x1∀y2∀y4∀z5((¬p(f(x1),y2) ∨r(x1)) ∧ (p(y4,f(g(x1,y2)))∨q(cz)) ∧ ¬q(cz) ∧ ¬r(z5)) -
A mag CNF-re hozása: teljesen ugyanazzal a módszerrel, mint ítéletkalkulusban, a zárt Skolem alakú formulánk magját CNF-re hozzuk. Most
- literál minden atomi formula (ők pozitívak) és azok negáltjai (ők negatívak), vagyis a predikátumjellel kezdődő, vagy esetlegesen negált predikátumjellel kezdődő részek
- klóz továbbra is véges sok literál vagyolása
- a CNF pedig továbbra is klózok éselése
| Ha megnézzük, a mostani munkaformulánkban literálok pl. a ¬p(f(x1),y2), az r(x1), a p(y4,f(g(x1,y2))), a q(cz), a ¬q(cz) és a ¬r(z5), de most teljesen jól vannak, literálok vannak vagyolva egy- vagy kéttagú klózokká, és ilyen klózból van négy. Akár le is írthatjuk őket egy Σ klózhalmazba, ugyanúgy halmazként reprezentálva mindent, mint ítéletkalkulusban tettük:
{{¬p(f(x1),y2),r(x1)}, {p(y4,f(g(x1,y2))),q(cz)}, {¬q(cz)}, {¬r(z5)}}.
|
Ez minden; mindkét rezolúciós algoritmus ebben a formátumban, zárt Skolem alakú formulákként, melyeknek a magját CNF-re hoztuk és az összes klózt egy Σ halmazba tesszük. Hogy mit tesznek vele, azt meglátjuk, miután megnézzük, hogy ezek az átalakítások tényleg jók lesznek nekünk.
No comments:
Post a Comment