Sztuczna inteligencja/SI Moduł 2/Semantyka języka logiki: Różnice pomiędzy wersjami

Aktualna wersja na dzień 22:13, 11 wrz 2023

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}$ ,.

\begin{figure}[h] \includegraphics[width=6cm]{rysunki/klocki.eps} \end{figure}

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$ ,-argumentowa funkcje $I (f) : X^{m} \mapsto X$ ,.
Symbole predykatowe: $m$ ,-argumentowy symbol predykatowy $P$ , oznacza $m$ ,-argumentowa relacje $I (P) \subset X^{m}$ , (równoważnie, możemy przyjąć, że $P$ , oznacza funkcje $I (P) : X^{m} \mapsto {0, 1}$ ,).

Przypomnijmy sobie, że relacją $m$ , argumentową określoną na zbiorze $X$ , jest dowolny podzbior iloczynu kartezjanskiego $X^{m}$ ,. Dla krotki złożonej z $m$ , elementow zbioru $X$ ,, która należy do relacji, mówimy także, ż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. Z kolei symbole zmiennych wyłączone są z intepretacji - mając ustaloną interpretację, byłyby identyczne z symbolami stałych. Dopuszcza się jednak przypisywanie zmiennym znaczenia przy intepretowaniu konkretnej formuły za pomocą wartościowania. Wartościowanie jest dowolnym odwzorowaniem symboli zmiennych na elementy dziedziny - dla symbolu zmiennej $x$ , wartosciowanie $v$ , określa wartosc $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 a 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) = gora$ ,	(8)
$I (g) = dol$ ,	(9)

Funkcje te określimy następująco:

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

(jak widać, funkcja $gora$ , przypisuje każdemu klockowi jego sąsiada z góry, o ile istnieje, albo jego samego; podobnie funkcja $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) = na$ ,	(15)
$I (Q) = nad$ ,	(16)
$I (R) = rowne$ ,	(17)

przy czym:

$na$ , jest relacją dwuargumentową, do której należą wszystkie pary klocków takie, że pierwszy leży na drugim: $⟨ B, A ⟩$ ,, $⟨ C, B ⟩$ ,, $⟨ E, D ⟩$ ,,
$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): $⟨ B, A ⟩$ ,, $⟨ C, A ⟩$ ,, $⟨ C, B ⟩$ ,, $⟨ E, D ⟩$ ,,
$rowne$ , jest relacją dwuargumentową, do której należą wszystkie pary złożone z dwóch wystąpień tych samych klocków: $⟨ A, A ⟩$ ,, $⟨ B, B ⟩$ ,, $⟨ C, C ⟩$ ,, $⟨ D, D ⟩$ ,, $⟨ E, E ⟩$ ,.

Interpretacja termów

Interpretacja wraz z wartościowaniem pozwala ustalić znaczenie dowolnego termu. Dla interpretacji $I$ , i wartosciowania $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 intepretacji 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 wartosciowaniu $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)$ ,. Poniewaz $I (b) = B$ ,, $I (f) = gora$ , oraz $gora (B) = C$ ,, wiec oczywiscie $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 intepretowane są podobnie jak termy złożone: przez zastosowanie intepretacji 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 krotke $m$ , obiektów z dziedziny $⟨ I_{v} (t_{1}), I_{v} (t_{2}), \dots, I_{v} (t_{m}) ⟩ \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{jesli <math>\langle I_v(t_1),I_v(t_2),\dots,I_v(t_m)\rangle\in I(P)} ,}

0 & \textit{jesli $⟨ I_{v} (t_{1}), I_{v} (t_{2}), \dots, I_{v} (t_{m}) ⟩ \in̸ I (P)$ ,.} \end{cases} </math>, (21)

Intepretacja 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 $\to$ ,:

\begin{center}

$I_{v} (α)$ ,	$I_{v} (β)$ ,	$I_{v} (α \to β)$ ,
$0$ ,	$0$ ,	$1$ ,
$0$ ,	$1$ ,	$1$ ,
$1$ ,	$0$ ,	$0$ ,
$1$ ,	$1$ ,	$1$ ,

\end{center}

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$ ,, interpretacje $I$ , i wartosciowanie $v$ ,, rozważmy interpretację formuły postaci $(\forall x) α$ ,. Aby uniknąć wikłania się w dyskusje o zasięgu kwantyfikatorów założymy, że w formule $α$ , nie występuje żaden inny kwantyfikator dla zmiennej $x$ , (czyli że wszystkie wystąpienia zmiennej $x$ , w formule $α$ , są wolne). Wartość logiczną formuły $(\forall x) α$ , przy interpretacji $I$ , i wartosciowaniu $v$ , ustalamy w następujący sposób:

$I_{v} ((\forall x) α) = 1$ , wtedy i tylko wtedy gdy dla wszystkich wartościowań $v_{x}$ , rozniacych sie od $v$ , co najwyżej wartością przypisywaną zmiennej $x$ , (a wiec takze dla $v_{x}$ , identycznego z $v$ ,) uzyskujemy $I_{v_{x}} (α) = 1$ ,,
$I_{v} ((\forall x) α) = 0$ , w przeciwnym przypadku.

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

$I_{v} ((\exists x) α) = 1$ , wtedy i tylko wtedy gdy istnieje wartościowanie $v_{x}$ , rozniace sie od $v$ , co najwyżej wartością przypisywaną zmiennej $x$ , (moze to byc w szczegolnosci $v_{x}$ , identyczne z $v$ ,) uzyskujemy $I_{v_{x}} (α) = 1$ ,,
$I_{v} ((\exists x) α) = 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)$ , wartosciowanie $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} (α) = 1$ , dla wszystkich mozliwych wartosci 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) \to Q (x, y)$ ,. Przy ustalonej w poprzednich przykładach intepretacji 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) \to Q (x, y)) = 1$ ,. Nietrudno się przekonać, że także dla formuły $(\forall x) (\forall y) (P (x, y) \to Q (x, y))$ , uzyskamy wartość logiczną $1$ ,, sprawdzajac, ze $I_{v} (P (x, y) \to Q (x, y))$ , niezaleznie od wartosci 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) \to 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)) \to (\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 intepretacja i wartościowanie, przy których jest ona spełniona, nazywana jest formułą spełnialną. Z kolei formuła spełniona przy dowolnej intepretacji 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 intepretacji 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 intepretacji 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) \to P (e, d)$ ,	(32)
$P (x, y) \to Q (x, y)$ ,	(33)
$(\forall x) (P (f (x), x) \lor R (f (x), x)$ ,	(34)
$(\forall x) (\forall y) (P (x, y) \to Q (x, y)$ ,	(35)
$(\forall x) (\forall y) (P (x, y) \to \neg R (x, a))$ ,	(36)
$(\forall x) R (g (x), x) \to (\exists y) P (y, x)$ ,	(37)

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

$P (x, y) \to (P (x, y) \to 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 $β$ , jest konsekwencją semantyczną zbioru formuł $Γ = {α_{1}, α_{2}, \dots, α_{n}}$ ,, jeśli formuła $α_{1} \land α_{2} \land \dots \land α_{n} \to β$ , jest prawdziwa. Będziemy wówczas pisać $Γ ⊨ β$ ,.

Sztuczna inteligencja/SI Moduł 2/Semantyka języka logiki: Różnice pomiędzy wersjami

Aktualna wersja na dzień 22:13, 11 wrz 2023

Spis treści

Semantyka języka logiki

Dziedzina

Interpretacja symboli

Interpretacja termów

Interpretacja formuł

Spełnialność i prawdziwość

Konsekwencja semantyczna

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia

@@ Linia 1: / Linia 1: @@
-\maketitle
-\sloppy
-== 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 sie 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 <math>a,b,c\dots</math>.
-* '''Symbole zmiennych:'''  oznaczane za pomocą liter <math>x,y,z\dots</math>.
-* '''Symbole funkcyjne:'''  oznaczane za pomocą liter <math>f,g,h\dots</math>. każdy symbol funkcyjny ma ustaloną liczbę argumentów.
-* '''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 ==
@@ Linia 119: / Linia 22: @@
 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>.
+jest w tym przypadku zbiorem pięciu klocków <math>\{A,B,C,D,E\}</math>,.
 \begin{figure}[h]
@@ Linia 127: / Linia 30: @@
 === Interpretacja symboli ===
-Mając ustaloną pewną dziedzinę <math>X</math>, symbole alfabetu języka predykatów
+Mając ustaloną pewną dziedzinę <math>X</math>,, symbole alfabetu języka predykatów
 interpretujemy następująco.
-* '''Symbole stałych:'''  symbol stałej <math>a</math> oznacza pewien obiekt z dziedziny <math>I(a)\in X</math>.
+* '''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 symbol funkcyjny <math>f</math> oznacza <math>m</math>-argumentową funkcję <math>I(f): X^m\mapsto X</math>.
+* '''Symbole funkcyjne:'''  <math>m</math>,-argumentowy symbol funkcyjny <math>f</math>, oznacza <math>m</math>,-argumentowa funkcje <math>I(f): X^m\mapsto X</math>,.
-* '''Symbole predykatowe:'''  <math>m</math>-argumentowy 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>).
+* '''Symbole predykatowe:'''  <math>m</math>,-argumentowy symbol predykatowy <math>P</math>, oznacza <math>m</math>,-argumentowa relacje <math>I(P)\subset X^m</math>, (równoważnie, możemy przyjąć, że <math>P</math>, oznacza funkcje <math>I(P): X^m\mapsto\{0,1\}</math>,).
-Przypomnijmy sobie, że relacją <math>m</math> argumentową określoną na zbiorze
+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>. Dla krotki
+<math>X</math>, jest dowolny podzbior iloczynu kartezjanskiego <math>X^m</math>,. Dla krotki
-złożonej z <math>m</math> elementów zbioru <math>X</math>, która należy do relacji, mówimy
+złożonej z <math>m</math>, elementow zbioru <math>X</math>,, która należy do relacji, mówimy
 także, że relacja jest spełniona.
@@ Linia 147: / Linia 50: @@
 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ść $v(x)\in
+zmiennej <math>x</math>, wartosciowanie <math>v</math>, określa wartosc <math>v(x)\in X</math>,.
-X$.
 '''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
+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}
-I(a) ={}& A\\
+<!-- begin{align}  TODO: kolumny-->
-I(b) ={}& B\\
+:{| width="400"
-I(c) ={}& C\\
+|<!-- equation 1 --><math>I(a) =   A</math>, || ''(1)''
-I(d) ={}& D\\
+|-
-I(e) ={}& E
+|<!-- equation 2 --><math>I(b) =   B</math>, || ''(2)''
-\end{align}
+|-
+|<!-- equation 3 --><math>I(c) =   C</math>, || ''(3)''
+|-
+|<!-- equation 4 --><math>I(d) =   D</math>, || ''(4)''
+|-
+|<!-- equation 5 --><math>I(e) =   E</math>, || ''(5)''
+|-
+|}
+<!-- end{align} -->
 Przyjmiemy także, że a alfabecie znajdują się dwa symbole zmiennych
-<math>x</math> i <math>y</math>, dla których określono wartościowanie następująco:
+<math>x</math>, i <math>y</math>,, dla których określono wartościowanie następująco:
-\begin{align}
-v(x) ={}& C\\
+<!-- begin{align}  TODO: kolumny-->
-v(y) ={}& B
+:{| width="400"
-\end{align}
+|<!-- equation 6 --><math>v(x) =   C</math>, || ''(6)''
+|-
+|<!-- equation 7 --><math>v(y) =   B</math>, || ''(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ć
+funkcyjne <math>f</math>, i <math>g</math>,. Nasza interpretacja będzie im przypisywać
 odpowiednio dwuargumentowe funkcje określone na dziedzinie:
-\begin{align}
-I(f) ={}& \textit{góra}\\
+<!-- begin{align}  TODO: kolumny-->
-I(g) ={}& \textit{dół}
+:{| width="400"
-\end{align}
+|<!-- equation 8 --><math>I(f) =   \textit{gora}</math>, || ''(8)''
+|-
+|<!-- equation 9 --><math>I(g) =   \textit{dol}</math>, || ''(9)''
+|-
+|}
+<!-- end{align} -->
 Funkcje te określimy następująco:
-\begin{align}
-\textit{góra}(A) ={}& B & \textit{dół}(A)={}& A\\
+<!-- begin{align}  TODO: kolumny-->
-\textit{góra}(B) ={}& C & \textit{dół}(B)={}& A\\
+:{| width="400"
-\textit{góra}(C) ={}& C & \textit{dół}(C)={}& B\\
+|<!-- equation 10 --><math>\textit{gora}(A) =   \;   B   \;   \textit{dol}(A)=   \;   A</math>, || ''(10)''
-\textit{góra}(D) ={}& E & \textit{dół}(D)={}& D\\
+|-
-\textit{góra}(E) ={}& E & \textit{dół}(E)={}& D
+|<!-- equation 11 --><math>\textit{gora}(B) =   \;   C   \;   \textit{dol}(B)=   \;   A</math>, || ''(11)''
-\end{align}
+|-
-(jak widać, funkcja <math>\textit{góra}</math> przypisuje każdemu klockowi jego
+|<!-- equation 12 --><math>\textit{gora}(C) =   \;   C   \;   \textit{dol}(C)=   \;   B</math>, || ''(12)''
+|-
+|<!-- equation 13 --><math>\textit{gora}(D) =   \;   E   \;   \textit{dol}(D)=   \;   D</math>, || ''(13)''
+|-
+|<!-- equation 14 --><math>\textit{gora}(E) =   \;   E   \;   \textit{dol}(E)=   \;   D</math>, || ''(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{dół}</math> przypisuje każdemu klockowi jego sąsiada z dołu, o ile
+<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>,
+logiki zawiera dwuargumentowe symbole predykatowe <math>P</math>,, <math>Q</math>, i <math>R</math>,,
 których interpretację ustalimy następująco:
-\begin{align}
-I(P) ={}& \textit{na}\\
+<!-- begin{align}  TODO: kolumny-->
-I(Q) ={}& \textit{nad}\\
+:{| width="400"
-I(R) ={}& \textit{równe}
+|<!-- equation 15 --><math>I(P) =   \textit{na}</math>, || ''(15)''
-\end{align}
+|-
+|<!-- equation 16 --><math>I(Q) =   \textit{nad}</math>, || ''(16)''
+|-
+|<!-- equation 17 --><math>I(R) =   \textit{rowne}</math>, || ''(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: $\langle B,A\rangle<math>, </math>\langle C, B\rangle<math>, </math>\langle E,D\rangle$,
+* <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{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{równe}</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>.
+* <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 termu. Dla interpretacji <math>I</math> i wartościowania <math>v</math> oznaczmy
+dowolnego termu. Dla interpretacji <math>I</math>, i wartosciowania <math>v</math>, oznaczmy
-dla wygody przez <math>I_v</math> ich połączenie, rozumiane następująco:
+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 stałych:'''  <math>I_v(a)=I(a)</math>,,
-* '''dla symboli zmiennych:'''  <math>I_v(x)=v(x)</math>.
+* '''dla symboli zmiennych:'''  <math>I_v(x)=v(x)</math>,.
 Termy złożone interpretowane są przez zastosowanie intepretacji 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 <math>I</math> i wartościowaniu <math>v</math>, może być
+ustalonej dziedzinie, interpretacji <math>I</math>, i wartosciowaniu <math>v</math>,, może być
-wyznaczone znaczenie każdego termu postaci <math>f(t_1,t_2,\dots,t_m)</math> w
+wyznaczone znaczenie każdego termu postaci <math>f(t_1,t_2,\dots,t_m)</math>, w
 następujący sposób:
-<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)).
+<!-- equation 18 -->
-</math>
+:<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>, ''(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{góra}</math>
+Weźmy pod uwagę term <math>f(b)</math>,. Poniewaz <math>I(b)=B</math>,, <math>I(f)=\textit{gora}</math>,
-oraz <math>\textit{góra}(B)=C</math>, więc oczywiście <math>I(f(b))=C</math>. Podobnie łatwo
+oraz <math>\textit{gora}(B)=C</math>,, wiec oczywiscie <math>I(f(b))=C</math>,. Podobnie łatwo
 można sprawdzić interpretację następujących termów:
-\begin{align}
-I_v(f(x)) ={}& C\\
+<!-- begin{align}  TODO: kolumny-->
-I_v(g(y)) ={}& A
+:{| width="400"
-\end{align}
+|<!-- equation 19 --><math>I_v(f(x)) =   C</math>, || ''(19)''
+|-
+|<!-- equation 20 --><math>I_v(g(y)) =   A</math>, || ''(20)''
+|-
+|}
+<!-- end{align} -->
 === Interpretacja formuł ===
@@ Linia 230: / Linia 184: @@
 Formuły atomowe intepretowane są podobnie jak termy złożone: przez
 zastosowanie intepretacji 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
+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
+ten sposób relację <math>I(P)</math>, oraz krotke <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
+<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:
-<math>
+<!-- equation 21 -->
+:<math>
 I_v(P(t_1,t_2,\dots,t_m)) =
 \begin{cases}
 &
-\text{jeśli <math>\langle I_v(t_1),I_v(t_2),\dots,I_v(t_m)\rangle\in I(P)</math>}\\
+\textit{jesli <math>\langle I_v(t_1),I_v(t_2),\dots,I_v(t_m)\rangle\in I(P)</math>,}
 &
-\text{jeśli <math>\langle I_v(t_1),I_v(t_2),\dots,I_v(t_m)\rangle\not\in I(P)</math>.}
+\textit{jesli <math>\langle I_v(t_1),I_v(t_2),\dots,I_v(t_m)\rangle\not\in I(P)</math>,.}
 \end{cases}
-</math>
+</math>, ''(21)''
 Intepretacja formuł złożonych polega na przypisaniu wartości logicznej
 formułom uzyskanym przez zastosowanie operatorów logicznych,
@@ Linia 250: / Linia 208: @@
 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>:
+<math>\rightarrow</math>,:
 \begin{center}
-\begin{tabular}{c|c||c}
-<math>I_v(\alpha)</math> & <math>I_v(\beta)</math> & <math>I_v(\alpha\rightarrow\beta)</math>\\
+<!-- \begin{tabular}{c|c||c} -->
-\hline
+:{| width="400" border="1"
-<math>0</math> & <math>0</math> & <math>1</math>\\
+|<math>I_v(\alpha)</math>,  ||  <math>I_v(\beta)</math>,  ||  <math>I_v(\alpha\rightarrow\beta)</math>,
-<math>0</math> & <math>1</math> & <math>1</math>\\
+|-
-<math>1</math> & <math>0</math> & <math>0</math>\\
+|<math>0</math>,  ||  <math>0</math>,  ||  <math>1</math>,
-<math>1</math> & <math>1</math> & <math>1</math>
+|-
-\end{tabular}
+|<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}
@@ Linia 268: / Linia 235: @@
 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ę
+<math>X</math>,, interpretacje <math>I</math>, i wartosciowanie <math>v</math>,, rozważmy interpretację
-formuły postaci <math>(\forall x)\alpha</math>. Aby uniknąć wikłania się w
+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
+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
+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ą
+wszystkie wystąpienia zmiennej <math>x</math>, w formule <math>\alpha</math>, są
-''wolne''). Wartość logiczną formuły <math>(\forall x)\alpha</math> przy
+''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:
+interpretacji <math>I</math>, i wartosciowaniu <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)=1</math>, wtedy i tylko wtedy gdy dla wszystkich wartościowań <math>v_x</math>, rozniacych sie od <math>v</math>, co najwyżej wartością przypisywaną zmiennej <math>x</math>, (a wiec takze 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.
+# <math>I_v((\forall x)\alpha)=0</math>, w przeciwnym przypadku.
-Analogicznie dla formuły <math>(exists x)\alpha</math>:
+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)=1</math>, wtedy i tylko wtedy gdy istnieje wartościowanie <math>v_x</math>, rozniace sie od <math>v</math>, co najwyżej wartością przypisywaną zmiennej <math>x</math>, (moze to byc w szczegolnosci <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.
+# <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
+wartość <math>v(x)</math>, wartosciowanie <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
+<math>I_v(\alpha)=1</math>, dla wszystkich mozliwych wartosci 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
+wartości zmiennej <math>x</math>, (w przypadku kwantyfikatora szczegółowego) z
-dziedziny <math>X</math>.
+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
+Weźmy pod uwagę formułę <math>P(x,y)\rightarrow Q(x,y)</math>,. Przy ustalonej w
 poprzednich przykładach intepretacji i wartościowaniu dostajemy:
-\begin{align}
-I_v(P(x,y)) ={}& 1\\
+<!-- begin{align}  TODO: kolumny-->
-I_v(Q(x,y)) ={}& 1
+:{| width="400"
-\end{align}
+|<!-- equation 22 --><math>I_v(P(x,y)) =   1</math>, || ''(22)''
-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>
+|<!-- equation 23 --><math>I_v(Q(x,y)) =   1</math>, || ''(23)''
-uzyskamy wartość logiczną <math>1</math>, sprawdzając, że $I_v(P(x,y)\rightarrow
+|-
-Q(x,y))<math> niezależnie od wartości przypisanych zmiennym </math>x<math> i </math>y$.
+|}
+<!-- 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>,, sprawdzajac, ze <math>I_v(P(x,y)\rightarrow Q(x,y))</math>, niezaleznie od wartosci 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:<math>
+* 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))</math>
+<!-- equation 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.<math>
+:<math>
- (\forall x)(\forall y)\neg(P(x,y)\land P(y,x))</math>
+(\forall x)(\forall y) P(x,y)\rightarrow R(x,f(y))
-* Każdy klocek, który nie ma górnego sąsiada, jest dolnym sąsiadem jakiegoś innego klocka.<math>
+</math>, ''(24)''
- (\forall x) R(x,f(x)) \rightarrow (\exists y) R(x,g(y))</math>
+* 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 -->
+:<math>
+(\forall x)(\forall y)\neg(P(x,y)\land P(y,x))
+</math>, ''(25)''
+* Każdy klocek, który nie ma górnego sąsiada, jest dolnym sąsiadem jakiegoś innego klocka.
+<!-- equation 26 -->
+:<math>
+(\forall x) R(x,f(x)) \rightarrow (\exists y) R(x,g(y))
+</math>, ''(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
+logiczną <math>1</math>,, nazywa się formułą ''spełnioną'' przy tej
 interpretacji i wartościowaniu. Formuła, dla której istnieje
 intepretacja i wartościowanie, przy których jest ona spełniona,
@@ Linia 327: / Linia 315: @@
 Dla formuły, która nie jest prawdziwa, istnieje interpretacja i
-wartościowanie, przy których jej wartość logiczna wynosi <math>0</math>. Taką
+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
+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''.
@@ Linia 345: / Linia 333: @@
 Łatwo sprawdzić, że następujące formuły są spełnione przy intepretacji
 i wartościowaniu określonych w poprzednich przykładach:
-\begin{align}
-& \neg P(y,x)\\
+<!-- begin{align}  TODO: kolumny-->
-& \neg P(b,a)\lor Q(e,d)\\
+:{| width="400"
-& P(f(x),b)\\
+|<!-- equation 27 --><math> \neg P(y,x)</math>, || ''(27)''
-& Q(f(x),y)\\
+|-
-& P(x,y)\land Q(x,a)\\
+|<!-- equation 28 --><math> \neg P(b,a)\lor Q(e,d)</math>, || ''(28)''
-& P(x,y) \rightarrow P(e,d)\\
+|-
-& P(x,y)\rightarrow Q(x,y)\\
+|<!-- equation 29 --><math> P(f(x),b)</math>, || ''(29)''
-& (\forall x) (P(f(x),x)\lor R(f(x),x)\\
+|-
-& (\forall x)(\forall y) (P(x,y)\rightarrow Q(x,y)\\
+|<!-- equation 30 --><math> Q(f(x),y)</math>, || ''(30)''
-& (\forall x)(\forall y) (P(x,y)\rightarrow \neg R(x,a))\\
+|-
-& (\forall x) R(g(x),x)\rightarrow (\exists y) P(y,x)
+|<!-- equation 31 --><math> P(x,y)\land Q(x,a)</math>, || ''(31)''
-\end{align}
+|-
+|<!-- equation 32 --><math> P(x,y) \rightarrow P(e,d)</math>, || ''(32)''
+|-
+|<!-- equation 33 --><math> P(x,y)\rightarrow Q(x,y)</math>, || ''(33)''
+|-
+|<!-- equation 34 --><math> (\forall x) (P(f(x),x)\lor R(f(x),x)</math>, || ''(34)''
+|-
+|<!-- equation 35 --><math> (\forall x)(\forall y) (P(x,y)\rightarrow Q(x,y)</math>, || ''(35)''
+|-
+|<!-- equation 36 --><math> (\forall x)(\forall y) (P(x,y)\rightarrow \neg R(x,a))</math>, || ''(36)''
+|-
+|<!-- equation 37 --><math> (\forall x) R(g(x),x)\rightarrow (\exists y) P(y,x)</math>, || ''(37)''
+|-
+|}
+<!-- end{align} -->
 Następujące formuły są także prawdziwe:
-\begin{align}
-P(x,y)\rightarrow (P(x,y)\rightarrow Q(x,y))\\
+<!-- begin{align}  TODO: kolumny-->
-P(a,e)\lor\neg P(a,e)
+:{| width="400"
-\end{align}
+|<!-- equation 38 --><math>P(x,y)\rightarrow (P(x,y)\rightarrow Q(x,y))</math>, || ''(38)''
+|-
+|<!-- equation 39 --><math>P(a,e)\lor\neg P(a,e)</math>, || ''(39)''
+|-
+|}
+<!-- end{align} -->
 === Konsekwencja semantyczna ===
@@ Linia 371: / Linia 382: @@
 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
-<math>\beta</math> jest konsekwencją semantyczną zbioru formuł
+<math>\beta</math>, jest konsekwencją semantyczną zbioru formuł
-<math>\Gamma=\{\alpha_1,\alpha_2,\dots,\alpha_n\}</math>, jeśli formuła
+<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
+<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>.
+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}
-& \alpha\lor\neg\alpha
-& \alpha\rightarrow(\beta\rightarrow\alpha)\\
-& (\alpha\rightarrow(\beta\rightarrow\gamma))\rightarrow
-((\alpha\rightarrow\beta)\rightarrow(\alpha\rightarrow\gamma))
-\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:
-<math>
-\frac{\alpha_1\;\alpha_2\;\dots.\;\alpha_n}{\beta}
-</math>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.
-<math>
-\frac{\alpha\rightarrow\beta,\;\alpha}{\beta}
-\label{eq:modusponens}
-</math>
-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.
-<math>
-\frac{\alpha\rightarrow\beta,\;\neg\beta}{\neg\alpha}
-\label{eq:modustollens}
-</math>
-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.
-<math>
-\frac{\alpha\lor\beta,\;\neg\beta}{\alpha}
-\label{eq:alternatywa}
-</math>
-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.
-<math>
-\frac{\alpha_1,\;\alpha_2,\;\dots,\;\alpha_n}
-{\alpha_1\land\alpha_2\land\dots\land\alpha_n}
-\label{eq:koniunkcja1}
-</math>
-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.
-<math>
-\frac{\alpha_1\land\alpha_2,\land\dots\land\alpha_n}
-{\alpha_1,\;\alpha_2,\;\dots,\;\alpha_n}
-\label{eq:koniunkcja2}
-</math>
-Powyższa reguła jest regułą odwrotną do poprzedniej - z koniunkcji
-generuje zbiór formuł będących członami tej koniunkcji.
-<math>
-\frac{(\forall x)\alpha}{\alpha[x/t]}
-\label{eq:specjalizacja}
-</math>
-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}
-& (\forall x) R(x,x)\label{eq:bw1}\\
-& (\forall x)(\forall y) ((R(x,y)\rightarrow R(y,x))
-\land((R(y,x)\rightarrow R(x,y))))\label{eq:bw2}\\
-& (\forall x) (P(x,g(x))\lor R(x,g(x)))\label{eq:bw3}\\
-& (\forall x) (P(f(x),x)\lor R(f(x),x))\label{eq:bw4}\\
-& (\forall x)(\forall y) (P(x,y)\rightarrow Q(x,y))\label{eq:bw5}\\
-& (\forall x)(\forall y) (Q(x,y)\rightarrow Q(f(x),y))\label{eq:bw6}\\
-& (\forall x)(\forall y) (Q(x,y)\rightarrow Q(x,g(y)))\label{eq:bw7}\\
-& \neg R(a,f(a))\label{eq:bw8}\\
-& \neg R(b,f(b))\label{eq:bw9}\\
-& R(c,f(c))\label{eq:bw10}\\
-& \neg R(d,f(d))\label{eq:bw11}\\
-& R(d,f(e))\label{eq:bw12}\\
-& R(a,g(a))\label{eq:bw13}\\
-& \neg R(b,g(b))\label{eq:bw14}\\
-& \neg R(c,g(c))\label{eq:bw15}\\
-& R(d,g(d))\label{eq:bw16}\\
-& \neg R(e,g(e))\label{eq:bw17}
-\end{align}
-(Zauważmy, że wszystkie te formuły są spełnione w dziedzinie świata
-klocków, przy intepretacji i wartościowaniu opisanych w poprzednich
-przykładach.)  Poszukamy dowodu formuły <math>Q(f(f(a)),a)</math>.
-# Stosując (dwukrotnie) regułę specjalizacji (\ref{eq:specjalizacja}) do formuły (\ref{eq:bw2}) 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:<math>
- (R(a,f(a))\rightarrow R(f(a),a)) \land((R(f(a),a)\rightarrow R(a,f(a))))</math>
-# Do formuły uzyskanej w poprzednim kroku stosujemy regułę koniunkcji (\ref{eq:koniunkcja2}), otrzymując w ten sposób dwie formuły: \begin{align} & R(a,f(a))\rightarrow R(f(a),a)\\ & R(f(a),a)\rightarrow R(a,f(a)) \end{align}
-# Do drugiej z otrzymanych w poprzednim kroku formuł oraz do formuły (\ref{eq:bw8}) stosujemy obecnie regułę ''modus tollens'' (\ref{eq:modustollens}), co daje w wyniku:<math>
- \neg R(f(a),a) \label{eq:d1}</math>
-# Stosując regułę specjalizacji (\ref{eq:specjalizacja}) do formuły (\ref{eq:bw4}) z podstawieniem stałej <math>a</math> w miejsce zmiennej <math>x</math> dostajemy:<math>
- P(f(a),a)\lor R(f(a),a) \label{eq:d2}</math>
-# Stosując regułę wnioskowania (\ref{eq:alternatywa}) do formuł uzyskanych w dwóch poprzednich krokach (\ref{eq:d2}) i (\ref{eq:d1}) wyprowadzamy:<math>
- P(f(a),a) \label{eq:d3}</math>
-# Stosując regułę specjalizacji (\ref{eq:specjalizacja}) do formuły (\ref{eq:bw5}) 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:<math>
- P(f(a),a)\rightarrow Q(f(a),a) \label{eq:d4}</math>
-# Przez zastosowanie reguły ''modus ponens'' (\ref{eq:modusponens}) do formuł uzyskanych w dwóch poprzednich krokach dowodu (\ref{eq:d4}) i (\ref{eq:d3}) wyprowadzamy formułę:<math>
- Q(f(a),a) \label{eq:d5}</math>
-# Stosując regułę specjalizacji (\ref{eq:specjalizacja}) do formuły (\ref{eq:bw6}) 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:<math>
- Q(f(a),a)\rightarrow Q(f(f(a)),a) \label{eq:d6}</math>
-# Wreszcie zastosowanie reguły ''modus ponens'' (\ref{eq:modusponens}) do formuł wyprowadzonych w dwóch poprzednich krokach (\ref{eq:d6}) i (\ref{eq:d5}) pozwala wygenerować poszukiwaną formułę docelową <math>Q(f(f(a)),a)</math>, która tym samym została udowodniona.
-Zauważmy, że udowodniona formuła jest spełniona w świecie klocków.  W
-procesie wnioskowania były stosowane tylko niektóre formuły wchodzące
-w skład bazy wiedzy. Nietrudno się przekonać, że jej zawartość
-umożliwia wyprowadzenie wielu innych formuł, także spełnionych w
-świecie klocków.
-=== Konsekwencja syntaktyczna ===
-Dla danego systemu wnioskowania można zdefiniować relację konsekwencji
-syntatycznej jako relację wyprowadzalności formuły z pewnej bazy
-wiedzy za pomocą tego systemu. Powiemy, że formuła <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ów wnioskowania dla ustalonego języka
-logiki. Każdy z nich określa pewien mechanizm generowania nowych
-formuł ze znanych formuł. Nie każdy z nich jednak jest przydatny do
-rozstrzygania o prawdziwości i fałszywości. Przydatny system
-wnioskowania powinien być poprawny i pełny.
-W uproszczeniu, system wnioskowania jest nazywany poprawnym wtedy, gdy
-wyprowadzalność formuły w tym systemie pociąga za sobą jej
-prawdziwość. Z kolei dla systemu pełnego zachowana jest właściwość
-odwrotna: każda prawdziwa formuła może być w tym systemie
-wyprowadzona. W obu przypadkach mówimy tu o wyprowadzalności z pustej
-początkowej bazy wiedzy (wyłącznie z wykorzystaniem aksjomatów systemu
-wnioskowania).
-Bardziej ogólnie i precyzyjnie powinniśmy raczej definiować poprawność
-i pełność odwołując się do relacji konsenwencji syntaktycznej i
-semantycznej. Powiemy, że system wnioskowania jest poprawny, gdy dla
-dowolnego zbioru formuł <math>\Gamma</math> oraz dowolnej formuły <math>\alpha</math>, jeśli
-<math>\alpha</math> jest konsenwencją syntaktyczną <math>\Gamma</math>, to <math>\alpha</math> jest
-także konsenwencją 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 konsenwencją semantyczną <math>\Gamma</math>, to
-<math>\alpha</math> jest także konsenwencją syntaktyczną <math>\Gamma</math>.
-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
-<math>
-\frac{\alpha_1\;\alpha_2\;\dots.\;\alpha_n}{\beta}
-</math>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 \emph{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 ===
-Przed podstawienie w ogólnym przypadku rozumiemy zbiór wiązań
-zmiennych, z których każde określa term podstawiany za jedną zmienną.
-Wiązanie przypisujące term <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:
-<math>
-P(x,y) \rightarrow Q(x,b)\lor R(a,y)
-</math>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:
-<math>
-P(a,f(b))\rightarrow Q(a,b)\lor R(a,f(b))
-</math>
-=== 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ł <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}
-& P(x,f(y)) \land \neg Q(y,b) \rightarrow R(g(a),z)\lor P(f(x),c)\\
-& P(b,v) \land \neg Q(d,b) \rightarrow R(w,g(c))\lor P(f(b),c)
-\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
-pozytywny, 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<math>, gdzie </math>L_0$ 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 $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łę (\ref{eq:koniunkcja2})
-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}
-\alpha\leftrightarrow\beta \;\;\;&\equiv\;\;\;
-(\alpha\rightarrow\beta)\land(\beta\rightarrow\alpha)\\
-\alpha\rightarrow\beta \;\;\;&\equiv\;\;\; \neg\alpha\lor\beta\\
-\neg(\neg\alpha) \;\;\;&\equiv\;\;\; \alpha\\
-\neg(\alpha\lor\beta) \;\;\;&\equiv\;\;\; \neg\alpha\land\neg\beta\\
-\neg(\alpha\land\beta) \;\;\;&\equiv\;\;\; \neg\alpha\lor\neg\beta\\
-\alpha\lor(\beta\land\gamma) \;\;\;&\equiv\;\;\;
-(\alpha\lor\beta)\land(\alpha\lor\gamma)\\
-\alpha\land(\beta\lor\gamma) \;\;\;&\equiv\;\;\;
-(\alpha\land\beta)\lor(\alpha\land\gamma)
-\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}
-& P(x,y)\lor Q(y,a)\rightarrow P(z,b)\land \neg R(v,b)\\
-& \neg(P(x,y)\lor Q(y,a)) \lor (P(z,b)\land \neg R(v,b))\\
-& \neg(P(x,y)\land\neg Q(y,a)) \lor (P(z,b)\land \neg R(v,b))\\
-& (\neg P(x,y)\lor P(z,b))\land(\neg P(x,y)\lor R(v,b))\land\nonumber\\
-& \;\;\;\;\;\land (\neg Q(y,a)\lor P(z,b))\land(\neg Q(y,a)\lor R(v,b))
-\end{align}
-=== 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
-<math>
-(\forall\dots)(\forall\dots)\dots(\forall\dots)\alpha.
-</math>
-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
-ogólnych. 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}
-\neg (\forall x)\alpha \;\;\;&\equiv\;\;\; (\exists x)\alpha\\
-\neg (\exists x)\alpha \;\;\;&\equiv\;\;\; (\forall x)\alpha\\
-(\forall x)\alpha\diamond\beta \;\;\;&\equiv\;\;\; (\forall x)(\alpha\diamond\beta)\\
-(\exists x)\alpha\diamond\beta \;\;\;&\equiv\;\;\; (\exists x)(\alpha\diamond\beta)\\
-\end{align}
-gdzie <math>\diamond</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, usywamy, 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łę:
-<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>Rozpoczynamy od przemianowania zmiennych tak, aby z każdym
-kwantyfikatorem związany był inny symbol zmiennej:
-<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>Obecnie wszystkie kwantyfikatory możemy przenieść na początek formuły:
-<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>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:
-<math>
-\begin{split}
-& (\forall x)(\forall v) (\neg P(x,h_1(x))\lor P(h_2(x),b))
-\land(\neg P(x,h_1(x))\lor R(v,b))\land\\
-& \phantom{(\forall x)(\forall y)}
-\land (\neg Q(h_1(x),a)\lor P(h_2(x),b))\land(\neg Q(h_1(x),a)\lor R(v,b))
-\end{split}
-</math>
-=== 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 <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
-klaulach. 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.