Sztuczna inteligencja/SI Moduł 2/Podstawienia i unifikacja

Podstawienia i unifikacja

Dopasowywanie formuł do reguł wnioskowania nie zawsze jest tak proste, jak sugerować by to mogły przedstawione wyżej przykłady. Często wzorce formuł wejściowych reguły wnioskowania wymagają do dopasowania dwóch formuł, które zawierają wspólny fragment (lub jedna jest fragmentem drugiej). Tak jest w szczególności w przypadku reguły \emph{modus ponens}, dla której wymagamy na wejściu formuł postaci $\alpha \to \beta$, i $\alpha$,. Tak zapisane wzorce nie służą jednak wyrażeniu ostrego wymagania, że poprzednik implikacji będącej pierwszą formułą wejściowa i druga formuła wejściowa są identyczne (jako napisy w języku logiki), lecz znacznie łagodniejszego wymagania, że są one unifikowalne, czyli mogą zostać sprowadzone do postaci identycznej przez zastosowanie odpowiednich podstawień dla zmiennych, czyli przypisanie im pewnych termów. To właśnie obecność symboli zmiennych powoduje, że nie możemy poprzestać na prostym wymaganiu identyczności.

Zanim dokładniej zajmiemy się podstawieniami i unifikacją, zwróćmy uwagę, że dopuszczając podstawianie pewnych wartości za zmienne w celu ujednolicenia dwóch formuł możemy w istocie mieć do czynienia z dwoma różnymi przypadkami:

• ujednolicanie zmiennych: jeśli dwie formuły różnią się tym, że w odpowiednich miejscach występują w nich konsekwentnie inne symbole zmiennych, to podstawienie ujednolicające te symbole jest trywialnym zabiegiem zmieniającym wyłącznie zapis formuł,
• uszczegółowienie: jeśli dwie formuły różnią się tym, że w miejscach gdzie w jednej z nich występuje pewien symbol zmiennej (związany kwantyfikatorem ogólnym), w drugiej konsekwentnie występuje pewien term nie będący zmienną (stała albo zastosowanie symbolu funkcyjnego), to w istocie dokonując podstawienia takiego termu za zmienną korzystamy z reguły wnioskowania, na mocy której taki symbol zmienne możemy zastąpić dowolnym termem.

Podstawienia

Przed podstawienie w ogólnym przypadku rozumiemy zbiór wiązań zmiennych, z których każde określa term podstawiany za jedną zmienną. Wiązanie przypisujące term $t$, zmiennej $x$, zapisywac $x/t$,. Podstawienie $\{x/t_1,y/t_2,z/t_3\}$, zawiera trzy wiązania, przypisujące zmiennym $x,y,z$, odpowiednio termy $t_1,t_2,t_3$,. Wynikiem zastosowania podstawienia $\sigma$, do formuly $\alpha$, jest formuła $\alpha [\sigma ]$,, w której wszystkie wystąpienia zmiennych objętych podstawieniem $\sigma$, zostały zastąpione odpowiednimi termami. Podstawienie może zawierać wiązania tylko dla niektórych zmiennych występujących w formule, a także zawierać wiązania dla innych zmiennych, nie występujących w formule.

Przykład podstawienia. Weźmy pod uwagę formułę $\alpha$, następującej postaci:

$P(x,y)\to Q(x,b)\vee R(a,y)$, (77)

oraz podstawienie $\sigma =\{x/a,y/f(b)\}$,. Wynikiem zastosowania podstawienia $\sigma$, do formuly $\alpha$, jest formuła $\alpha [\sigma ]$, następującej postaci:

$P(a,f(b))\to Q(a,b)\vee R(a,f(b))$, (78)

Unifikacja

Unifikacja to doprowadzenie dwóch (lub w ogólnym wypadku większej liczby) formuł do identycznej postaci przez zastosowanie do nich jednego wspólnego podstawienia. Dla dwóch formuł $\alpha$, i $\beta$, unifikatorem nazwiemy dowolne podstawienie $\sigma$, takie, że formuły $\alpha [\sigma ]$, i $\beta [\sigma ]$, są identyczne. Jeśli dla pary formuł istnieje wiele unifikatorów, przy wnioskowaniu interesować nas będzie najbardziej ogólny unifikator, czyli podstawienie zawierające wiązania dla możliwie najmniejszej liczby zmiennych.

Nie będziemy zajmować się szczegółowo algorytmami unifikacji. Po ustaleniu, że struktura unifikowanych formuł jest identyczna z dokładnością do termów będących argumentami symboli predykatowych, podejmowana jest próba ujednolicenia. Odbywa się to przez porównywanie unifikowanych formuł w celu znalezienia par różniących się termów (czyli określenia tzw. zbioru niezgodności), a następnie dobieranie podstawienia, które usuwa niezgodności.

Przykład unifikacji. Łatwo sprawdzić, że dla następujących dwóch formuł:

$P(x,f(y))\wedge \mathrm{\neg }Q(y,b)\to R(g(a),z)\vee P(f(x),c)$,	(79)
$P(b,v)\wedge \mathrm{\neg }Q(d,b)\to R(w,g(c))\vee P(f(b),c)$,	(80)

najbardziej ogólnym unifikatorem jest podstawienie $\{x/b,y/d,z/g(c),v/f(d),w/g(a)\}$,.