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 Parser nie mógł rozpoznać (błąd składni): {\displaystyle \alpha\rightarrow\beta \} , i Parser nie mógł rozpoznać (błąd składni): {\displaystyle \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 Parser nie mógł rozpoznać (błąd składni): {\displaystyle t \} , zmiennej Parser nie mógł rozpoznać (błąd składni): {\displaystyle x \} , zapisywac Parser nie mógł rozpoznać (błąd składni): {\displaystyle x/t \} ,. Podstawienie Parser nie mógł rozpoznać (błąd składni): {\displaystyle \{x/t_1,y/t_2,z/t_3\} \} , zawiera trzy wiązania, przypisujące zmiennym Parser nie mógł rozpoznać (błąd składni): {\displaystyle x,y,z \} , odpowiednio termy Parser nie mógł rozpoznać (błąd składni): {\displaystyle t_1,t_2,t_3 \} ,. Wynikiem zastosowania podstawienia Parser nie mógł rozpoznać (błąd składni): {\displaystyle \sigma \} , do formuly Parser nie mógł rozpoznać (błąd składni): {\displaystyle \alpha \} , jest formuła Parser nie mógł rozpoznać (błąd składni): {\displaystyle \alpha[\sigma] \} ,, w której wszystkie wystąpienia zmiennych objętych podstawieniem Parser nie mógł rozpoznać (błąd składni): {\displaystyle \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łę Parser nie mógł rozpoznać (błąd składni): {\displaystyle \alpha \} , następującej postaci:

Parser nie mógł rozpoznać (błąd składni): {\displaystyle P(x,y) \rightarrow Q(x,b)\lor R(a,y) \} , (77)

oraz podstawienie Parser nie mógł rozpoznać (błąd składni): {\displaystyle \sigma=\{x/a,y/f(b)\} \} ,. Wynikiem zastosowania podstawienia Parser nie mógł rozpoznać (błąd składni): {\displaystyle \sigma \} , do formuly Parser nie mógł rozpoznać (błąd składni): {\displaystyle \alpha \} , jest formuła Parser nie mógł rozpoznać (błąd składni): {\displaystyle \alpha[\sigma] \} , następującej postaci:

Parser nie mógł rozpoznać (błąd składni): {\displaystyle P(a,f(b))\rightarrow Q(a,b)\lor 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ł Parser nie mógł rozpoznać (błąd składni): {\displaystyle \alpha \} , i Parser nie mógł rozpoznać (błąd składni): {\displaystyle \beta \} , unifikatorem nazwiemy dowolne podstawienie Parser nie mógł rozpoznać (błąd składni): {\displaystyle \sigma \} , takie, że formuły Parser nie mógł rozpoznać (błąd składni): {\displaystyle \alpha[\sigma] \} , i Parser nie mógł rozpoznać (błąd składni): {\displaystyle \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ł:

Parser nie mógł rozpoznać (błąd składni): {\displaystyle P(x,f(y)) \land \neg Q(y,b) \rightarrow R(g(a),z)\lor P(f(x),c) \} ,	(79)
Parser nie mógł rozpoznać (błąd składni): {\displaystyle P(b,v) \land \neg Q(d,b) \rightarrow R(w,g(c))\lor P(f(b),c) \} ,	(80)

najbardziej ogólnym unifikatorem jest podstawienie Parser nie mógł rozpoznać (błąd składni): {\displaystyle \{x/b, y/d, z/g(c), v/f(d), w/g(a)\} \} ,.