Sztuczna inteligencja/SI Moduł 2/Postaci normalne formuł

Postaci normalne formuł

Aby uzyskać pełny system wnioskowania z niewielką liczbą aksjomatów i reguł, można ograniczyć się do wykorzystywania wyłącznie formuł w pewnych określonych postaciach, nazywanych postaciami normalnymi. Jeśli każda z formuł należących do bazy wiedzy zostanie wstępnie sprowadzona do odpowiedniej postaci normalnej, to wystarczy wówczas wykorzystywać w systemie reguły wnioskowania pasujące do formuł w takiej postaci i generujące formuły w takiej postaci.

Klauzule

Ustalmy, że dowolną formułę atomową będziemy nazywać literałem pozytywny, a dowolną formułę atomową poprzedzoną operatorem negacji - literałem negatywnym. Formułę, która ma postać alternatywy dowolnej liczby literałów (pozytywnych lub negatywnych), nazwiemy klauzulą. W szczególności, pojedynczy literał także jest klauzulą.

Na szczególną uwagę zasługują klauzule, które zawierają nie więcej niż jeden literał pozytywny. Nazywane są one klauzulami Horna (albo hornowskimi). Nietrudno zauważyć, że klauzula Horna postaci $L_0\vee \mathrm{\neg }{L}_1\vee \dots \vee \mathrm{\neg }{L}_n$,, gdzie $L_0$, jest literałem pozytywnym, a literały $\mathrm{\neg }{L}_1,\dots ,\mathrm{\neg }{L}_n$, są literałami negatywnymi, może być także zapisana w postaci implikacji $L_1\wedge L_2\wedge \dots \wedge L_n\to L_0$,.

Klauzule Horna, zapisane w postaci implikacji, to oczywiście dogodna forma zapisu formuł do stosowania podanej wyżej reguły wnioskowania modus ponens. Do klauzul dowolnej postaci może być stosowana zasada rezolucji. Niestety, nie każdą formułę można przedstawić w postaci klauzuli - najprostszym przykładem formuły, dla której nie jest to możliwe, jest koniunkcja dwóch literałów.

Koniunkcyjna postać normalna

Formułą w koniunkcyjnej postaci normalnej (CNF) nazwiemy koniunkcję dowolnej liczby dowolnych klauzul. W szczególności także pojedyncza klauzula (a więc i pojedynczy literał) jest w koniunkcyjnej postaci normalnej. Użyteczność koniunkcyjnej postaci normalnej polega na tym, że pozwala ona reprezentować formułę jako zbiór klauzul - mając koniunkcję klauzul możemy stosując regułę (48) wyprowadzić każdą wchodzącą w jej skład klauzulę, i do dalszych kroków wnioskowania używać już tylko pojedynczych klauzul.

Każdą formułę nie zawierającą kwantyfikatorów można przedstawić w koniunkcyjnej postaci normalnej. Należy się w tym celu posłużyć odpowiednimi przekształceniami:

$\alpha \leftrightarrow \beta \equiv (\alpha \to \beta )\wedge (\beta \to \alpha )$,	(81)
$\alpha \to \beta \equiv \mathrm{\neg }\alpha \vee \beta$,	(82)
$\mathrm{\neg }(\mathrm{\neg }\alpha )\equiv \alpha$,	(83)
$\mathrm{\neg }(\alpha \vee \beta )\equiv \mathrm{\neg }\alpha \wedge \mathrm{\neg }\beta$,	(84)
$\mathrm{\neg }(\alpha \wedge \beta )\equiv \mathrm{\neg }\alpha \vee \mathrm{\neg }\beta$,	(85)
$\alpha \vee (\beta \wedge \gamma )\equiv (\alpha \vee \beta )\wedge (\alpha \vee \gamma )$,	(86)
$\alpha \wedge (\beta \vee \gamma )\equiv (\alpha \wedge \beta )\vee (\alpha \wedge \gamma )$,	(87)

Formalnie rzecz biorąc, takie przekształcenia można traktować jako szczególne reguły wnioskowania, które z jednej formuły generują jedną inną, i które stosowane byłyby w pierwszej kolejności do sprowadzenia wszystkich formuł z bazy wiedzy do koniunkcyjnej postaci normalnej. Można łatwo sprawdzić, że reguły te, a także reguły do nich odwrotne, są poprawne.

Przykład normalizacji. Prześledzimy kolejne kroki sprowadzania formuły do postaci CNF:

$P(x,y)\vee Q(y,a)\to P(z,b)\wedge \mathrm{\neg }R(v,b)$,	(88)
$\mathrm{\neg }(P(x,y)\vee Q(y,a))\vee (P(z,b)\wedge \mathrm{\neg }R(v,b))$,	(89)
$\mathrm{\neg }(P(x,y)\wedge \mathrm{\neg }Q(y,a))\vee (P(z,b)\wedge \mathrm{\neg }R(v,b))$,	(90)
$(\mathrm{\neg }P(x,y)\vee P(z,b))\wedge (\mathrm{\neg }P(x,y)\vee R(v,b))\wedge$,	(90)
$\wedge (\mathrm{\neg }Q(y,a)\vee P(z,b))\wedge (\mathrm{\neg }Q(y,a)\vee R(v,b))$,	(91)

Postać standardowa Skolema

Postać standardowa Skolema jest rozszerzeniem koniunkcyjnej postaci normalnej na formuły z kwantyfikatorami. Formuła w tej postaci jest złożeniem dwóch części: przedrostka (być może pustego) zawierającego dowolną liczbę kwantyfikatorów ogólnych oraz matrycy, która jest formułą w postaci CNF

$(\mathrm{\forall }\dots )(\mathrm{\forall }\dots )\dots (\mathrm{\forall }\dots )\alpha$, (92)

Przekształcenie formuły do postaci standardowej Skolema, czyli tzw. skolemizacja, wymaga więc najpierw wyprowadzenia "przed nawias" wszystkich kwantyfikatorów, a następnie eliminacji kwantyfikatorów ogólnych. Następnie pozostaje sprowadzenie formuły bez kwantyfikatorów do postaci CNF. Wyprowadzenie kwantyfikatorów "przed nawias" jest możliwe na podstawie następujących przekształceń:

$\mathrm{\neg }(\mathrm{\forall }x)\alpha \equiv (\mathrm{\exists }x)\alpha$,	(93)
$\mathrm{\neg }(\mathrm{\exists }x)\alpha \equiv (\mathrm{\forall }x)\alpha$,	(94)
$(\mathrm{\forall }x)\alpha \mathrm{♢}\beta \equiv (\mathrm{\forall }x)(\alpha \mathrm{♢}\beta )$,	(95)
$(\mathrm{\exists }x)\alpha \mathrm{♢}\beta \equiv (\mathrm{\exists }x)(\alpha \mathrm{♢}\beta )$,	(96)

gdzie $\mathrm{♢}$, moze byc operatorem $\vee$,, $\wedge$,, $\to$,, $\leftrightarrow$,, przy zalożeniu, ze zmienna $x$, nie występuje w formule $\beta$,. Do spełnienia tego założenia można bez trudu zawsze doprowadzić przemianowując w razie potrzeby zmienne. (Niektóre przekształcenia mogą być wykonane także wtedy, gdy $\beta$, zawiera $x$,, lecz nie ma potrzeby rozważania ich tutaj.)

Aby następnie wyeliminować kwantyfikatory szczegółowe, należy postępować zgodnie z następującym schematem.

1. Bierzemy pod uwagę kolejne kwantyfikatory szczegółowe od lewej do prawej.
2. Kwantyfikator szczegółowy, który nie jest poprzedzony żadnym kwantyfikatorem ogólnym, usywamy, zastępując jednocześnie w formule wszystkie wystąpienia zmiennej związanej z tym kwantyfikatorem nowym unikalnym symbolem stałej (tzw. stała Skolema).
3. Kwantyfikator szczegółowy, który jest poprzedzony kwantyfikatorami ogólnymi, z którymi związane są zmienne $x_1,x_2,\dots ,x_m$,, usuwamy, zastępując jednocześnie w formule wszystkie wystąpienia zmiennej związanej z tym kwantyfikatorem nowym unikalnym symbolem funkcyjnym (tzw. funkcja Skolema) zastosowanym do argumentów $x_1,x_2,\dots ,x_m$,.

Przykład skolemizacji. Weźmy pod uwagę formułę:

$(\mathrm{\forall }x)(\mathrm{\exists }y)(P(x,y)\vee Q(y,a))\to (\mathrm{\exists }x)(\mathrm{\forall }y)(P(x,b)\wedge \mathrm{\neg }R(y,b))$, (97)

Rozpoczynamy od przemianowania zmiennych tak, aby z każdym kwantyfikatorem związany był inny symbol zmiennej:

$(\mathrm{\forall }x)(\mathrm{\exists }y)(P(x,y)\vee Q(y,a))\to (\mathrm{\exists }z)(\mathrm{\forall }v)(P(z,b)\wedge \mathrm{\neg }R(v,b))$, (98)

Obecnie wszystkie kwantyfikatory możemy przenieść na początek formuły:

$(\mathrm{\forall }x)(\mathrm{\exists }y)(\mathrm{\exists }z)(\mathrm{\forall }v)(P(x,y)\vee Q(y,a)\to P(z,b)\wedge \mathrm{\neg }R(v,b))$, (99)

Kwantyfikator szczegółowy dotyczący zmiennej $y$, występuje po kwantyfikatorze ogólnym dla zmiennej $x$,. Aby pominąć ten kwantyfikator szczegółowy, wprowadzamy nowy symbol funkcyjny $h_1$, i zastępujemy wszystkie wystąpienia zmiennej $y$, przez $h_1(x)$,. Podobnie postępując z kolejnym kwantyfikatorem szczegółowym, zastępujemy wszystkie wystąpienia zmiennej $z$, przez $h_2(x)$,, gdzie $h_2$, jest kolejnym nowym symbolem funkcyjnym. Formułę, która pozostaje po pominięciu kwantyfikatorów, sprowadzaliśmy do postaci CNF w poprzednim przykładzie. Zatem ostatecznie poszukiwana postać normalna Skolema formuły jest następująca:

Parser nie mógł rozpoznać (nieznana funkcja „\begin{split}”): {\displaystyle \begin{split} & (\forall x)(\forall v) (\neg P(x,h_1(x))\lor P(h_2(x),b)) \land(\neg P(x,h_1(x))\lor R(v,b))\land & \phantom{(\forall x)(\forall y)} \land (\neg Q(h_1(x),a)\lor P(h_2(x),b))\land(\neg Q(h_1(x),a)\lor R(v,b)) \end{split} } , (100)

Baza wiedzy jako zbiór klauzul

W praktycznych zagadnieniach wnioskowania można bezpiecznie założyć, że w zbiorze formuł, który ma stanowić początkową zawartość bazy wiedzy, nie występują zmienne wolne - wszystkie wystąpienia zmiennych są związane z pewnym kwantyfikatorem. Przy tym założeniu, po sprowadzeniu każdej formuły do postaci Skolema, możemy pominąć przedrostki - traktując wszystkie wystąpienia zmiennych jako związane z kwantyfikatorami ogólnymi przez domniemanie. Wówczas każda formuła w postaci CNF może zostać zastąpiona zbiorem wchodzących w jej skład klauzul, a tym samym cała baza wiedzy może być reprezentowana w postaci zbioru klauzul. Jest to reprezentacja bardzo dogodna do powszechnie stosowanych algorytmów wnioskowania w logice predykatów, opartych na zasadzie rezolucji.

Przekształcając zbiór formuł rachunku predykatów do postaci zbioru klauzul, z domniemanymi ogólnymi kwantyfikatorami dla wszystkich zmiennych, może wymagać przemianowania zmiennych w celu zachowania ich rozróżnialności. Konieczność ta wynika z faktu, że przechodząc z postaci CNF do postaci zbioru klauzul tracimy informację, z której pierwotnej formuły pochodzą poszczególne klauzule. Jeśli pewna zmienna $x$, występuje w różnych klauzulach w obrębie tej samej formuły w postaci standardowej Skolema, to po przejściu do reprezentacji w postaci zbioru klauzul powinna ona pozostać tą samą zmienną w obu klaulach. Jeśli jednak ten sam symbol zmiennej występuje w klauzulach należących do dwóch różnych formuł, to przechodząc na reprezentację w postaci zbioru klauzul musimy zmienić jeden z nich. Praktycznie wygodnym rozwiązaniem jest wstępne przemianowanie zmiennych w ten sposób, aby żaden symbol zmiennej nie występował w więcej niż jednej formule, a dokładniej - aby każdy symbol zmiennej związany był jednoznacznie z jednym wystąpieniem kwantyfikatora.