Sztuczna inteligencja/SI Moduł 2/System wnioskowania

System wnioskowania

System wnioskowania to formalny aparat umożliwiający prowadzenie procesu wnioskowania - wyprowadzania nowych formuł z pewnego początkowego zbioru znanych formuł, nazywanego bazą wiedzy. Dla dowolnego języka logiki, a więc także dla języka predykatów, można zaproponować wiele różnych systemów wnioskowania - język nie wyznacza jednoznacznie mechanizmów wnioskowania, jakimi można się posługiwać. Systemy wnioskowania dla języka logiki predykatów obejmują dwa składniki.

• Aksjomaty: formuły, których prawdziwość przyjmowana jest bez dowodu.
• Reguły wnioskowania: wzorce opisujące dozwolone sposoby bezpośredniego wyprowadzania nowych formuł ze znanych formuł.

Aksjomaty

Aksjomaty to formuły, których w systemie wnioskowania używa się wraz z formułami z początkowej bazy wiedzy jako "punktów startowych" wnioskowania, wyprowadzając z nich nowe formuły. Ściśle rzecz biorąc, aksjomaty są nie tyle formułami, co raczej wzorcami formuł, które można konkretyzować odpowiednio do potrzeb. Poniżej podane są przykładowe aksjomaty dla logiki predykatów, przy czym w trakcie wnioskowania $\alpha$, $\beta$ i $\gamma$ można zastąpić dowolnymi formułami innymi symbolami predykatowymi, zaś symbole zmiennych $x$ i $y$ można zastąpić dowolnymi innymi symbolami zmiennych.

$\alpha \vee \mathrm{\neg }\alpha$	(40)
$\alpha \to (\beta \to \alpha )$	(41)
$(\alpha \to (\beta \to \gamma ))\to ((\alpha \to \beta )\to (\alpha \to \gamma ))$	(42)

Reguły wnioskowania

Reguła wnioskowania opisuje możliwą realizację pojedynczego kroku wnioskowania. Zwyczajowo regułę wnioskowania zapisuje się w następującej postaci:

$\frac{{\alpha }_1{\alpha }_2\dots .{\alpha }_n}{\beta }$ (43)

gdzie ${\alpha }_1,{\alpha }_2,\dots ,{\alpha }_n$ oznaczają wzorce formuł wejściowych reguły, a $\beta$ oznacza wzorzec formuły wynikowej. Zastosowanie reguły wnioskowania polega na odnalezieniu w bazie wiedzy (połączonej ze zbiorem aksjomatów) formuł pasujących do wzorców formuł wejściowych i wygenerowaniu odpowiedniej formuły wynikowej. Zamiast precyzyjnie definiować, co oznaczają wzorce formuł, posłużymy się przykładami prostych reguł wnioskowania, których sposób stosowania opiszemy słownie.

$\frac{\alpha \to \beta ,\alpha }{\beta }$ (44)

W powyższej regule, znanej jako reguła modus ponens, wzorce formuł wejściowych pasują do dowolnych dwóch formuł, z których jedna jest implikacją, a druga - poprzednikiem tej implikacji. Reguła mówi, że mając dwie takie formuły możemy wygenerować formułę będącą następnikiem tej implikacji.

$\frac{\alpha \to \beta ,\mathrm{\neg }\beta }{\mathrm{\neg }\alpha }$ (45)

Powyższa reguła, znana pod nazwą modus tollens, może być zastosowana do dowolnych dwóch formuł, z których jedna jest implikacją, a druga - zanegowanym następnikiem tej implikacji. Wówczas reguła generuje formułę będącą zanegowanym poprzednikiem implikacji.

$\frac{\alpha \vee \beta ,\mathrm{\neg }\beta }{\alpha }$ (46)

Powyższa reguła, zbliżona do poprzedniej, pozwala wyprowadzić formułę wynikową będącą jednym członem alternatywy, która została dopasowana jako formuła wejściowa, o ile drugą formułę wejściową dopasowano jako zanegowany drugi człon tej alternatywy.

$\frac{{\alpha }_1,{\alpha }_2,\dots ,{\alpha }_n}{{\alpha }_1\wedge {\alpha }_2\wedge \dots \wedge {\alpha }_n}$ (47)

Do wzorców formuł wejściowych powyższej reguły pasują dowolne dwie lub więcej formuł. Wynikiem zastosowania reguły jest wygenerowanie formuły wynikowej będącej koniunkcją formuł wejściowych.

$\frac{{\alpha }_1\wedge {\alpha }_2,\wedge \dots \wedge {\alpha }_n}{{\alpha }_1,{\alpha }_2,\dots ,{\alpha }_n}$ (48)

Powyższa reguła jest regułą odwrotną do poprzedniej - z koniunkcji generuje zbiór formuł będących członami tej koniunkcji.

$\frac{(\mathrm{\forall }x)\alpha }{\alpha [x/t]}$ (49)

W powyższej regule wzorzec formuły wejściowej pasuje do dowolnej formuły z kwantyfikatorem ogólnym, po którym następuje formuła zawierająca zmienną objętą tym kwantyfikatorem. Dodatkowo założymy, że w formule tej nie występuje żaden inny kwantyfikator dotyczący tej samej zmiennej. Wówczas na mocy podanej reguły można wygenerować formułę wynikową uzyskaną przez pominięcie kwantyfikatora oraz zastąpienie wszystkich wystąpień zmiennej $x$ przez dowolny term $t$, co zostało zapisane jako $\alpha [x/t]$. Możemy tę regułę nazwać regułą specjalizacji.

Dowód

System wnioskowania służy do produkowania dowodów, czyli wyprowadzeń formuł. Formalnie rzecz biorąc, dla ustalonego systemu wnioskowania dowodem formuły $\beta$ ze zbioru formul $\mathrm{\Gamma }$ nazywamy dowolny ciąg formuł ${\alpha }_1,{\alpha }_2,\dots ,{\alpha }_{n-1},{\alpha }_n$ spełniający warunki:

1. ${\alpha }_n=\beta$,
2. dla każdego $i=1,2,\dots .n$ zachodzi jedna z następujących sytuacji:
   1. ${\alpha }_i$ jest aksjomatem,
   2. ${\alpha }_i\in \mathrm{\Gamma }$,
   3. ${\alpha }_i$ jest wynikiem zastosowania pewnej reguły wnioskowania do formuł ${\alpha }_{j_1},\dots ,{\alpha }_{jk}$, gdzie $j_1,\dots ,j_k<n$.

Przykład wnioskowania. Weźmy pod uwagę bazę wiedzy zawierającą następujące formuły:

$(\mathrm{\forall }x)R(x,x)$	(50)
$(\mathrm{\forall }x)(\mathrm{\forall }y)((R(x,y)\to R(y,x))\wedge ((R(y,x)\to R(x,y))))$	(51)
$(\mathrm{\forall }x)(P(x,g(x))\vee R(x,g(x)))$	(52)
$(\mathrm{\forall }x)(P(f(x),x)\vee R(f(x),x))$	(53)
$(\mathrm{\forall }x)(\mathrm{\forall }y)(P(x,y)\to Q(x,y))$	(54)
$(\mathrm{\forall }x)(\mathrm{\forall }y)(Q(x,y)\to Q(f(x),y))$	(55)
$(\mathrm{\forall }x)(\mathrm{\forall }y)(Q(x,y)\to Q(x,g(y)))$	(56)
$\mathrm{\neg }R(a,f(a))$	(57)
$\mathrm{\neg }R(b,f(b))$	(58)
$R(c,f(c))$	(59)
$\mathrm{\neg }R(d,f(d))$	(60)
$R(d,f(e))$	(61)
$R(a,g(a))$	(62)
$\mathrm{\neg }R(b,g(b))$	(63)
$\mathrm{\neg }R(c,g(c))$	(64)
$R(d,g(d))$	(65)
$\mathrm{\neg }R(e,g(e))$	(66)

(Zauważmy, że wszystkie te formuły są spełnione w dziedzinie świata klocków, przy intepretacji i wartościowaniu opisanych w poprzednich przykładach.) Poszukamy dowodu formuły $Q(f(f(a)),a)$.

1. Stosując (dwukrotnie) regułę specjalizacji (49) do formuły (51) z podstawieniem stałej $a$ w miejsce zmiennej $x$ oraz termu $f(a)$ w miejsce zmiennej $y$ dostajemy:

$(R(a,f(a))\to R(f(a),a))\wedge ((R(f(a),a)\to R(a,f(a))))$ (67)

1. Do formuły uzyskanej w poprzednim kroku stosujemy regułę koniunkcji (48), otrzymując w ten sposób dwie formuły:

$R(a,f(a))\to R(f(a),a)$	(68)
$R(f(a),a)\to R(a,f(a))$	(69)

1. Do drugiej z otrzymanych w poprzednim kroku formuł oraz do formuły (57) stosujemy obecnie regułę modus tollens (45), co daje w wyniku:

$\mathrm{\neg }R(f(a),a)$ (70)

1. Stosując regułę specjalizacji (49) do formuły (53) z podstawieniem stałej $a$ w miejsce zmiennej $x$ dostajemy:

$P(f(a),a)\vee R(f(a),a)$ (71)

1. Stosując regułę wnioskowania (46) do formuł uzyskanych w dwóch poprzednich krokach (71) i (70) wyprowadzamy:

$P(f(a),a)$ (72)

1. Stosując regułę specjalizacji (49) do formuły (54) z podstawieniem termu $f(a)$ w miejsce zmiennej $x$ oraz stalej $a$ w miejsce zmiennej $y$ otrzymujemy:

$P(f(a),a)\to Q(f(a),a)$ (73)

1. Przez zastosowanie reguły modus ponens (44) do formuł uzyskanych w dwóch poprzednich krokach dowodu (73) i (72) wyprowadzamy formułę:

$Q(f(a),a)$ (74)

1. Stosując regułę specjalizacji (49) do formuły (55) z podstawieniem termu $f(a)$ w miejsce zmiennej $x$ oraz stalej $a$ w miejsce zmiennej $y$ otrzymujemy:

$Q(f(a),a)\to Q(f(f(a)),a)$ (75)

1. Wreszcie zastosowanie reguły modus ponens (44) do formuł wyprowadzonych w dwóch poprzednich krokach (75) i (74) pozwala wygenerować poszukiwaną formułę docelową $Q(f(f(a)),a)$, która tym samym została udowodniona.

Zauważmy, że udowodniona formuła jest spełniona w świecie klocków. W procesie wnioskowania były stosowane tylko niektóre formuły wchodzące w skład bazy wiedzy. Nietrudno się przekonać, że jej zawartość umożliwia wyprowadzenie wielu innych formuł, także spełnionych w świecie klocków.

Konsekwencja syntaktyczna

Dla danego systemu wnioskowania można zdefiniować relację konsekwencji syntatycznej jako relację wyprowadzalności formuły z pewnej bazy wiedzy za pomocą tego systemu. Powiemy, że formuła $\beta$ jest konsekwencją syntaktyczną zbioru formuł $\mathrm{\Gamma }$, jeśli istnieje dowód formuły $\beta$ ze zbioru formul $\mathrm{\Gamma }$. Będziemy wówczas pisać $\mathrm{\Gamma }⊢\beta$.

Poprawny i pełny system wnioskowania

Można podać dowolnie wiele systemów wnioskowania dla ustalonego języka logiki. Każdy z nich określa pewien mechanizm generowania nowych formuł ze znanych formuł. Nie każdy z nich jednak jest przydatny do rozstrzygania o prawdziwości i fałszywości. Przydatny system wnioskowania powinien być poprawny i pełny.

W uproszczeniu, system wnioskowania jest nazywany poprawnym wtedy, gdy wyprowadzalność formuły w tym systemie pociąga za sobą jej prawdziwość. Z kolei dla systemu pełnego zachowana jest właściwość odwrotna: każda prawdziwa formuła może być w tym systemie wyprowadzona. W obu przypadkach mówimy tu o wyprowadzalności z pustej początkowej bazy wiedzy (wyłącznie z wykorzystaniem aksjomatów systemu wnioskowania).

Bardziej ogólnie i precyzyjnie powinniśmy raczej definiować poprawność i pełność odwołując się do relacji konsenwencji syntaktycznej i semantycznej. Powiemy, że system wnioskowania jest poprawny, gdy dla dowolnego zbioru formuł $\mathrm{\Gamma }$ oraz dowolnej formuly $\alpha$, jeśli $\alpha$ jest konsenwencją syntaktyczna $\mathrm{\Gamma }$, to $\alpha$ jest także konsenwencją semantyczną. Z kolei system wnioskowania nazwiemy pełnym, gdy dla dowolnego zbioru formuł $\mathrm{\Gamma }$ oraz dowolnej formuły $\alpha$, jesli $\alpha$ jest konsenwencją semantyczna $\mathrm{\Gamma }$, to $\alpha$ jest takze konsenwencją syntaktyczna $\mathrm{\Gamma }$.

O pojedynczych elementach systemu wnioskowania - aksjomatach i regułach wnioskowania - także możemy mówić, że są bądź nie są poprawne. Aksjomat jest poprawny, jeśli jest formułą prawdziwą. Reguła wnioskowania postaci

$\frac{{\alpha }_1{\alpha }_2\dots .{\alpha }_n}{\beta }$ (76)

jest poprawna, jeśli dla każdej możliwej konkretyzacji wzorców formuł wejściowych formuła postaci ${\alpha }_1\wedge {\alpha }_2\wedge \dots \wedge {\alpha }_n\to \beta$ jest prawdziwa. Jeśli wszystkie aksjomaty i reguły wnioskowania wchodzące w skład systemu wnioskowania są poprawne, to system wnioskowania jest poprawny. Wszystkie podane wyżej aksjomaty i reguły wnioskowania są poprawne.