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 Parser nie mógł rozpoznać (błąd składni): {\displaystyle L_0\lor \neg L_1\lor\dots\lor \neg L_n \} ,, gdzie Parser nie mógł rozpoznać (błąd składni): {\displaystyle L_0 \} , jest literałem pozytywnym, a literały Parser nie mógł rozpoznać (błąd składni): {\displaystyle \neg L_1,\dots,\neg L_n \} , są literałami negatywnymi, może być także zapisana w postaci implikacji Parser nie mógł rozpoznać (błąd składni): {\displaystyle L_1\land L_2\land\dots\land L_n\rightarrow 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:
Parser nie mógł rozpoznać (błąd składni): {\displaystyle \alpha\leftrightarrow\beta \;\;\; \equiv\;\;\; (\alpha\rightarrow\beta)\land(\beta\rightarrow\alpha) \} , (81) Parser nie mógł rozpoznać (błąd składni): {\displaystyle \alpha\rightarrow\beta \;\;\; \equiv\;\;\; \neg\alpha\lor\beta \} , (82) Parser nie mógł rozpoznać (błąd składni): {\displaystyle \neg(\neg\alpha) \;\;\; \equiv\;\;\; \alpha \} , (83) Parser nie mógł rozpoznać (błąd składni): {\displaystyle \neg(\alpha\lor\beta) \;\;\; \equiv\;\;\; \neg\alpha\land\neg\beta \} , (84) Parser nie mógł rozpoznać (błąd składni): {\displaystyle \neg(\alpha\land\beta) \;\;\; \equiv\;\;\; \neg\alpha\lor\neg\beta \} , (85) Parser nie mógł rozpoznać (błąd składni): {\displaystyle \alpha\lor(\beta\land\gamma) \;\;\; \equiv\;\;\; (\alpha\lor\beta)\land(\alpha\lor\gamma) \} , (86) Parser nie mógł rozpoznać (błąd składni): {\displaystyle \alpha\land(\beta\lor\gamma) \;\;\; \equiv\;\;\; (\alpha\land\beta)\lor(\alpha\land\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:
Parser nie mógł rozpoznać (błąd składni): {\displaystyle P(x,y)\lor Q(y,a)\rightarrow P(z,b)\land \neg R(v,b) \} , (88) Parser nie mógł rozpoznać (błąd składni): {\displaystyle \neg(P(x,y)\lor Q(y,a)) \lor (P(z,b)\land \neg R(v,b)) \} , (89) Parser nie mógł rozpoznać (błąd składni): {\displaystyle \neg(P(x,y)\land\neg Q(y,a)) \lor (P(z,b)\land \neg R(v,b)) \} , (90) Parser nie mógł rozpoznać (błąd składni): {\displaystyle (\neg P(x,y)\lor P(z,b))\land(\neg P(x,y)\lor R(v,b))\land \} , (90) Parser nie mógł rozpoznać (błąd składni): {\displaystyle \;\;\;\;\;\land (\neg Q(y,a)\lor P(z,b))\land(\neg Q(y,a)\lor 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
- Parser nie mógł rozpoznać (błąd składni): {\displaystyle (\forall\dots)(\forall\dots)\dots(\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ń:
Parser nie mógł rozpoznać (błąd składni): {\displaystyle \neg (\forall x)\alpha \;\;\; \equiv\;\;\; (\exists x)\alpha \} , (93) Parser nie mógł rozpoznać (błąd składni): {\displaystyle \neg (\exists x)\alpha \;\;\; \equiv\;\;\; (\forall x)\alpha \} , (94) Parser nie mógł rozpoznać (błąd składni): {\displaystyle (\forall x)\alpha\diamondsuit\beta \;\;\; \equiv\;\;\; (\forall x)(\alpha\diamondsuit\beta) \} , (95) Parser nie mógł rozpoznać (błąd składni): {\displaystyle (\exists x)\alpha\diamondsuit\beta \;\;\; \equiv\;\;\; (\exists x)(\alpha\diamondsuit\beta) \} , (96)
gdzie Parser nie mógł rozpoznać (błąd składni): {\displaystyle \diamondsuit \} , moze byc operatorem Parser nie mógł rozpoznać (błąd składni): {\displaystyle \lor \} ,, Parser nie mógł rozpoznać (błąd składni): {\displaystyle \land \} ,, Parser nie mógł rozpoznać (błąd składni): {\displaystyle \rightarrow \} ,, Parser nie mógł rozpoznać (błąd składni): {\displaystyle \leftrightarrow \} ,, przy zalożeniu, ze zmienna Parser nie mógł rozpoznać (błąd składni): {\displaystyle x \} , nie występuje w formule Parser nie mógł rozpoznać (błąd składni): {\displaystyle \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 Parser nie mógł rozpoznać (błąd składni): {\displaystyle \beta \} , zawiera Parser nie mógł rozpoznać (błąd składni): {\displaystyle 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.
- Bierzemy pod uwagę kolejne kwantyfikatory szczegółowe od lewej do prawej.
- 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).
- Kwantyfikator szczegółowy, który jest poprzedzony kwantyfikatorami ogólnymi, z którymi związane są zmienne Parser nie mógł rozpoznać (błąd składni): {\displaystyle 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 Parser nie mógł rozpoznać (błąd składni): {\displaystyle x_1,x_2,\dots,x_m \} ,.
Przykład skolemizacji. Weźmy pod uwagę formułę:
- Parser nie mógł rozpoznać (błąd składni): {\displaystyle (\forall x)(\exists y)(P(x,y)\lor Q(y,a))\rightarrow (\exists x)(\forall y)(P(x,b)\land\neg R(y,b)) \} , (97)
Rozpoczynamy od przemianowania zmiennych tak, aby z każdym kwantyfikatorem związany był inny symbol zmiennej:
- Parser nie mógł rozpoznać (błąd składni): {\displaystyle (\forall x)(\exists y)(P(x,y)\lor Q(y,a))\rightarrow (\exists z)(\forall v)(P(z,b)\land\neg R(v,b)) \} , (98)
Obecnie wszystkie kwantyfikatory możemy przenieść na początek formuły:
- Parser nie mógł rozpoznać (błąd składni): {\displaystyle (\forall x)(\exists y)(\exists z)(\forall v) (P(x,y)\lor Q(y,a)\rightarrow P(z,b)\land\neg R(v,b)) \} , (99)
Kwantyfikator szczegółowy dotyczący zmiennej Parser nie mógł rozpoznać (błąd składni): {\displaystyle y \} , występuje po kwantyfikatorze ogólnym dla zmiennej Parser nie mógł rozpoznać (błąd składni): {\displaystyle x \} ,. Aby pominąć ten kwantyfikator szczegółowy, wprowadzamy nowy symbol funkcyjny Parser nie mógł rozpoznać (błąd składni): {\displaystyle h_1 \} , i zastępujemy wszystkie wystąpienia zmiennej Parser nie mógł rozpoznać (błąd składni): {\displaystyle y \} , przez Parser nie mógł rozpoznać (błąd składni): {\displaystyle h_1(x) \} ,. Podobnie postępując z kolejnym kwantyfikatorem szczegółowym, zastępujemy wszystkie wystąpienia zmiennej Parser nie mógł rozpoznać (błąd składni): {\displaystyle z \} , przez Parser nie mógł rozpoznać (błąd składni): {\displaystyle h_2(x) \} ,, gdzie Parser nie mógł rozpoznać (błąd składni): {\displaystyle 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 Parser nie mógł rozpoznać (błąd składni): {\displaystyle 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.
