Tehát most a célunk az, hogy egy következtető rendszert adjunk meg, ami elsőrendű logikai formulák egy $\Sigma$ halmazára és egy $F$ célformulára ha $\Sigma\vDash 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:
$\forall x(\exists yp(f(x),y)~\to r(x))~\wedge~\exists x\forall y(p(y,f(x))\vee q(z))~\wedge~\neg q(z)~\wedge~\forall z\neg r(z)$.
|
-
Elimináljuk a $\to$ és $\leftrightarrow$ konnektívákat a szokásos
$\begin{align*}F\to G&\equiv\neg F\vee G&F\leftrightarrow G&\equiv(\neg F\vee G)\wedge(F\vee\neg G)\end{align*}$azonosságokkal.
Most ennek az eredménye ezen a formulán az egyetlen $\to$ konnektíva kiütése után:
$\forall x(\neg\exists yp(f(x),y)~\vee r(x))~\wedge~\exists x\forall y(p(y,f(x))\vee q(z))~\wedge~\neg q(z)~\wedge~\forall z\neg 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:
$\forall x_1(\neg\exists y_2p(f(x_1),y_2)~\vee r(x_1))~\wedge~\exists x_3\forall y_4(p(y_4,f(x_3))\vee q(z))~\wedge~\neg q(z)~\wedge~\forall z_5\neg r(z_5)$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:
$\begin{align*}(Qx F)\bullet G&\equiv Qx(F\bullet G)\tag{minden $Q\in\{\exists,\forall\}$, $\bullet\in\{\vee,\wedge\}$ esetén}\\F\bullet(QxG)&\equiv Qx(F\bullet G)\tag{minden $Q\in\{\exists,\forall\}$, $\bullet\in\{\vee,\wedge\}$ esetén}\\\neg\exists xF&\equiv\forall x\neg F\\\neg\forall xF&\equiv \exists x\neg F\end{align*}$Ha ezeket a szabályokat alkalmazgatjuk a munkaformulánkon, akkor ilyesmi lépéseket kapunk:
$\forall x_1(\neg\exists y_2p(f(x_1),y_2)~\vee r(x_1))~\wedge~\exists x_3\forall y_4(p(y_4,f(x_3))\vee q(z))~\wedge~\neg q(z)~\wedge~\forall z_5\neg r(z_5)$$\forall x_1(\forall y_2\neg p(f(x_1),y_2)~\vee r(x_1))~\wedge~\exists x_3\forall y_4(p(y_4,f(x_3))\vee q(z))~\wedge~\neg q(z)~\wedge~\forall z_5\neg r(z_5)$$\forall x_1\forall y_2(\neg p(f(x_1),y_2)~\vee r(x_1))~\wedge~\exists x_3\forall y_4(p(y_4,f(x_3))\vee q(z))~\wedge~\neg q(z)~\wedge~\forall z_5\neg r(z_5)$
és ezen a ponton van négy formulánk éselve, mindnek az elején kvantorok, kihozzuk mindet:$\forall x_1\forall y_2\exists x_3\forall y_4\forall z_5\Bigl((\neg p(f(x_1),y_2)~\vee r(x_1))~\wedge~(p(y_4,f(x_3))\vee q(z))~\wedge~\neg q(z)~\wedge~\neg r(z_5)\Bigr)$
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" ($\exists$-ből $\forall$ lesz és fordítva), ha páratlan sok $\neg$ 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.
$\forall x_1(\neg\exists y_2p(f(x_1),y_2)~\vee r(x_1))~\wedge~\exists x_3\forall y_4(p(y_4,f(x_3))\vee q(z))~\wedge~\neg q(z)~\wedge~\forall z_5\neg r(z_5)$a sorrend $x_1$, $y_2$, $x_3$, $y_4$, $z_5$ lesz; három negálás van a formulában, nincsenek egymásba ágyazva, így ezt most egyszerű látni, hogy csak az $\exists y_2$ 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 $\forall x_1\forall y_2\exists x_3\forall y_4\forall z_5$ lesz. Utánaírjuk a formulánkat úgy, hogy kitöröljük a kvantorokat éééés:
$\forall x_1\forall y_2\exists x_3\forall y_4\forall z_5\Bigl((\neg p(f(x_1),y_2)~\vee r(x_1))~\wedge~(p(y_4,f(x_3))\vee q(z))~\wedge~\neg q(z)~\wedge~\neg r(z_5)\Bigr)$yep, ugyanaz lett, mint az előbb. -
Skolem alakra hozás: ennek a lépésnek a célja, hogy csak $\forall$-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 $\exists y$-ra
- kitöröljük az $\exists y$-t a formula elejéről
- és $y$ minden előfordulásának helyébe a magban egy $f(x_1,\ldots,x_n)$ 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 $x_1,\ldots,x_n$ változók pedig azok, akik az $y$ előtt (attól balra) vannak $\forall$ kvantorral kötve a formulában.
nézzük ezt a munkaformulánkon, itt tartunk:
$\forall x_1\forall y_2\exists x_3\forall y_4\forall z_5\Bigl((\neg p(f(x_1),y_2)~\vee r(x_1))~\wedge~(p(y_4,f(x_3))\vee q(z))~\wedge~\neg q(z)~\wedge~\neg r(z_5)\Bigr)$sok dolgunk nincs ezzel most, egyetlen $\exists$ kvantor van benne, ami $x_3$-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 $x_1$-től és $y_2$-től, mert azok vannak $x_3$ előtt univerzálisan deklarálva. Tehát, töröljük a $\exists x_3$ részt és a formulában $x_3$ minden előfordulása helyébe $g(x_1,y_2)$-t írunk:
$\forall x_1\forall y_2\forall y_4\forall z_5\Bigl((\neg p(f(x_1),y_2)~\vee r(x_1))~\wedge~(p(y_4,f(g(x_1,y_2)))\vee q(z))~\wedge~\neg q(z)~\wedge~\neg r(z_5)\Bigr)$
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. $c_x$-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 $c_x$-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 $c_z$ konstans:
$\forall x_1\forall y_2\forall y_4\forall z_5\Bigl((\neg p(f(x_1),y_2)~\vee r(x_1))~\wedge~(p(y_4,f(g(x_1,y_2)))\vee q(c_z))~\wedge~\neg q(c_z)~\wedge~\neg r(z_5)\Bigr)$ -
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 $\neg p(f(x_1),y_2)$, az $r(x_1)$, a $p(y_4,f(g(x_1,y_2)))$, a $q(c_z)$, a $\neg q(c_z)$ és a $\neg r(z_5)$, 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 $\Sigma$ klózhalmazba, ugyanúgy halmazként reprezentálva mindent, mint ítéletkalkulusban tettük:
$\left\{\{\neg p(f(x_1),y_2),r(x_1)\},~\{p(y_4,f(g(x_1,y_2))),q(c_z)\},~\{\neg q(c_z)\},~\{\neg r(z_5)\}\right\}$.
|
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 $\Sigma$ 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