Sztuczna inteligencja/SI Moduł 2 - Od logiki do wnioskowania

Zadanie wnioskowania

Wnioskowanie formalne, czyli możliwe do zautomatyzowania, przetwarza wiedzę zapisaną w odpowiednim języku logiki. Język ten określa sposób zapisywania i interpretacji reprezentujących wiedzę formuł. Wówczas wnioskowanie można traktować jako przetwarzanie formuł, które z pewnego zbioru znanych formuł (bazy wiedzy) wyprowadza nowe formuły. Wyprowadzanie formuł odbywa się zgodnie z regułami wnioskowania, które określają, jak z formuł określonej postaci uzyskać nową formułę, która jest ich logiczną konsekwencją.

Będziemy się koncentrować na najczęściej spotykanym wariancie zadania wnioskowania, w której celem jest wykazanie prawdziwości pewnej formuły docelowej na podstawie danego zestawu znanych (uznawanych za prawdziwe) formuł. Cel ten jest osiągany przez znalezienie dowodu, czyli ciągu formuł, z których każda kolejna albo pochodzi z początkowej bazy wiedzy, albo jest wynikiem zastosowania pewnej reguły wnioskowania do formuł wcześniejszych. Ostatnią formułą w takim ciągu musi być formuła docelowa. Ze względów praktycznych od systemów wnioskujących oczekuje się także uzasadnienia poprawności dowodu, czyli wskazania zastosowanych do jego skonstruowania reguł wnioskowania.

Składnia języka logiki

Obecnie przystąpimy do zdefiniowania składni języka logiki predykatów, w którym będą zapisywane formuły przetwarzane w procesie wnioskowania, Składnia określa reguły budowania poprawnych formuł, czyli takich, które mogą być przetwarzane przez system wnioskujący. Definiując składnię nie będziemy się zajmować znaczeniem poszczególnych symboli i konstrukcji języka, choć oczywiście znaczenie części z nich będzie dla nas oczywiste ze względu na powszechne doświadczenie z używaniem notacji logicznej np. do zapisu twierdzeń matematycznych.

Alfabet

Alfabet, czyli zbiór symboli języka logiki predykatów, obejmuje poniższe kategorie symboli. Dla każdej z nich podano oznaczenia, jakie będą dalej stosowane.

Symbole stałych: oznaczane za pomocą liter $a,b,c\dots \,$.

Symbole zmiennych: oznaczane za pomocą liter $x,y,z\dots \,$.

Symbole funkcyjne: oznaczane za pomocą liter $f,g,h\dots \,$; każdy symbol funkcyjny ma ustaloną liczbę argumentów.

Symbole predykatowe: oznaczane za pomocą liter $P,Q,R,\dots \,$; każdy symbol predykatowy ma ustaloną liczbę argumentów.

Operatory logiczne: $\neg \,$ (negacja), $\land \,$ (koniunkcja), $\lor \,$ (alternatywa), $\rightarrow \,$ (implikacja), $\leftrightarrow \,$ (równoważność).

Kwantyfikatory: kwantyfikator ogólny $\forall \,$, kwantyfikator szczegółowy $\exists \,$.

Nawiasy: $(\,$, $)\,$, w razie potrzeby także inne.

Będziemy czasem skrótowo mówić o symbolach stałych jako o stałych, o symbolach zmiennych jako o zmiennych, o symbolach funkcyjnych jako o funkcjach, o symbolach predykatowych jako o predykatach, trzeba jednak pamiętać, że - jak długo nie określimy ich znaczenia - są to wyłącznie symbole, czyli pewne napisy, z których konstruowane są bardziej złożone napisy (formuły) według opisanych dalej reguł.

Termy

Jak zobaczymy, formuły konstruowane są z symboli predykatowych stosowanych do argumentów. Poprawnej postaci argumenty dla symboli predykatowych nazywane są termami. Każda stała i zmienna jest termem. Ponadto, jeśli $f\,$ jest dowolnym $m\,$-argumentowym symbolem funkcyjnym, a $t_{1},t_{2},\dots ,t_{m}\,$ są dowolnymi termami, to także $f(t_{1},t_{2},\dots ,t_{m})\,$ jest termem. Jak widać, stosując dowolny symbol funkcyjny do argumentów będących termami uzyskujemy term.

Formuły atomowe

Jeśli $P\,$ oznacza dowolny $m\,$-argumentowy symbol predykatowy, a $t_{1},t_{2},\dots ,t_{m}\,$ są dowolnymi termami, to $P(t_{1},t_{2},\dots ,t_{m})\,$ jest formułą atomową. Formułą atomową jest więc dowolne zastosowanie symbolu predykatowego do argumentów będących termami.

Formuły złożone

Formuły złożone są konstruowane z formuł atomowych przez zastosowanie operatorów logicznych, kwantyfikatorów i nawiasów, zgodnie z określonymi poniżej zasadami.

• Jeśli $\alpha \,$ jest formułą, to $(\alpha )\,$ jest formułą.
• Jeśli $\alpha \,$ jest formułą, to $\neg \alpha \,$ jest formułą.
• Jeśli $\alpha \,$ i $\beta \,$ są formułami, to:
  • $\alpha \land \beta \,$ jest formułą,
  • $\alpha \lor \beta \,$ jest formułą,
  • $\alpha \rightarrow \beta \,$ jest formułą,
  • $\alpha \leftrightarrow \beta \,$ jest formułą.
• Jeśli $\alpha \,$ jest formułą i $x\,$ jest symbolem zmiennej, to
  • $(\forall x)\alpha \,$ jest formułą,
  • $(\exists x)\alpha \,$ jest formułą.

Semantyka języka logiki

Semantyka języka logiki określa sposób, w jaki formułom zapisanym zgodnie z podanymi wyżej regułami składni, można przypisać znaczenie, które z kolei pozwala określić ich wartość logiczną. Aby stało się to możliwe, musi oczywiście zostać określone znaczenie wszystkich symboli wchodzących w skład alfabetu języka logiki, a następnie zasady, zgodnie z którymi określa się znaczenie formuł na podstawie znaczenia symboli w nich występujących. Nie będziemy tu prezentować semantyki języka logiki w sposób w pełni formalny i systematyczny, poprzestając tylko na zwięzłym nieformalnym szkicu.

Dziedzina

Aby interpretować formuły języka predykatów musimy (w ogólnym przypadku) przyjąć pewną ustaloną dziedzinę, do której te formuły się odnoszą. Dziedzina jest zbiorem obiektów (np. przedmiotów, ludzi, sytuacji, zdarzeń itp.), na temat właściwości których lub relacji między którymi wiedzę zamierzamy zapisywać w języku logiki.

Przykład: świat klocków. Będziemy ilustrować definicję semantyki języka logiki posługując się prostym przykładem świata klocków, zilustrowanym na rysunku. Dziedzina jest w tym przypadku zbiorem pięciu klocków $\{A,B,C,D,E\}\,$.

Interpretacja symboli

Mając ustaloną pewną dziedzinę $X\,$, symbole alfabetu języka predykatów interpretujemy następująco.

Symbole stałych: symbol stałej $a\,$ oznacza pewien obiekt z dziedziny $I(a)\in X\,$.

Symbole funkcyjne: $m\,$-argumentowy symbol funkcyjny $f\,$ oznacza $m\,$-argumentową funkcję $I(f):X^{m}\mapsto X\,$.

Symbole predykatowe: $m\,$-argumentowy symbol predykatowy $P\,$ oznacza $m\,$-argumentową relację $I(P)\subset X^{m}\,$ (równoważnie, możemy przyjąć, że $P\,$ oznacza funkcję $I(P):X^{m}\mapsto \{0,1\}\,$).

Przypomnijmy sobie, że relacją $m\,$ argumentową określoną na zbiorze $X\,$ jest dowolny podzbiór iloczynu kartezjańskiego $X^{m}\,$. Jeżeli krotka złożona z $m\,$ elementów zbioru $X\,$ należy do relacji to mówimy że relacja jest spełniona.

Operatory logiczne, kwantyfikatory i nawiasy służą do budowania formuł złożonych z formuł atomowych i nie mają samodzielnej interpretacji. Symbole zmiennych są interpretowane - w przeciwnym przypadku byłyby identyczne z symbolami stałych. Dopuszcza się jednak przypisywanie zmiennym znaczenia przy interpretowaniu konkretnej formuły za pomocą wartościowania. Wartościowanie jest dowolnym odwzorowaniem symboli zmiennych na elementy dziedziny - dla symbolu zmiennej $x\,$ wartościowanie $v\,$ określa wartość $v(x)\in X\,$.

Przykład: świat klocków. Rozważmy język logiki predykatów, którego alfabet zawiera symbole stałych $\{a,b,c,d,e\}\,$. Możemy przyjąć interpretację, w której każdemu symbolowi stałej odpowiada inny klocek z dziedziny, np.:

$I(a)=\,$	$A\,$	(1)
$I(b)=\,$	$B\,$	(2)
$I(c)=\,$	$C\,$	(3)
$I(d)=\,$	$D\,$	(4)
$I(e)=\,$	$E\,$	(5)

Przyjmiemy także, że w alfabecie znajdują się dwa symbole zmiennych $x\,$ i $y\,$, dla których określono wartościowanie następująco:

$v(x)=\,$	$C\,$	(6)
$v(y)=\,$	$B\,$	(7)

Załóżmy dalej, że alfabet zawiera dwa jednoargumentowe symbole funkcyjne $f\,$ i $g\,$. Nasza interpretacja będzie im przypisywać odpowiednio dwuargumentowe funkcje określone na dziedzinie:

$I(f)=\,$	${\textit {gora}}\,$	(8)
$I(g)=\,$	${\textit {dol}}\,$	(9)

Funkcje te określimy następująco:

${\textit {gora}}(A)=B$	${\textit {dol}}(A)=A\,$	(10)
${\textit {gora}}(B)=C$	${\textit {dol}}(B)=A\,$	(11)
${\textit {gora}}(C)=C$	${\textit {dol}}(C)=B\,$	(12)
${\textit {gora}}(D)=E$	${\textit {dol}}(D)=D\,$	(13)
${\textit {gora}}(E)=E$	${\textit {dol}}(E)=D\,$	(14)

(jak widać, funkcja ${\textit {gora}}\,$ przypisuje każdemu klockowi jego sąsiada z góry, o ile istnieje, albo jego samego; podobnie funkcja ${\textit {dol}}\,$ przypisuje każdemu klockowi jego sąsiada z dołu, o ile istnieje, albo jego samego). Założymy także, że alfabet naszego języka logiki zawiera dwuargumentowe symbole predykatowe $P\,$, $Q\,$ i $R\,$, których interpretację ustalimy następująco:

$I(P)=\,$	${\textit {na}}\,$	(15)
$I(Q)=\,$	${\textit {nad}}\,$	(16)
$I(R)=\,$	${\textit {rowne}}\,$	(17)

przy czym:

• ${\textit {na}}\,$ jest relacją dwuargumentową, do której należą wszystkie pary klocków takie, że pierwszy leży na drugim: $\langle B,A\rangle \,$, $\langle C,B\rangle \,$, $\langle E,D\rangle \,$,
• ${\textit {nad}}\,$ jest relacją dwuargumentową, do której należą wszystkie pary klocków takie, że pierwszy leży nad drugim (tj. na nim lub wyżej): $\langle B,A\rangle \,$, $\langle C,A\rangle \,$, $\langle C,B\rangle \,$, $\langle E,D\rangle \,$,
• ${\textit {rowne}}\,$ jest relacją dwuargumentową, do której należą wszystkie pary złożone z dwóch wystąpień tych samych klocków: $\langle A,A\rangle \,$, $\langle B,B\rangle \,$, $\langle C,C\rangle \,$, $\langle D,D\rangle \,$, $\langle E,E\rangle \,$.

Interpretacja termów

Interpretacja wraz z wartościowaniem pozwala ustalić znaczenie dowolnego termu. Dla interpretacji $I\,$ i wartościowania $v\,$ oznaczmy dla wygody przez $I_{v}\,$ ich połączenie, rozumiane następująco:

dla symboli stałych: $I_{v}(a)=I(a)\,$,

dla symboli zmiennych: $I_{v}(x)=v(x)\,$.

Termy złożone interpretowane są przez zastosowanie interpretacji do wchodzących w ich skład symboli stałych i symboli funkcyjnych oraz zastosowanie wartościowania do wchodzących w ich skład zmiennych. Przy ustalonej dziedzinie, interpretacji $I\,$ i wartościowaniu $v\,$, może być wyznaczone znaczenie każdego termu postaci $f(t_{1},t_{2},\dots ,t_{m})\,$ w następujący sposób:

$I_{v}(f(t_{1},t_{2},\dots ,t_{m}))=I(f)(I_{v}(t_{1}),I_{v}(t_{2}),\dots ,I_{v}(t_{m})).\,$

(18)

Przykład: ślad klocków. Weźmy pod uwagę term $f(b)\,$. Ponieważ $I(b)=B\,$, $I(f)={\textit {gora}}\,$ oraz ${\textit {gora}}(B)=C\,$, więc oczywiście $I(f(b))=C\,$. Podobnie łatwo można sprawdzić interpretację następujących termów:

$I_{v}(f(x))=\,$	$C\,$	(19)
$I_{v}(g(y))=\,$	$A\,$	(20)

Interpretacja formuł

Formuły atomowe interpretowane są podobnie jak termy złożone: przez zastosowanie interpretacji i wartościowania do każdego występującego w nich symbolu. Dla formuły postaci $P(t_{1},t_{2},\dots ,t_{m})\,$ otrzymujemy w ten sposób relację $I(P)\,$ oraz krotkę $m\,$ obiektów z dziedziny $\langle I_{v}(t_{1}),I_{v}(t_{2}),\dots ,I_{v}(t_{m})\rangle \in X^{m}\,$. Znaczeniem formuły będzie jej wartość logiczna określona na podstawie tego, czy krotka obiektów należy do relacji:

Parser nie mógł rozpoznać (nieznana funkcja „\begin{cases}”): {\displaystyle I_v(P(t_1,t_2,\dots,t_m)) = \begin{cases} 1 & \textit{jeśli\ } \langle I_v(t_1),I_v(t_2),\dots,I_v(t_m)\rangle\in I(P)\\ 0 & \textit{jeśli\ } \langle I_v(t_1),I_v(t_2),\dots,I_v(t_m)\rangle\not\in I(P)\textit{.} \end{cases} \,}

(21)

Interpretacja formuł złożonych polega na przypisaniu wartości logicznej formułom uzyskanym przez zastosowanie operatorów logicznych, kwantyfikatorów i nawiasów, na podstawie wartości logicznej wchodzących w ich skład formuł atomowych. Skrupulatne definiowanie wszystkich przypadków operatorów logicznych byłoby żmudne i mało pouczające, więc ograniczymy się do przykładu dla operatora implikacji $\rightarrow \,$:

$I_{v}(\alpha )\,$	$I_{v}(\beta )\,$	$I_{v}(\alpha \rightarrow \beta )\,$
$0$	$0$	$1$
$0$	$1$	$1$
$1$	$0$	$0$
$1$	$1$	$1$

Jak widać, definicja „znaczenia implikacji” sprowadza się do podania tzw. tabeli prawdy.

Na uważniejsze potraktowanie zasługuje kwestia znaczenia formuł zbudowanych z wykorzystaniem kwantyfikatorów. Przyjmując dziedzinę $X\,$, interpretację $I\,$ i wartościowanie $v\,$, rozważmy interpretację formuły postaci $(\forall x)\alpha \,$. Aby uniknąć wikłania się w dyskusje o zasięgu kwantyfikatorów założymy, że w formule $\alpha \,$ nie występuje żaden inny kwantyfikator dla zmiennej $x\,$ (czyli że wszystkie wystąpienia zmiennej $x\,$ w formule $\alpha \,$ są wolne). Wartość logiczną formuły $(\forall x)\alpha \,$ przy interpretacji $I\,$ i wartościowaniu $v\,$ ustalamy w następujący sposób:

1. $I_{v}((\forall x)\alpha )=1\,$ wtedy i tylko wtedy gdy dla wszystkich wartościowań $v_{x}\,$ różniących się od $v\,$ co najwyżej wartością przypisywaną zmiennej $x\,$ (a więc także dla $v_{x}\,$ identycznego z $v\,$) uzyskujemy $I_{v_{x}}(\alpha )=1\,$,
2. $I_{v}((\forall x)\alpha )=0\,$ w przeciwnym przypadku.

Analogicznie dla formuły $(\exists x)\alpha \,$:

1. $I_{v}((\exists x)\alpha )=1\,$ wtedy i tylko wtedy gdy istnieje wartościowanie $v_{x}\,$ różniące się od $v\,$ co najwyżej wartością przypisywaną zmiennej $x\,$ (może to być w szczególności $v_{x}\,$ identyczne z $v\,$) uzyskujemy $I_{v_{x}}(\alpha )=1\,$,
2. $I_{v}((\exists x)\alpha )=0\,$ w przeciwnym przypadku.

Istotą przytoczonych definicji znaczenia formuł z kwantyfikatorem jest wyłączenie zmiennej objętej kwantyfikatorem z wartościowania. Dla określenia wartości logicznej takiej formuły jest obojętne, jaką wartość $v(x)\,$ wartościowanie $v\,$ przypisuje zmiennej $x\,$ objętej kwantyfikatorem. Ważne jest tylko, aby przy niezmienionych wartościach przypisywanych wszystkim pozostałym zmiennym można było stwierdzić, że $I_{v}(\alpha )=1\,$ dla wszystkich możliwych wartości zmiennej $x\,$ (w przypadku kwantyfikatora ogólnego) albo dla przynajmniej jednej wartości zmiennej $x\,$ (w przypadku kwantyfikatora szczegółowego) z dziedziny $X\,$.

Przykład: świat klocków. Weźmy pod uwagę formułę $P(x,y)\rightarrow Q(x,y)\,$. Przy ustalonej w poprzednich przykładach interpretacji i wartościowaniu dostajemy:

$I_{v}(P(x,y))=\,$	$1\,$	(22)
$I_{v}(Q(x,y))=\,$	$1\,$	(23)

a więc $I_{v}(P(x,y)\rightarrow Q(x,y))=1\,$. Nietrudno się przekonać, że także dla formuły $(\forall x)(\forall y)(P(x,y)\rightarrow Q(x,y))\,$ uzyskamy wartość logiczną $1\,$, sprawdzając, że $I_{v}(P(x,y)\rightarrow Q(x,y))\,$ niezależnie od wartości przypisanych zmiennym $x\,$ i $y\,$.

Mając określoną składnię i semantykę języka logiki, możemy zapisywać w nim stwierdzenia na temat dziedziny wyrażone w języku naturalnym:

• Jeśli jakiś klocek leży na innym klocku, to jest jego górnym sąsiadem:

$(\forall x)(\forall y)P(x,y)\rightarrow R(x,f(y))\,$

(24)

• Dla dowolnych dwóch klocków nie jest możliwe, żeby pierwszy z: nich leżał nad drugim i jednocześnie drugi nad pierwszym.

$(\forall x)(\forall y)\neg (P(x,y)\land P(y,x))\,$

(25)

• Każdy klocek, który nie ma górnego sąsiada, jest dolnym sąsiadem: jakiegoś innego klocka.

$(\forall x)R(x,f(x))\rightarrow (\exists y)R(x,g(y))\,$

(26)

Spełnialność i prawdziwość

Formułę, która dla ustalonej interpretacji i wartościowania ma wartość logiczną $1\,$, nazywa się formułą spełnioną przy tej interpretacji i wartościowaniu. Formuła, dla której istnieje interpretacja i wartościowanie, przy których jest ona spełniona, nazywana jest formułą spełnialną. Z kolei formuła spełniona przy dowolnej interpretacji i wartościowaniu jest formułą prawdziwą.

Dla formuły, która nie jest prawdziwa, istnieje interpretacja i wartościowanie, przy których jej wartość logiczna wynosi $0\,$. Taką formułę nazywa się formułą falsyfikowalną. Z kolei formuła, która nie jest spełnialna, ma wartość logiczną $0\,$ przy dowolnej interpretacji i wartościowaniu. O takiej formule mówi się, że jest fałszywa.

Weryfikacja spełnienie formuły przy konkretnej interpretacji i wartościowaniu jest trywialna. Dalej będziemy się interesować tylko znacznie bardziej złożonym zagadnieniem rozstrzygania o prawdziwości bądź fałszywości formuł. Z wyjątkiem trywialnie małych dziedzin, nie można takiej weryfikacji przeprowadzić bezpośrednio opierając się na powyższych definicjach. Z tego wynika potrzeba stosowania wnioskowania.

Przykład: świat klocków. Łatwo sprawdzić, że następujące formuły są spełnione przy interpretacji i wartościowaniu określonych w poprzednich przykładach:

	$\neg P(y,x)\,$	(27)
	$\neg P(b,a)\lor Q(e,d)\,$	(28)
	$P(f(x),b)\,$	(29)
	$Q(f(x),y)\,$	(30)
	$P(x,y)\land Q(x,a)\,$	(31)
	$P(x,y)\rightarrow P(e,d)\,$	(32)
	$P(x,y)\rightarrow Q(x,y)\,$	(33)
	$(\forall x)(P(f(x),x)\lor R(f(x),x)\,$	(34)
	$(\forall x)(\forall y)(P(x,y)\rightarrow Q(x,y)\,$	(35)
	$(\forall x)(\forall y)(P(x,y)\rightarrow \neg R(x,a))\,$	(36)
	$(\forall x)R(g(x),x)\rightarrow (\exists y)P(y,x)\,$	(37)

Następujące formuły są także prawdziwe:

$P(x,y)\rightarrow (P(x,y)\rightarrow Q(x,y))\,$	(38)
$P(a,e)\lor \neg P(a,e)\,$	(39)

Konsekwencja semantyczna

W praktycznych zadaniach wnioskowania najczęściej rozważanym pytaniem jest w gruncie rzeczy nie tyle pytanie o prawdziwość pojedynczych formuł, co raczej o „wynikanie” pewnych formuł z innych formuł. Opisuje to relacja konsekwencji semantycznej, którą definiuje się bezpośrednio odwołując się do prawdziwości. Będziemy mówić, że formuła $\beta \,$ jest konsekwencją semantyczną zbioru formuł $\Gamma =\{\alpha _{1},\alpha _{2},\dots ,\alpha _{n}\}\,$, jeśli formuła $\alpha _{1}\land \alpha _{2}\land \dots \land \alpha _{n}\rightarrow \beta \,$ jest prawdziwa. Będziemy wówczas pisać $\Gamma \models \beta \,$.

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 \lor \neg \alpha \,$	(40)
	$\alpha \rightarrow (\beta \rightarrow \alpha )\,$	(41)
	$(\alpha \rightarrow (\beta \rightarrow \gamma ))\rightarrow ((\alpha \rightarrow \beta )\rightarrow (\alpha \rightarrow \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 \rightarrow \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 \rightarrow \beta ,\;\neg \beta }{\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 \lor \beta ,\;\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}\land \alpha _{2}\land \dots \land \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}\land \alpha _{2},\land \dots \land \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 {(\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 formuł $\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 \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:

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

(Zauważmy, że wszystkie te formuły są spełnione w dziedzinie świata klocków, przy interpretacji 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))\rightarrow R(f(a),a))\land ((R(f(a),a)\rightarrow R(a,f(a))))\,$

   (67)

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

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

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

   $\neg R(f(a),a)\,$

   (70)

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

   $P(f(a),a)\lor R(f(a),a)\,$

   (71)

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

   $P(f(a),a)\,$

   (72)

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

   $P(f(a),a)\rightarrow Q(f(a),a)\,$

   (73)

7. 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)

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

   $Q(f(a),a)\rightarrow Q(f(f(a)),a)\,$

   (75)

9. 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 syntaktycznej jako relację wyprowadzalności formuły z pewnej bazy wiedzy za pomocą tego systemu. Powiemy, że formuła $\beta \,$ jest konsekwencją syntaktyczną zbioru formuł $\Gamma \,$, jeśli istnieje dowód formuły $\beta \,$ ze zbioru formuł $\Gamma \,$. Będziemy wówczas pisać $\Gamma \vdash \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 konsekwencji syntaktycznej i semantycznej. Powiemy, że system wnioskowania jest poprawny, gdy dla dowolnego zbioru formuł $\Gamma \,$ oraz dowolnej formuły $\alpha \,$, jeśli $\alpha \,$ jest konsekwencją syntaktyczną $\Gamma \,$, to $\alpha \,$ jest także konsekwencją semantyczną. Z kolei system wnioskowania nazwiemy pełnym, gdy dla dowolnego zbioru formuł $\Gamma \,$ oraz dowolnej formuły $\alpha \,$, jeśli $\alpha \,$ jest konsekwencją semantyczną $\Gamma \,$, to $\alpha \,$ jest także konsekwencją syntaktyczną $\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}\land \alpha _{2}\land \dots \land \alpha _{n}\rightarrow \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.

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 modus ponens, dla której wymagamy na wejściu formuł postaci $\alpha \rightarrow \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

Przez 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\,$ zapisywać $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 formuły $\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)\rightarrow Q(x,b)\lor R(a,y)\,$

(77)

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

$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ł $\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))\land \neg Q(y,b)\rightarrow R(g(a),z)\lor P(f(x),c)\,$	(79)
	$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 $\{x/b,y/d,z/g(c),v/f(d),w/g(a)\}\,$.

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 pozytywnym, 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}\lor \neg L_{1}\lor \dots \lor \neg L_{n}\,$, gdzie $L_{0}\,$ jest literałem pozytywnym, a literały $\neg L_{1},\dots ,\neg L_{n}\,$ są literałami negatywnymi, może być także zapisana w postaci implikacji $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:

$\alpha \leftrightarrow \beta \,$	$\equiv (\alpha \rightarrow \beta )\land (\beta \rightarrow \alpha )\,$	(81)
$\alpha \rightarrow \beta \,$	$\equiv \neg \alpha \lor \beta \,$	(82)
$\neg (\neg \alpha )\,$	$\equiv \alpha \,$	(83)
$\neg (\alpha \lor \beta )\,$	$\equiv \neg \alpha \land \neg \beta \,$	(84)
$\neg (\alpha \land \beta )\,$	$\equiv \neg \alpha \lor \neg \beta \,$	(85)
$\alpha \lor (\beta \land \gamma )\,$	$\equiv (\alpha \lor \beta )\land (\alpha \lor \gamma )\,$	(86)
$\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:

	$P(x,y)\lor Q(y,a)\rightarrow P(z,b)\land \neg R(v,b)\,$	(88)
	$\neg (P(x,y)\lor Q(y,a))\lor (P(z,b)\land \neg R(v,b))\,$	(89)
	$(\neg P(x,y)\land \neg Q(y,a))\lor (P(z,b)\land \neg R(v,b))\,$	(90)
	$(\neg P(x,y)\lor P(z,b))\land (\neg P(x,y)\lor \neg R(v,b))\land \,$
	$\;\;\;\;\;\land (\neg Q(y,a)\lor P(z,b))\land (\neg Q(y,a)\lor \neg 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

$(\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 szczegółowych. 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ń:

$\neg (\forall x)\alpha \;\;\;\,$	$\equiv \;\;\;(\exists x)\neg \alpha \,$	(93)
$\neg (\exists x)\alpha \;\;\;\,$	$\equiv \;\;\;(\forall x)\neg \alpha \,$	(94)
$(\forall x)\alpha \diamondsuit \beta \;\;\;\,$	$\equiv \;\;\;(\forall x)(\alpha \diamondsuit \beta )\,$	(95)
$(\exists x)\alpha \diamondsuit \beta \;\;\;\,$	$\equiv \;\;\;(\exists x)(\alpha \diamondsuit \beta )\,$	(96)

gdzie $\diamondsuit \,$ może być operatorem $\lor \,$, $\land \,$, $\rightarrow \,$, $\leftrightarrow \,$, przy założeniu, że 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, usuwamy, 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łę:

$(\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:

$(\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:

$(\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 $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:

$(\forall x)(\forall v)\,$	$(\neg P(x,h_{1}(x))\lor P(h_{2}(x),b))\land (\neg P(x,h_{1}(x))\lor \neg R(v,b))\land \,$	(100)
	$\land (\neg Q(h_{1}(x),a)\lor P(h_{2}(x),b))\land (\neg Q(h_{1}(x),a)\lor \neg R(v,b))\,$

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 klauzulach. 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.