Tekst źródłowy strony Sztuczna inteligencja/SI Moduł 2 - Od logiki do wnioskowania

<!-- Wygenerowane przez tex2wikiu8.pl czas: wto lip 18 17:47:56 CEST 2006 -->

== Zadanie wnioskowania ==

Wnioskowanie formalne, czyli możliwe do zautomatyzowania, przetwarza
wiedzę zapisaną w odpowiednim [[#Składnia języka logiki|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ły wnioskowania|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 [[#Dowód|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:'''  {{Kotwica|Symbole stałych|}}oznaczane za pomocą liter <math>a,b,c\dots \,</math>.
: '''Symbole zmiennych:'''  {{Kotwica|Symbole zmiennych|}}oznaczane za pomocą liter <math>x,y,z\dots \,</math>.
: '''Symbole funkcyjne:'''  {{Kotwica|Symbole funkcyjne|}}oznaczane za pomocą liter <math>f,g,h\dots \,</math>; każdy symbol funkcyjny ma ustaloną liczbę argumentów.
: '''Symbole predykatowe:'''  {{Kotwica|Symbole predykatowe|}}oznaczane za pomocą liter <math>P,Q,R,\dots \,</math>; każdy symbol predykatowy ma ustaloną liczbę argumentów.
: '''Operatory logiczne:'''  <math>\neg \,</math> (negacja), <math>\land \,</math> (koniunkcja), <math>\lor \,</math> (alternatywa), <math>\rightarrow \,</math> (implikacja), <math>\leftrightarrow \,</math> (równoważność).
: '''Kwantyfikatory:'''  kwantyfikator ogólny <math>\forall \,</math>, kwantyfikator szczegółowy <math>\exists \,</math>.
: '''Nawiasy:'''  <math>( \,</math>, <math>) \,</math>, 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 <math>f \,</math> jest dowolnym <math>m \,</math>-argumentowym symbolem
funkcyjnym, a <math>t_1,t_2,\dots,t_m \,</math> są dowolnymi termami, to także
<math>f(t_1,t_2,\dots,t_m) \,</math> jest termem. Jak widać, stosując dowolny symbol
funkcyjny do argumentów będących termami uzyskujemy term.

=== Formuły atomowe ===

Jeśli <math>P \,</math> oznacza dowolny <math>m \,</math>-argumentowy symbol predykatowy, a
<math>t_1,t_2,\dots,t_m \,</math> są dowolnymi termami, to <math>P(t_1,t_2,\dots,t_m) \,</math>
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 <math>\alpha \,</math> jest formułą, to <math>(\alpha) \,</math> jest formułą.
* Jeśli <math>\alpha \,</math> jest formułą, to <math>\neg\alpha \,</math> jest formułą.
* Jeśli <math>\alpha \,</math> i <math>\beta \,</math> są formułami, to:
** <math>\alpha\land\beta \,</math> jest formułą,
** <math>\alpha\lor\beta \,</math> jest formułą,
** <math>\alpha\rightarrow\beta \,</math> jest formułą,
** <math>\alpha\leftrightarrow\beta \,</math> jest formułą.
* Jeśli <math>\alpha \,</math> jest formułą i <math>x \,</math> jest symbolem zmiennej, to
** <math>(\forall x)\alpha \,</math> jest formułą,
** <math>(\exists x)\alpha \,</math> jest formułą.

== Semantyka języka logiki ==

Semantyka języka logiki określa sposób, w jaki formułom zapisanym
zgodnie z podanymi wyżej [[#Składnia języka logiki|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 <math>\{A,B,C,D,E\} \,</math>.

<!-- begin{center} --><div align="center">
<!-- begin{wiki} -->
[[Grafika:SI M2 Klocki.png]]
<!-- end{wiki} -->
<!-- end{center} --></div>

=== Interpretacja symboli ===

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

: '''Symbole stałych:'''  [[#Symbole stałych|symbol stałej]] <math>a \,</math> oznacza pewien obiekt z dziedziny <math>I(a)\in X \,</math>.
: '''Symbole funkcyjne:'''  <math>m \,</math>-argumentowy [[#Symbole funkcyjne|symbol funkcyjny]] <math>f \,</math> oznacza <math>m \,</math>-argumentową funkcję <math>I(f): X^m\mapsto X \,</math>.
: '''Symbole predykatowe:'''  <math>m \,</math>-argumentowy [[#Symbole predykatowe|symbol predykatowy]] <math>P \,</math> oznacza <math>m \,</math>-argumentową relację <math>I(P)\subset X^m \,</math> (równoważnie, możemy przyjąć, że <math>P \,</math> oznacza funkcję <math>I(P): X^m\mapsto\{0,1\} \,</math>).

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

Operatory logiczne, kwantyfikatory i nawiasy służą do budowania
[[#Formuły złożone|formuł złożonych]] z formuł atomowych i nie mają samodzielnej interpretacji. [[#Symbole zmiennych|Symbole zmiennych]] są interpretowane - w przeciwnym przypadku byłyby identyczne z symbolami stałych. {{Kotwica|Wartościowanie|}}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 <math>x \,</math> wartościowanie <math>v \,</math> określa wartość <math>v(x)\in X \,</math>.

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

<!-- begin{align}  TODO: kolumny-->
:{| width="100%"
| width="1" align="right"|<!-- equation 1 --><math>I(a) = \,</math>
| align="left" |<math>A \,</math>
| width="5%" align="right" | ''(1)''
|-
| width="1" align="right"|<!-- equation 2 --><math>I(b) = \,</math>
| align="left" |<math>B \,</math>
| width="5%" align="right" | ''(2)''
|-
| width="1" align="right"|<!-- equation 3 --><math>I(c) = \,</math>
| align="left" |<math>C \,</math>
| width="5%" align="right" | ''(3)''
|-
| width="1" align="right"|<!-- equation 4 --><math>I(d) = \,</math>
| align="left" |<math>D \,</math>
| width="5%" align="right" | ''(4)''
|-
| width="1" align="right"|<!-- equation 5 --><math>I(e) = \,</math>
| align="left" |<math>E \,</math>
| width="5%" align="right" | ''(5)''
|-
|}
<!-- end{align} -->
Przyjmiemy także, że w alfabecie znajdują się dwa symbole zmiennych
<math>x \,</math> i <math>y \,</math>, dla których określono wartościowanie następująco:

<!-- begin{align}  TODO: kolumny-->
:{| width="100%"
| width="1" align="right"|<!-- equation 6 --><math>v(x) = \,</math>
| align="left" |<math>C \,</math>
| width="5%" align="right" | ''(6)''
|-
| width="1" align="right"|<!-- equation 7 --><math>v(y) = \,</math>
| align="left" |<math>B \,</math>
| width="5%" align="right" | ''(7)''
|-
|}
<!-- end{align} -->
Załóżmy dalej, że alfabet zawiera dwa jednoargumentowe symbole
funkcyjne <math>f \,</math> i <math>g \,</math>. Nasza interpretacja będzie im przypisywać
odpowiednio dwuargumentowe funkcje określone na dziedzinie:

<!-- begin{align}  TODO: kolumny-->
:{| width="100%"
| width="1" align="right"|<!-- equation 8 --><math>I(f) = \,</math>
| align="left" |<math>\textit{gora} \,</math>
| width="5%" align="right" | ''(8)''
|-
| width="1" align="right"|<!-- equation 9 --><math>I(g) = \,</math>
| align="left" |<math>\textit{dol} \,</math>
| width="5%" align="right" | ''(9)''
|-
|}
<!-- end{align} -->
Funkcje te określimy następująco:

<!-- begin{align}  TODO: kolumny-->
:{| width="100%"
| width="30%" align="left"|<!-- equation 10 --><math>\textit{gora}(A) = B</math>
| align="left" | <math>\textit{dol}(A)=A \,</math>
| width="5%" align="right" | ''(10)''
|-
| width="30%" align="left"|<!-- equation 11 --><math>\textit{gora}(B) = C</math>
| align="left" | <math>\textit{dol}(B)=A \,</math>
| width="5%" align="right" | ''(11)''
|-
| width="30%" align="left"|<!-- equation 12 --><math>\textit{gora}(C) = C</math>
| align="left" | <math>\textit{dol}(C)=B \,</math>
| width="5%" align="right" | ''(12)''
|-
| width="30%" align="left"|<!-- equation 13 --><math>\textit{gora}(D) = E</math>
| align="left" | <math>\textit{dol}(D)= D \,</math>
| width="5%" align="right" | ''(13)''
|-
| width="30%" align="left"|<!-- equation 14 --><math>\textit{gora}(E) = E</math>
| align="left" | <math>\textit{dol}(E)= D \,</math>
| width="5%" align="right" | ''(14)''
|-
|}
<!-- end{align} -->
(jak widać, funkcja <math>\textit{gora} \,</math> przypisuje każdemu klockowi jego
sąsiada z góry, o ile istnieje, albo jego samego; podobnie funkcja
<math>\textit{dol} \,</math> 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 <math>P \,</math>, <math>Q \,</math> i <math>R \,</math>,
których interpretację ustalimy następująco:

<!-- begin{align}  TODO: kolumny-->
:{| width="100%"
| width="1" align="right"|<!-- equation 15 --><math>I(P) = \,</math>
| align="left" |<math>\textit{na} \,</math>
| width="5%" align="right" | ''(15)''
|-
| width="1" align="right"|<!-- equation 16 --><math>I(Q) = \,</math>
| align="left" |<math>\textit{nad} \,</math>
| width="5%" align="right" | ''(16)''
|-
| width="1" align="right"|<!-- equation 17 --><math>I(R) = \,</math>
| align="left" |<math>\textit{rowne} \,</math>
| width="5%" align="right" | ''(17)''
|-
|}
<!-- end{align} -->
przy czym:
* <math>\textit{na} \,</math> jest relacją dwuargumentową, do której należą wszystkie pary klocków takie, że pierwszy leży na drugim: <math>\langle B,A\rangle \,</math>, <math>\langle C, B\rangle \,</math>, <math>\langle E,D\rangle \,</math>,
* <math>\textit{nad} \,</math> jest relacją dwuargumentową, do której należą wszystkie pary klocków takie, że pierwszy leży nad drugim (tj. na nim lub wyżej): <math>\langle B,A\rangle \,</math>, <math>\langle C, A\rangle \,</math>, <math>\langle C,B\rangle \,</math>, <math>\langle E,D\rangle \,</math>,
* <math>\textit{rowne} \,</math> jest relacją dwuargumentową, do której należą wszystkie pary złożone z dwóch wystąpień tych samych klocków: <math>\langle A,A\rangle \,</math>, <math>\langle B,B\rangle \,</math>, <math>\langle C,C\rangle \,</math>, <math>\langle D,D\rangle \,</math>, <math>\langle E,E\rangle \,</math>.

=== Interpretacja termów ===

Interpretacja wraz z wartościowaniem pozwala ustalić znaczenie
dowolnego [[#Termy|termu]]. Dla interpretacji <math>I \,</math> i wartościowania <math>v \,</math> oznaczmy
dla wygody przez <math>I_v \,</math> ich połączenie, rozumiane następująco:
: '''dla symboli stałych:'''  <math>I_v(a)=I(a) \,</math>,
: '''dla symboli zmiennych:'''  <math>I_v(x)=v(x) \,</math>.

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ściowanie|wartościowania]] do wchodzących w ich skład zmiennych. Przy
ustalonej dziedzinie, interpretacji <math>I \,</math> i wartościowaniu <math>v \,</math>, może być
wyznaczone znaczenie każdego termu postaci <math>f(t_1,t_2,\dots,t_m) \,</math> w
następujący sposób:

<!-- equation 18 -->
:{| width="100%"
| width="95%" align="left" | <math>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)).
 \,</math>
| align="right" | ''(18)''
|}

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

<!-- begin{align}  TODO: kolumny-->
:{| width="100%"
| width="1" align="right"|<!-- equation 19 --><math>I_v(f(x)) = \,</math>
| align="left" |<math>C \,</math>
| width="5%" align="right" | ''(19)''
|-
| width="1" align="right"|<!-- equation 20 --><math>I_v(g(y)) = \,</math>
| align="left" |<math>A \,</math>
| width="5%" align="right" | ''(20)''
|-
|}
<!-- end{align} -->

=== Interpretacja formuł ===

[[#Formuły atomowe|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 <math>P(t_1,t_2,\dots,t_m) \,</math> otrzymujemy w
ten sposób relację <math>I(P) \,</math> oraz krotkę <math>m \,</math> obiektów z dziedziny
<math>\langle I_v(t_1),I_v(t_2),\dots,I_v(t_m)\rangle\in X^m \,</math>. Znaczeniem
formuły będzie jej wartość logiczna określona na podstawie tego, czy
krotka obiektów należy do relacji:

<!-- equation 21 -->
:{| width="100%"
| width="95%" align="left" | <math>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}
 \,</math>
| align="right" | ''(21)''
|}

Interpretacja [[#Formuły złożone|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
<math>\rightarrow \,</math>:

<!-- begin{center} --><div align="center">

<!-- \begin{tabular}{c|c||c} -->
:{| border="1" style="text-align:center"
|<math>I_v(\alpha) \,</math>  ||  <math>I_v(\beta) \,</math>  ||  <math>I_v(\alpha\rightarrow\beta) \,</math>
|-
|<math>0</math>  ||  <math>0</math>  ||  <math>1</math>
|-
|<math>0</math>  ||  <math>1</math>  ||  <math>1</math>
|-
|<math>1</math>  ||  <math>0</math>  ||  <math>0</math>
|-
|<math>1</math>  ||  <math>1</math>  ||  <math>1</math>
|-
|}
<!-- end{tabular} -->
<!-- end{center} --></div>

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ę
<math>X \,</math>, interpretację <math>I \,</math> i wartościowanie <math>v \,</math>, rozważmy interpretację
formuły postaci <math>(\forall x)\alpha \,</math>. Aby uniknąć wikłania się w
dyskusje o zasięgu kwantyfikatorów założymy, że w formule <math>\alpha \,</math> nie
występuje żaden inny kwantyfikator dla zmiennej <math>x \,</math> (czyli że
wszystkie wystąpienia zmiennej <math>x \,</math> w formule <math>\alpha \,</math> są
''wolne''). Wartość logiczną formuły <math>(\forall x)\alpha \,</math> przy
interpretacji <math>I \,</math> i wartościowaniu <math>v \,</math> ustalamy w następujący sposób:
# <math>I_v((\forall x)\alpha)=1 \,</math> wtedy i tylko wtedy gdy dla wszystkich wartościowań <math>v_x \,</math> różniących się od <math>v \,</math> co najwyżej wartością przypisywaną zmiennej <math>x \,</math> (a więc także dla <math>v_x \,</math> identycznego z <math>v \,</math>) uzyskujemy <math>I_{v_x}(\alpha)=1 \,</math>,
# <math>I_v((\forall x)\alpha)=0 \,</math> w przeciwnym przypadku.
Analogicznie dla formuły <math>(\exists x)\alpha \,</math>:
# <math>I_v((\exists x)\alpha)=1 \,</math> wtedy i tylko wtedy gdy istnieje wartościowanie <math>v_x \,</math> różniące się od <math>v \,</math> co najwyżej wartością przypisywaną zmiennej <math>x \,</math> (może to być w szczególności <math>v_x \,</math> identyczne z <math>v \,</math>) uzyskujemy <math>I_{v_x}(\alpha)=1 \,</math>,
# <math>I_v((\exists x)\alpha)=0 \,</math> 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ść <math>v(x) \,</math> wartościowanie <math>v \,</math> przypisuje zmiennej <math>x \,</math> objętej
kwantyfikatorem. Ważne jest tylko, aby przy niezmienionych wartościach
przypisywanych wszystkim pozostałym zmiennym można było stwierdzić, że
<math>I_v(\alpha)=1 \,</math> dla wszystkich możliwych wartości zmiennej <math>x \,</math> (w
przypadku kwantyfikatora ogólnego) albo dla przynajmniej jednej
wartości zmiennej <math>x \,</math> (w przypadku kwantyfikatora szczegółowego) z
dziedziny <math>X \,</math>.

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

<!-- begin{align}  TODO: kolumny-->
:{| width="100%"
| width="1" align="right"|<!-- equation 22 --><math>I_v(P(x,y)) = \,</math>
| align="left" |<math>1 \,</math>
| width="5%" align="right" | ''(22)''
|-
| width="1" align="right"|<!-- equation 23 --><math>I_v(Q(x,y)) = \,</math>
| align="left" |<math>1 \,</math>
| width="5%" align="right" | ''(23)''
|-
|}
<!-- end{align} -->
a więc <math>I_v(P(x,y)\rightarrow Q(x,y))=1 \,</math>. Nietrudno się przekonać, że
także dla formuły <math>(\forall x)(\forall y)(P(x,y)\rightarrow Q(x,y)) \,</math>
uzyskamy wartość logiczną <math>1 \,</math>, sprawdzając, że <math>I_v(P(x,y)\rightarrow Q(x,y)) \,</math> niezależnie od wartości przypisanych zmiennym <math>x \,</math> i <math>y \,</math>.

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:
<!-- equation 24 -->
:{| width="100%"
| width="95%" align="left" | <math>(\forall x)(\forall y) P(x,y)\rightarrow R(x,f(y))
 \,</math>
| align="right" | ''(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.
<!-- equation 25 -->
:{| width="100%"
| width="95%" align="left" | <math>(\forall x)(\forall y)\neg(P(x,y)\land P(y,x))
 \,</math>
| align="right" | ''(25)''
|}

* Każdy klocek, który nie ma górnego sąsiada, jest dolnym sąsiadem: jakiegoś innego klocka.
<!-- equation 26 -->
:{| width="100%"
| width="95%" align="left" | <math>(\forall x) R(x,f(x)) \rightarrow (\exists y) R(x,g(y))
 \,</math>
| align="right" | ''(26)''
|}

=== Spełnialność i prawdziwość ===

Formułę, która dla ustalonej interpretacji i wartościowania ma wartość
logiczną <math>1 \,</math>, nazywa się formułą ''spełnioną'' przy tej
interpretacji i wartościowaniu. {{Kotwica|Spełnialność|}}Formuła, dla której istnieje
interpretacja i wartościowanie, przy których jest ona spełniona,
nazywana jest formułą ''spełnialną''. {{Kotwica|Prawdziwość|}}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 <math>0 \,</math>. Taką
formułę nazywa się formułą ''falsyfikowalną''. Z kolei formuła,
która nie jest spełnialna, ma wartość logiczną <math>0 \,</math> 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:

<!-- begin{align}  TODO: kolumny-->
:{| width="100%"
| width="1" align="right"|<!-- equation 27 -->&nbsp;
| align="left" |<math>\neg P(y,x) \,</math>
| width="5%" align="right" | ''(27)''
|-
| width="1" align="right"|<!-- equation 28 -->&nbsp;
| align="left" |<math>\neg P(b,a)\lor Q(e,d) \,</math>
| width="5%" align="right" | ''(28)''
|-
| width="1" align="right"|<!-- equation 29 -->&nbsp;
| align="left" |<math>P(f(x),b) \,</math>
| width="5%" align="right" | ''(29)''
|-
| width="1" align="right"|<!-- equation 30 -->&nbsp;
| align="left" |<math>Q(f(x),y) \,</math>
| width="5%" align="right" | ''(30)''
|-
| width="1" align="right"|<!-- equation 31 -->&nbsp;
| align="left" |<math>P(x,y)\land Q(x,a) \,</math>
| width="5%" align="right" | ''(31)''
|-
| width="1" align="right"|<!-- equation 32 -->&nbsp;
| align="left" |<math>P(x,y) \rightarrow P(e,d) \,</math>
| width="5%" align="right" | ''(32)''
|-
| width="1" align="right"|<!-- equation 33 -->&nbsp;
| align="left" |<math>P(x,y)\rightarrow Q(x,y) \,</math>
| width="5%" align="right" | ''(33)''
|-
| width="1" align="right"|<!-- equation 34 -->&nbsp;
| align="left" |<math>(\forall x) (P(f(x),x)\lor R(f(x),x) \,</math>
| width="5%" align="right" | ''(34)''
|-
| width="1" align="right"|<!-- equation 35 -->&nbsp;
| align="left" |<math>(\forall x)(\forall y) (P(x,y)\rightarrow Q(x,y) \,</math>
| width="5%" align="right" | ''(35)''
|-
| width="1" align="right"|<!-- equation 36 -->&nbsp;
| align="left" |<math>(\forall x)(\forall y) (P(x,y)\rightarrow \neg R(x,a)) \,</math>
| width="5%" align="right" | ''(36)''
|-
| width="1" align="right"|<!-- equation 37 -->&nbsp;
| align="left" |<math>(\forall x) R(g(x),x)\rightarrow (\exists y) P(y,x) \,</math>
| width="5%" align="right" | ''(37)''
|-
|}
<!-- end{align} -->
Następujące formuły są także prawdziwe:

<!-- begin{align}  TODO: kolumny-->
:{| width="100%"
| width="95%" align="left"|<!-- equation 38 --><math>P(x,y)\rightarrow (P(x,y)\rightarrow Q(x,y)) \,</math>
| width="5%" align="right" | ''(38)''
|-
| width="95%" align="left"|<!-- equation 39 --><math>P(a,e)\lor\neg P(a,e) \,</math>
| width="5%" align="right" | ''(39)''
|-
|}
<!-- end{align} -->

=== 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ść|prawdziwości]]. Będziemy mówić, że formuła
<math>\beta \,</math> jest konsekwencją semantyczną zbioru formuł
<math>\Gamma=\{\alpha_1,\alpha_2,\dots,\alpha_n\} \,</math>, jeśli formuła
<math>\alpha_1\land\alpha_2\land\dots\land\alpha_n\rightarrow\beta \,</math> jest
prawdziwa. Będziemy wówczas pisać <math>\Gamma\models\beta \,</math>.

== 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 <math>\alpha \,</math>, <math>\beta \,</math> i <math>\gamma \,</math> można zastąpić dowolnymi
formułami innymi symbolami predykatowymi, zaś symbole zmiennych <math>x \,</math> i
<math>y \,</math> można zastąpić dowolnymi innymi symbolami zmiennych.

<!-- begin{align}  TODO: kolumny-->
:{| width="100%"
| width="1" align="right"|<!-- equation 40 -->&nbsp;
| align="left" |<math>\alpha\lor\neg\alpha \,</math>
| width="5%" align="right" | ''(40)''
|-
| width="1" align="right"|<!-- equation 41 -->&nbsp;
| align="left" |<math>\alpha\rightarrow(\beta\rightarrow\alpha) \,</math>
| width="5%" align="right" | ''(41)''
|-
| width="1" align="right"|<!-- equation 42 -->&nbsp;
| align="left" |<math>(\alpha\rightarrow(\beta\rightarrow\gamma))\rightarrow ((\alpha\rightarrow\beta)\rightarrow(\alpha\rightarrow\gamma)) \,</math>
| width="5%" align="right" | ''(42)''
|-
|}
<!-- end{align} -->

=== Reguły wnioskowania ===

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

<!-- equation 43 -->
:{| width="100%"
| width="95%" align="left" | <math>\frac{\alpha_1\;\alpha_2\;\dots.\;\alpha_n}{\beta}
 \,</math>
| align="right" | ''(43)''
|}
gdzie <math>\alpha_1,\alpha_2,\dots,\alpha_n \,</math> oznaczają wzorce formuł
wejściowych reguły, a <math>\beta \,</math> 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.

<!-- equation 44 --><!-- label: eq_modusponens -->{{kotwica|eq_modusponens|}}
:{| width="100%"
| width="95%" align="left" | <math>\frac{\alpha\rightarrow\beta,\;\alpha}{\beta}

 \,</math>
| align="right" | ''(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.

<!-- equation 45 --><!-- label: eq_modustollens -->{{kotwica|eq_modustollens|}}
:{| width="100%"
| width="95%" align="left" | <math>\frac{\alpha\rightarrow\beta,\;\neg\beta}{\neg\alpha}

 \,</math>
| align="right" | ''(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.

<!-- equation 46 --><!-- label: eq_alternatywa -->{{kotwica|eq_alternatywa|}}
:{| width="100%"
| width="95%" align="left" | <math>\frac{\alpha\lor\beta,\;\neg\beta}{\alpha}

 \,</math>
| align="right" | ''(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.

<!-- equation 47 --><!-- label: eq_koniunkcja1 -->{{kotwica|eq_koniunkcja1|}}
:{| width="100%"
| width="95%" align="left" | <math>\frac{\alpha_1,\;\alpha_2,\;\dots,\;\alpha_n}
{\alpha_1\land\alpha_2\land\dots\land\alpha_n}

 \,</math>
| align="right" | ''(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.

<!-- equation 48 --><!-- label: eq_koniunkcja2 -->{{kotwica|eq_koniunkcja2|}}
:{| width="100%"
| width="95%" align="left" | <math>\frac{\alpha_1\land\alpha_2,\land\dots\land\alpha_n}
{\alpha_1,\;\alpha_2,\;\dots,\;\alpha_n}

 \,</math>
| align="right" | ''(48)''
|}

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

<!-- equation 49 --><!-- label: eq_specjalizacja -->{{kotwica|eq_specjalizacja|}}
:{| width="100%"
| width="95%" align="left" | <math>\frac{(\forall x)\alpha}{\alpha[x/t]}

 \,</math>
| align="right" | ''(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 <math>x \,</math> przez dowolny term <math>t \,</math>,
co zostało zapisane jako <math>\alpha[x/t] \,</math>. 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 <math>\beta \,</math> ze zbioru formuł <math>\Gamma \,</math> nazywamy dowolny
ciąg formuł <math>\alpha_1,\alpha_2,\dots,\alpha_{n-1},\alpha_n \,</math>
spełniający warunki:
# <math>\alpha_n=\beta \,</math>,
# dla każdego <math>i=1,2,\dots.n \,</math> zachodzi jedna z następujących sytuacji:
## <math>\alpha_i \,</math> jest aksjomatem,
## <math>\alpha_i\in\Gamma \,</math>,
## <math>\alpha_i \,</math> jest wynikiem zastosowania pewnej reguły wnioskowania do formuł <math>\alpha_{j_1},\dots,\alpha_{jk} \,</math>, gdzie <math>j_1,\dots,j_k<n \,</math>.


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

<!-- begin{align}  TODO: kolumny-->
:{| width="100%"
| width="1" align="right"|<!-- equation 50 --><!-- label: eq_bw1 -->{{kotwica|eq_bw1|}}&nbsp;
| align="left" |<math>(\forall x) R(x,x) \,</math>
| width="5%" align="right" | ''(50)''
|-
| width="1" align="right"|<!-- equation 51 --><!-- label: eq_bw2 -->{{kotwica|eq_bw2|}}&nbsp;
| align="left" |<math>(\forall x)(\forall y) ((R(x,y)\rightarrow R(y,x)) \land((R(y,x)\rightarrow R(x,y)))) \,</math>
| width="5%" align="right" | ''(51)''
|-
| width="1" align="right"|<!-- equation 52 --><!-- label: eq_bw3 -->{{kotwica|eq_bw3|}}&nbsp;
| align="left" |<math>(\forall x) (P(x,g(x))\lor R(x,g(x))) \,</math>
| width="5%" align="right" | ''(52)''
|-
| width="1" align="right"|<!-- equation 53 --><!-- label: eq_bw4 -->{{kotwica|eq_bw4|}}&nbsp;
| align="left" |<math>(\forall x) (P(f(x),x)\lor R(f(x),x)) \,</math>
| width="5%" align="right" | ''(53)''
|-
| width="1" align="right"|<!-- equation 54 --><!-- label: eq_bw5 -->{{kotwica|eq_bw5|}}&nbsp;
| align="left" |<math>(\forall x)(\forall y) (P(x,y)\rightarrow Q(x,y)) \,</math>
| width="5%" align="right" | ''(54)''
|-
| width="1" align="right"|<!-- equation 55 --><!-- label: eq_bw6 -->{{kotwica|eq_bw6|}}&nbsp;
| align="left" |<math>(\forall x)(\forall y) (Q(x,y)\rightarrow Q(f(x),y)) \,</math>
| width="5%" align="right" | ''(55)''
|-
| width="1" align="right"|<!-- equation 56 --><!-- label: eq_bw7 -->{{kotwica|eq_bw7|}}&nbsp;
| align="left" |<math>(\forall x)(\forall y) (Q(x,y)\rightarrow Q(x,g(y))) \,</math>
| width="5%" align="right" | ''(56)''
|-
| width="1" align="right"|<!-- equation 57 --><!-- label: eq_bw8 -->{{kotwica|eq_bw8|}}&nbsp;
| align="left" |<math>\neg R(a,f(a)) \,</math>
| width="5%" align="right" | ''(57)''
|-
| width="1" align="right"|<!-- equation 58 --><!-- label: eq_bw9 -->{{kotwica|eq_bw9|}}&nbsp;
| align="left" |<math>\neg R(b,f(b)) \,</math>
| width="5%" align="right" | ''(58)''
|-
| width="1" align="right"|<!-- equation 59 --><!-- label: eq_bw10 -->{{kotwica|eq_bw10|}}&nbsp;
| align="left" |<math>R(c,f(c)) \,</math>
| width="5%" align="right" | ''(59)''
|-
| width="1" align="right"|<!-- equation 60 --><!-- label: eq_bw11 -->{{kotwica|eq_bw11|}}&nbsp;
| align="left" |<math>\neg R(d,f(d)) \,</math>
| width="5%" align="right" | ''(60)''
|-
| width="1" align="right"|<!-- equation 61 --><!-- label: eq_bw12 -->{{kotwica|eq_bw12|}}&nbsp;
| align="left" |<math>R(d,f(e)) \,</math>
| width="5%" align="right" | ''(61)''
|-
| width="1" align="right"|<!-- equation 62 --><!-- label: eq_bw13 -->{{kotwica|eq_bw13|}}&nbsp;
| align="left" |<math>R(a,g(a)) \,</math>
| width="5%" align="right" | ''(62)''
|-
| width="1" align="right"|<!-- equation 63 --><!-- label: eq_bw14 -->{{kotwica|eq_bw14|}}&nbsp;
| align="left" |<math>\neg R(b,g(b)) \,</math>
| width="5%" align="right" | ''(63)''
|-
| width="1" align="right"|<!-- equation 64 --><!-- label: eq_bw15 -->{{kotwica|eq_bw15|}}&nbsp;
| align="left" |<math>\neg R(c,g(c)) \,</math>
| width="5%" align="right" | ''(64)''
|-
| width="1" align="right"|<!-- equation 65 --><!-- label: eq_bw16 -->{{kotwica|eq_bw16|}}&nbsp;
| align="left" |<math>R(d,g(d)) \,</math>
| width="5%" align="right" | ''(65)''
|-
| width="1" align="right"|<!-- equation 66 --><!-- label: eq_bw17 -->{{kotwica|eq_bw17|}}&nbsp;
| align="left" |<math>\neg R(e,g(e)) \,</math>
| width="5%" align="right" | ''(66)''
|-
|}
<!-- end{align} -->
(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 <math>Q(f(f(a)),a) \,</math>.

<ol>
<li>
Stosując (dwukrotnie) regułę specjalizacji (<!-- ref: eq_specjalizacja -->[[#eq_specjalizacja|49]]) do formuły (<!-- ref: eq_bw2 -->[[#eq_bw2|51]]) z podstawieniem stałej <math>a \,</math> w miejsce zmiennej <math>x \,</math> oraz termu <math>f(a) \,</math> w miejsce zmiennej <math>y \,</math> dostajemy:
<!-- equation 67 -->
:{| width="100%"
| width="95%" align="left" | <math>(R(a,f(a))\rightarrow R(f(a),a))
\land((R(f(a),a)\rightarrow R(a,f(a))))
 \,</math>
| align="right" | ''(67)''
|}
</li><li>
Do formuły uzyskanej w poprzednim kroku stosujemy regułę: koniunkcji (<!-- ref: eq_koniunkcja2 -->[[#eq_koniunkcja2|48]]), otrzymując w ten sposób dwie formuły:
<!-- begin{align}  TODO: kolumny-->
:{| width="100%"
| width="1" align="right"|<!-- equation 68 -->&nbsp;
| align="left" |<math>R(a,f(a))\rightarrow R(f(a),a) \,</math>
| width="5%" align="right" | ''(68)''
|-
| width="1" align="right"|<!-- equation 69 -->&nbsp;
| align="left" |<math>R(f(a),a)\rightarrow R(a,f(a)) \,</math>
| width="5%" align="right" | ''(69)''
|-
|}
<!-- end{align} -->
</li><li>
Do drugiej z otrzymanych w poprzednim kroku formuł oraz do: formuły (<!-- ref: eq_bw8 -->[[#eq_bw8|57]]) stosujemy obecnie regułę ''modus tollens'' (<!-- ref: eq_modustollens -->[[#eq_modustollens|45]]), co daje w wyniku:
<!-- equation 70 --><!-- label: eq_d1 -->{{kotwica|eq_d1|}}
:{| width="100%"
| width="95%" align="left" | <math>\neg R(f(a),a)

 \,</math>
| align="right" | ''(70)''
|}
</li><li>
Stosując regułę specjalizacji (<!-- ref: eq_specjalizacja -->[[#eq_specjalizacja|49]]) do: formuły (<!-- ref: eq_bw4 -->[[#eq_bw4|53]]) z podstawieniem stałej <math>a \,</math> w miejsce zmiennej <math>x \,</math> dostajemy:
<!-- equation 71 --><!-- label: eq_d2 -->{{kotwica|eq_d2|}}
:{| width="100%"
| width="95%" align="left" | <math>P(f(a),a)\lor R(f(a),a)

 \,</math>
| align="right" | ''(71)''
|}
</li><li>
Stosując regułę wnioskowania (<!-- ref: eq_alternatywa -->[[#eq_alternatywa|46]]) do formuł: uzyskanych w dwóch poprzednich krokach (<!-- ref: eq_d2 -->[[#eq_d2|71]]) i (<!-- ref: eq_d1 -->[[#eq_d1|70]]) wyprowadzamy:
<!-- equation 72 --><!-- label: eq_d3 -->{{kotwica|eq_d3|}}
:{| width="100%"
| width="95%" align="left" | <math>P(f(a),a)

 \,</math>
| align="right" | ''(72)''
|}
</li><li>
Stosując regułę specjalizacji (<!-- ref: eq_specjalizacja -->[[#eq_specjalizacja|49]]) do: formuły (<!-- ref: eq_bw5 -->[[#eq_bw5|54]]) z podstawieniem termu <math>f(a) \,</math> w miejsce zmiennej <math>x \,</math> oraz stałej <math>a \,</math> w miejsce zmiennej <math>y \,</math> otrzymujemy:
<!-- equation 73 --><!-- label: eq_d4 -->{{kotwica|eq_d4|}}
:{| width="100%"
| width="95%" align="left" | <math>P(f(a),a)\rightarrow Q(f(a),a)

 \,</math>
| align="right" | ''(73)''
|}
</li><li>
Przez zastosowanie reguły ''modus ponens'': (<!-- ref: eq_modusponens -->[[#eq_modusponens|44]]) do formuł uzyskanych w dwóch poprzednich krokach dowodu (<!-- ref: eq_d4 -->[[#eq_d4|73]]) i (<!-- ref: eq_d3 -->[[#eq_d3|72]]) wyprowadzamy formułę:
<!-- equation 74 --><!-- label: eq_d5 -->{{kotwica|eq_d5|}}
:{| width="100%"
| width="95%" align="left" | <math>Q(f(a),a)

 \,</math>
| align="right" | ''(74)''
|}
</li><li>
Stosując regułę specjalizacji (<!-- ref: eq_specjalizacja -->[[#eq_specjalizacja|49]]) do: formuły (<!-- ref: eq_bw6 -->[[#eq_bw6|55]]) z podstawieniem termu <math>f(a) \,</math> w miejsce zmiennej <math>x \,</math> oraz stałej <math>a \,</math> w miejsce zmiennej <math>y \,</math> otrzymujemy:
<!-- equation 75 --><!-- label: eq_d6 -->{{kotwica|eq_d6|}}
:{| width="100%"
| width="95%" align="left" | <math>Q(f(a),a)\rightarrow Q(f(f(a)),a)

 \,</math>
| align="right" | ''(75)''
|}
</li><li>
Wreszcie zastosowanie reguły ''modus ponens'': (<!-- ref: eq_modusponens -->[[#eq_modusponens|44]]) do formuł wyprowadzonych w dwóch poprzednich krokach (<!-- ref: eq_d6 -->[[#eq_d6|75]]) i (<!-- ref: eq_d5 -->[[#eq_d5|74]]) pozwala wygenerować poszukiwaną formułę docelową <math>Q(f(f(a)),a) \,</math>, która tym samym została udowodniona.
</li>
</ol>

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 [[#System wnioskowania|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 <math>\beta \,</math> jest
konsekwencją syntaktyczną zbioru formuł <math>\Gamma \,</math>, jeśli istnieje dowód
formuły <math>\beta \,</math> ze zbioru formuł <math>\Gamma \,</math>. Będziemy wówczas pisać
<math>\Gamma\vdash\beta \,</math>.

=== Poprawny i pełny system wnioskowania ===

Można podać dowolnie wiele [[#System wnioskowania|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ł <math>\Gamma \,</math> oraz dowolnej formuły <math>\alpha \,</math>, jeśli
<math>\alpha \,</math> jest konsekwencją syntaktyczną <math>\Gamma \,</math>, to <math>\alpha \,</math> jest
także konsekwencją semantyczną. Z kolei system wnioskowania nazwiemy
pełnym, gdy dla dowolnego zbioru formuł <math>\Gamma \,</math> oraz dowolnej formuły
<math>\alpha \,</math>, jeśli <math>\alpha \,</math> jest konsekwencją semantyczną <math>\Gamma \,</math>, to
<math>\alpha \,</math> jest także konsekwencją syntaktyczną <math>\Gamma \,</math>.

O pojedynczych elementach systemu wnioskowania - [[#Aksjomaty|aksjomatach]] i
[[#Reguły wnioskowania|regułach wnioskowania]] - także możemy mówić, że są bądź nie są
poprawne. {{Kotwica|Aksjomat poprawny|}}Aksjomat jest poprawny, jeśli jest [[#Prawdziwość|formułą prawdziwą]].
{{Kotwica|Reguła wnioskowania poprawna|}}Reguła wnioskowania postaci

<!-- equation 76 -->
:{| width="100%"
| width="95%" align="left" | <math>\frac{\alpha_1\;\alpha_2\;\dots.\;\alpha_n}{\beta}
 \,</math>
| align="right" | ''(76)''
|}
jest poprawna, jeśli dla każdej możliwej konkretyzacji wzorców formuł
wejściowych formuła postaci
<math>\alpha_1\land\alpha_2\land\dots\land\alpha_n\rightarrow\beta \,</math> 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
<math>\alpha\rightarrow\beta \,</math> i <math>\alpha \,</math>. 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 <math>t \,</math> zmiennej <math>x \,</math> zapisywać <math>x/t \,</math>.
Podstawienie <math>\{x/t_1,y/t_2,z/t_3\} \,</math> zawiera trzy wiązania,
przypisujące zmiennym <math>x,y,z \,</math> odpowiednio termy <math>t_1,t_2,t_3 \,</math>.
Wynikiem zastosowania podstawienia <math>\sigma \,</math> do formuły <math>\alpha \,</math> jest
formuła <math>\alpha[\sigma] \,</math>, w której wszystkie wystąpienia zmiennych
objętych podstawieniem <math>\sigma \,</math> 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łę <math>\alpha \,</math> następującej postaci:

<!-- equation 77 -->
:{| width="100%"
| width="95%" align="left" | <math>P(x,y) \rightarrow Q(x,b)\lor R(a,y)
 \,</math>
| align="right" | ''(77)''
|}
oraz podstawienie <math>\sigma=\{x/a,y/f(b)\} \,</math>. Wynikiem zastosowania
podstawienia <math>\sigma \,</math> do formuły <math>\alpha \,</math> jest formuła
<math>\alpha[\sigma] \,</math> następującej postaci:

<!-- equation 78 -->
:{| width="100%"
| width="95%" align="left" | <math>P(a,f(b))\rightarrow Q(a,b)\lor R(a,f(b))
 \,</math>
| align="right" | ''(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|podstawienia]]. Dla dwóch formuł <math>\alpha \,</math> i <math>\beta \,</math>
unifikatorem nazwiemy dowolne podstawienie <math>\sigma \,</math> takie, że formuły
<math>\alpha[\sigma] \,</math> i <math>\beta[\sigma] \,</math> 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ł:

<!-- begin{align}  TODO: kolumny-->
:{| width="100%"
| width="1" align="right"|<!-- equation 79 -->&nbsp;
| align="left" |<math>P(x,f(y)) \land \neg Q(y,b) \rightarrow R(g(a),z)\lor P(f(x),c) \,</math>
| width="5%" align="right" | ''(79)''
|-
| width="1" align="right"|<!-- equation 80 -->&nbsp;
| align="left" |<math>P(b,v) \land \neg Q(d,b) \rightarrow R(w,g(c))\lor P(f(b),c) \,</math>
| width="5%" align="right" | ''(80)''
|-
|}
<!-- end{align} -->
najbardziej ogólnym unifikatorem jest podstawienie
<math>\{x/b, y/d, z/g(c), v/f(d), w/g(a)\} \,</math>.

== 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
<math>L_0\lor \neg L_1\lor\dots\lor \neg L_n \,</math>, gdzie <math>L_0 \,</math> jest literałem
pozytywnym, a literały <math>\neg L_1,\dots,\neg L_n \,</math> są literałami
negatywnymi, może być także zapisana w postaci implikacji
<math>L_1\land L_2\land\dots\land L_n\rightarrow L_0 \,</math>.

Klauzule Horna, zapisane w postaci implikacji, to oczywiście dogodna
forma zapisu formuł do stosowania podanej wyżej reguły wnioskowania
''[[#eq_modusponens|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łę (<!-- ref: eq_koniunkcja2 -->[[#eq_koniunkcja2|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:

<!-- begin{align}  TODO: kolumny-->
:{| width="100%"
| width="1" align="right"|<!-- equation 81 --><math>\alpha\leftrightarrow\beta \,</math>
| align="left" |<math>\equiv (\alpha\rightarrow\beta)\land(\beta\rightarrow\alpha) \,</math>
| width="5%" align="right" | ''(81)''
|-
| width="1" align="right"|<!-- equation 82 --><math>\alpha\rightarrow\beta \,</math>
| align="left" |<math>\equiv \neg\alpha\lor\beta \,</math>
| width="5%" align="right" | ''(82)''
|-
| width="1" align="right"|<!-- equation 83 --><math>\neg(\neg\alpha) \,</math>
| align="left" |<math>\equiv \alpha \,</math>
| width="5%" align="right" | ''(83)''
|-
| width="1" align="right"|<!-- equation 84 --><math>\neg(\alpha\lor\beta) \,</math>
| align="left" |<math>\equiv \neg\alpha\land\neg\beta \,</math>
| width="5%" align="right" | ''(84)''
|-
| width="1" align="right"|<!-- equation 85 --><math>\neg(\alpha\land\beta) \,</math>
| align="left" |<math>\equiv \neg\alpha\lor\neg\beta \,</math>
| width="5%" align="right" | ''(85)''
|-
| width="1" align="right"|<!-- equation 86 --><math>\alpha\lor(\beta\land\gamma) \,</math>
| align="left" |<math>\equiv (\alpha\lor\beta)\land(\alpha\lor\gamma) \,</math>
| width="5%" align="right" | ''(86)''
|-
| width="1" align="right"|<!-- equation 87 --><math>\alpha\land(\beta\lor\gamma) \,</math>
| align="left" |<math>\equiv (\alpha\land\beta)\lor(\alpha\land\gamma) \,</math>
| width="5%" align="right" | ''(87)''
|-
|}
<!-- end{align} -->

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:

<!-- begin{align}  TODO: kolumny-->
:{| width="100%"
| width="1" align="right"|<!-- equation 88 -->&nbsp;
| align="left" |<math>P(x,y)\lor Q(y,a)\rightarrow P(z,b)\land \neg R(v,b) \,</math>
| width="5%" align="right" | ''(88)''
|-
| width="1" align="right"|<!-- equation 89 -->&nbsp;
| align="left" |<math>\neg(P(x,y)\lor Q(y,a)) \lor (P(z,b)\land \neg R(v,b)) \,</math>
| width="5%" align="right" | ''(89)''
|-
| width="1" align="right"|<!-- equation 90 -->&nbsp;
| align="left" |<math>(\neg P(x,y)\land\neg Q(y,a)) \lor (P(z,b)\land \neg R(v,b)) \,</math>
| width="5%" align="right" | ''(90)''
|-
| width="1" align="right"|<!-- equation 90 -->&nbsp;
| align="left" |<math>(\neg P(x,y)\lor P(z,b))\land(\neg P(x,y)\lor \neg R(v,b))\land \,</math>
| width="5%" align="right" | &nbsp;
|-
| width="1" align="right"|<!-- equation 91 -->&nbsp;
| align="left" |<math>\;\;\;\;\;\land (\neg Q(y,a)\lor P(z,b))\land(\neg Q(y,a)\lor \neg R(v,b)) \,</math>
| width="5%" align="right" | ''(91)''
|-
|}
<!-- end{align} -->

=== Postać standardowa Skolema ===

Postać standardowa Skolema jest rozszerzeniem
[[#Koniunkcyjna postać normalna|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

<!-- equation 92 -->
:{| width="100%"
| width="95%" align="left" | <math>(\forall\dots)(\forall\dots)\dots(\forall\dots)\alpha.
 \,</math>
| align="right" | ''(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ń:

<!-- begin{align}  TODO: kolumny-->
:{| width="100%"
| width="1" align="right"|<!-- equation 93 --><math>\neg (\forall x)\alpha \;\;\;\,</math>
| align="left" |<math>\equiv\;\;\; (\exists x)\neg \alpha \,</math>
| width="5%" align="right" | ''(93)''
|-
| width="1" align="right"|<!-- equation 94 --><math>\neg (\exists x)\alpha \;\;\;\,</math>
| align="left" |<math>\equiv\;\;\; (\forall x)\neg \alpha \,</math>
| width="5%" align="right" | ''(94)''
|-
| width="1" align="right"|<!-- equation 95 --><math>(\forall x)\alpha\diamondsuit\beta \;\;\;\,</math>
| align="left" |<math>\equiv\;\;\; (\forall x)(\alpha\diamondsuit\beta) \,</math>
| width="5%" align="right" | ''(95)''
|-
| width="1" align="right"|<!-- equation 96 --><math>(\exists x)\alpha\diamondsuit\beta \;\;\;\,</math>
| align="left" |<math>\equiv\;\;\; (\exists x)(\alpha\diamondsuit\beta) \,</math>
| width="5%" align="right" | ''(96)''
|-
|}
<!-- end{align} -->
gdzie <math>\diamondsuit \,</math> może być operatorem <math>\lor \,</math>, <math>\land \,</math>, <math>\rightarrow \,</math>,
<math>\leftrightarrow \,</math>, przy założeniu, że zmienna <math>x \,</math> nie występuje w
formule <math>\beta \,</math>. 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 <math>\beta \,</math> zawiera
<math>x \,</math>, 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, 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).
# Kwantyfikator szczegółowy, który jest poprzedzony kwantyfikatorami ogólnymi, z którymi związane są zmienne <math>x_1,x_2,\dots,x_m \,</math>, 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 <math>x_1,x_2,\dots,x_m \,</math>.

'''Przykład skolemizacji.''' 
Weźmy pod uwagę formułę:

<!-- equation 97 -->
:{| width="100%"
| width="95%" align="left" | <math>(\forall x)(\exists y)(P(x,y)\lor Q(y,a))\rightarrow
(\exists x)(\forall y)(P(x,b)\land\neg R(y,b))
 \,</math>
| align="right" | ''(97)''
|}
Rozpoczynamy od przemianowania zmiennych tak, aby z każdym
kwantyfikatorem związany był inny symbol zmiennej:

<!-- equation 98 -->
:{| width="100%"
| width="95%" align="left" | <math>(\forall x)(\exists y)(P(x,y)\lor Q(y,a))\rightarrow
(\exists z)(\forall v)(P(z,b)\land\neg R(v,b))
 \,</math>
| align="right" | ''(98)''
|}
Obecnie wszystkie kwantyfikatory możemy przenieść na początek formuły:

<!-- equation 99 -->
:{| width="100%"
| width="95%" align="left" | <math>(\forall x)(\exists y)(\exists z)(\forall v)
((P(x,y)\lor Q(y,a))\rightarrow (P(z,b)\land\neg R(v,b)))
 \,</math>
| align="right" | ''(99)''
|}
Kwantyfikator szczegółowy dotyczący zmiennej <math>y \,</math> występuje po
kwantyfikatorze ogólnym dla zmiennej <math>x \,</math>. Aby pominąć ten
kwantyfikator szczegółowy, wprowadzamy nowy symbol funkcyjny <math>h_1 \,</math> i
zastępujemy wszystkie wystąpienia zmiennej <math>y \,</math> przez <math>h_1(x) \,</math>.
Podobnie postępując z kolejnym kwantyfikatorem szczegółowym,
zastępujemy wszystkie wystąpienia zmiennej <math>z \,</math> przez <math>h_2(x) \,</math>, gdzie
<math>h_2 \,</math> 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:

<!-- begin{align}  TODO: kolumny-->
:{| width="100%"
| width="1" align="right"|<!-- equation 100 --><math>(\forall x)(\forall v) \,</math>
| align="left" |<math>(\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  \,</math>
| width="5%" align="right" | ''(100)''
|-
| width="1" align="right"|<!-- equation 100 -->&nbsp;
| align="left" |<math>\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))  \,</math>
| width="5%" align="right" | &nbsp;
|-
|}
<!-- end{align} -->

=== 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 [[#Postać standardowa Skolema|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 [[#Klauzule|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
[[#Koniunkcyjna postać normalna|postaci CNF]] do postaci zbioru klauzul tracimy informację, z której
pierwotnej formuły pochodzą poszczególne klauzule.  Jeśli pewna
zmienna <math>x \,</math> 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.