Agent wnioskujący

Baza wiedzy (knowledge base): Zbiór faktów o świecie. Fakty te, zwane zdaniami lub formułami, zapisane są w języku reprezentacji wiedzy. Agent komunikuje się z bazą wiedzy (KB), używając operacji TELL i ASK:

• TELL: Agent → KB – dodanie obserwacji do KB.

• ASK: KB → Agent – pytanie o akcję.

Ogólny model agenta posługującego się bazą wiedzy:

82

Reprezentacja, wnioskowanie i logika

Reprezentacja wiedzy (knowledge representation: Dziedzina SI zajmująca się metodami reprezentowania wiedzy o świecie.

Język reprezentacji wiedzy tworzą:

• Syntaktyka — opisuje budowę zdań.

• Semantyka — opisuje związek pomiędzy zdaniami i odpowiadającymi im faktami zachodzącymi w świecie.

Wnioskowanie: proces wyprowadzania nowych zdań ze zdań przyjętych jako prawdziwe (tzn. reprezentujących prawdziwe fakty). Poprawne wnioskowanie powinno zapewniać prawdziwość wyprowadzonych zdań.

Model dla zbioru zdań X: każdy świat w którym prawdziwe są wszystkie zdania ze zbioru X.

Wynikanie (entailment): Zdanie A wynika ze zbioru zdań X, X ⊧ A, jeśli A jest prawdziwe w każdym modelu dla X.

Wyprowadzalność (derivability): Zdanie A jest wyprowadzalne ze zbioru zdań X przy użyciu procedury dowodzenia Π, X ⊢_{Π} A, wtw gdy Π znajduje dowód zdania A ze zdań zbioru X.

Poprawność procedury dowodzenia: Procedura dowodzenia Π jest poprawna wtw gdy dla każdego zbioru zdań X i każdego zdania A, X ⊢_{Π} A pociąga X ⊧ A.

Pełność procedury dowodzenia: Procedura dowodzenia Π jest pełna wtw gdy dla każdego zbioru zdań X i każdego zdania A, X ⊧ A pociąga X ⊢_{Π} A.

Logika: Język reprezentacji wiedzy (syntaktyka, semantyka) oraz procedura dowodzenia.

Reguła wnioskowania: \frac{α_{1},...α_{n}}{β}. Reguła jest poprawna, jeśli β jest prawdziwa w każdej interpretacji, w której prawdziwe są α_{1}, … α_{n}.

Przykłady poprawnych reguł wnioskowania

Reguła odrywania (modus ponens): \frac{α, α⇒β}{β}.

Reguła eliminacji koniunkcji: \frac{α_{1} ∧···∧ α_{n}}{α_{i}} Reguła wprowadzenia koniunkcji: \frac{α_{1}, ..., α_{n}}{α_{1} ∧···∧ α_{n}}

Reguła rezolucji: \frac{α∨β, ¬β∨γ}{α∨γ}.

Poprawność reguły rezolucji (\frac{α∨β, ¬β∨γ}{α∨γ}):

Monotoniczność: Jeśli formuła A wynika ze zbioru formuł X, to A wynika również z każdego nadzbioru zbioru X.

Złożoność rachunku zdań: Problem stwierdzenia, czy formuła jest tautologią jest NP-zupełny.

Procedury dowodzenia w logice pierwszego

rzędu

Podstawienie: Zbiór postaci

{x_{1}/t_{1}, … x_{n}/t_{n}} (1)

gdzie x_{1}, …, x_{n} są różnymi zmiennymi, natomiast t_{1}, … t_{n} są termami. Dopuszczamy podstawienie puste, oznaczane ϵ.

Niech θ będzie podstawieniem postaci (1) i niech α będzie wyrażeniem (tzn. formułą lub termem). Piszemy αθ na oznaczenie wyrażenia powstałego z α w wyniku jednoczesnego zastąpienia wszystkich wolnych wystąpień zmiennych x_{1}, …, x_{n} termami t_{1}, … t_{n}. Na przykład, jeśli θ = {x/Sam, y/P am}, to

(Likes(x, y))θ = Likes(Sam, P am).

Literał: Formuła atomowa lub negacja formuły atomowej. Zdanie: Formuła bez zmiennych wolnych. Reguła: Zdanie postaci

∀x⃗ (L_{1} ∧ ⋯ ∧ L_{n−1} ⇒ L_{n}) gdzie L_{1}, …, L_{n} (n > 1) są literałami różnymi od T rue i F alse. Zakładamy, że każda formuła bazy wiedzy jest albo regułą, albo formułą postaci ∀x⃗ L, gdzie L jest literałem. Powyższe założenie pozwala opuścić kwantyfikatory (uniwersalne).

Uogólniona reguła odrywania:

\frac{L′_{1}, …, L′_{n−1}, (L_{1} ∧ ⋯ ∧ L_{n−1} ⇒ L_{n})}{(L_{n})θ}

gdzie L′_{1}, …, L′_{n−1}, L_{1}, … L_{n} są literałami, natomiast θ jest podstawieniem takim, że dla każdego i ∈ {1, …, n−1}, (L′_{i})θ = (L_{i})θ.

Złożeniem podstawień θ_{1}, θ_{2} jest podstawienie, oznaczane θ_{1}θ_{2}, którego efekt sprowadza się do kolejnego wykonania θ_{1} i θ_{2}. Zatem:

Eθ_{1}θ_{2} = (Eθ_{1})θ_{2}.

Podstawienie θ jest unifikatorem wyrażeń E_{1}, …, E_{n} jeśli E_{1}θ =E_{2}θ = ⋯ = E_{n}θ.

Podstawienie {x/a} jest unifikatorem wyrażeń P (x), P (a). Wyrażenia P (x), Q(b) nie są unifikowalne.

Podstawienie θ jest najogólniejszym unifikatorem wyrażeń E_{1}, …, E_{n}, jeśli dla każdego unifikatora tych wyrażeń, γ, istnieje podstawienie λ takie, że γ = θλ.

Wyrażenia P (John, x), P (y, z) posiadają nieskończenie wiele unifikatorów:

{y/John, x/z}, {y/John, x/z, w/F reda}, {y/John, x/John, z/John} . . ..

Najogólniejszy unifikator – {y/John, x/z}.

Problem unifikacji: Stwierdzić, czy dane wyrażenia E_{1}, …, E_{n} są unifikowalne. Jeśli tak, znaleźć ich najogólniejszy unifikator.

Problem unifikacji jest rozstrzygalny.

Zakładamy, że mamy funkcję UNIF Y, która dla zadanych wyrażeń E_{1}, …, E_{n}, zwraca ich najogólniejszy unifikator θ lub specjalną stałą fail, jeśli unifikator nie istnieje.

Wariant (renaming) — Formuła A jest wariantem formuły B, jeśli A można otrzymać z B, zastępując niektóre zmienne, zmiennymi nie występującymi w B.

Likes(x, John) jest wariantem Likes(y, John). Likes(x, x) nie jest wariantem Likes(x, y).

Formuły naszej bazy wiedzy są takiej postaci, że każda może być zastąpiona swoim wariantem. (Powstała w ten sposób nowa baza wiedzy będzie równoważna starej.)

Dlaczego należy przemianowywać zmienne?

Knows(x, Elizabeth).

Knows(John, x) ⇒ Hates(John, x).

Powinniśmy, stosując ogólną regułę odrywania, wywnioskować Hates(John, Elizabeth). Niestety jest to niemożliwe: formuły Knows(John, x) i Knows(x, Elizabeth) nie są unifikowalne. Jeśli przemianujemy zmienne w jednej z formuł, np. formułę Knows(x, Elizabeth) zastąpimy przez Knows(y, Elizabeth), będziemy mogli wyprowadzić Hates(John, Elizabeth).

Możemy założyć: Przesłanki uogólnionej reguły odrywania nie zawierają wspólnych zmiennych.

Procedury dowodzenia oparte na uogólnionej

regule odrywania

Metoda progresywna (Forward-chaining). Stosujemy, kiedy nowy fakt p zostaje dodany do bazy wiedzy KB. Procedura znajduje nowe fakty, które wynikają z KB ∪ {p}.

Metoda regresywna (Backward-chaining). Stosujemy, kiedy chcemy otrzymać odpowiedź na pytanie zadane bazie wiedzy.

Przykład: Dowieść, że Criminal(W est).

American(x) ∧ W eapon(y) ∧ Nation(z)∧

Hostile(z)∧Sells(x, z, y)⇒Criminal(x).  (1)
Owns(Nono, M1).  (2)
Missile(M1).  (3)
Owns(Nono, x) ∧ Missile(x) ⇒ Sells(W est, Nono, x).  (4)
Missile(x) ⇒ W eapon(x).  (5)
Enemy(x, America) ⇒ Hostile(x).  (6)
American(W est).  (7)
Nation(Nono).  (8)
Enemy(Nono, America).  (9)
Nation(America).  (10)

98

Metody wnioskowania oparte na uogólnionej regule odrywania są niepełne.

∀x P (x) ⇒ Q(x).

∀x ¬P (x) ⇒ R(x).

∀x Q(x) ⇒ S(x).

∀x R(x) ⇒ S(x).

T (a).

Z powyższych formuł wynika S(a). (S(a) jest prawdziwa jeśli Q(a) lub R(a) jest prawdziwa, a jedna z tych formuł musi być prawdziwa, ponieważ P (a) jest prawdziwa lub ¬P (a) jest prawdziwa.) Niestety formuły S(a) nie można wyprowadzić ani metodą progresywną ani regresywną.

Metoda rezolucji

Metoda rezolucji (Robinson, 1965) jest pełną (i stosunkowo efektywną) procedurą dowodzenia twierdzeń w logice pierwszego rzędu.

Problem dowodzenia twierdzeń: Dla danej bazy wiedzy KB i danej formuły α stwierdzić, czy KB ⊧ α. (Problem półrozstrzygalny.)

Problem dowodzenia twierdzeń jest równoważny problemowi spełnialności: Dla danej bazy wiedzy KB i danej formuły α stwierdzić, czy zbiór KB ∪ {¬α} jest niespełnialny.

Ponieważ bazy wiedzy są skończone, KB ∪ {¬α} można zawsze traktować jako pojedynczą formułę.

Metoda rezolucji dla danej formuły β próbuje stwierdzić, czy β jest niespełnialna.

Metodę rezolucji stosuje się dla formuł w postaci klauzulowej. Klauzula – formuła postaci

l_{1} ∨ ⋯ ∨ l_{n} (n ≥ 0) (11) gdzie l_{1}, …, l_{n} są literałami. Jeśli n = 0, klauzulę (11) nazywamy klauzulą pustą i oznaczamy symbolem ⊥. Postać klauzulowa:

∀ x_{1} C_{1} ∧ ⋯ ∧ ∀ x_{m} C_{m} (m ≥ 1) gdzie C_{1}, …, C_{n} są klauzulami, natomiast x_{i} jest listą wszystkich zmiennych występujących w C_{i}.

Twierdzenie Istnieje algorytm, który dla dowolnej formuły A znajduje formułę B taką, że:

(1) B jest w postaci klauzulowej.

(2) A jest spełnialna wtw gdy B jest spełnialna. (A i B nie muszą być równoważne.)

Sprowadzanie formuły A do postaci klauzulowej

1. Niech x będzie listą wszystkich zmiennych wolnych występujących w A. Zastępujemy A formułą ∃ x A.

2. Eliminujemy wszystkie redundantne kwantyfikatory, tzn. każdy kwantyfikator postaci ∀x lub ∃x taki, że zmienna x nie występuje w obrębie działania tego kwantyfikatora.

3. Przemianowujemy zmienne tak, aby wszystkie kwantyfikowane zmienne były różne.

4. Eliminujemy “⇒” i “⇔”, zastępując B ⇒ C przez ¬B ∨ C i B ⇔ C przez ((¬B ∨ C) ∧ (¬C ∨ B)).

5. Przesuwamy “¬” w prawo, zastępując ¬∀xB przez ∃x ¬B, ¬∃x B przez ∀x ¬B, ¬(B ∨ C) przez ¬B ∧ ¬C, ¬(B ∧ C) przez ¬B ∨ ¬C, ¬¬B przez B, tak długo aż wszystkie symbole negacji występują bezpośrednio przed formułami atomowymi.

6. (Krok opcjonalny. Poniżej Q oznacza ∀ lub ∃; ♢ oznacza ∧ lub ∨.) Przesuwamy kwantyfikatory w prawo, zastępując Qx(B♢C) przez B♢(QxC), jeśli x nie jest wolna w B, i przez (QxB)♢C, jeśli x nie jest wolna w C.

7. Skolemizacja (Usunięcie kwantyfikatorów egzystencjalnych). Powtarzamy poniższy proces, aż wszystkie kwantyfikatory ∃ zostaną usunięte.

Bierzemy dowolną podformułę postaci ∃y B(y). Niech x_{1}, …, x_{n} (n ≥ 0) będzie listą wszystkich zmiennych wolnych występujących w ∃y B(y), które są uniwersalnie kwantyfikowane w pewnej nadformule formuły ∃y B(y). Jeśli n = 0, zastępujemy ∃y B(y) przez B(A), gdzie A jest nową stałą indywiduową. Jeśli n > 0, zastępujemy ∃y B(y) przez B(F (x_{1}, …, x_{n})), gdzie F jest nowym symbolem funkcji n-argumentowej.

8. Usuwamy wszystkie kwantyfikatory uniwersalne.

9. Rozdzielamy ∧ względem ∨, zastępując (B ∧ C) ∨ D przez (B ∨ D) ∧ (C ∨ D) oraz B ∨ (C ∧ D) przez (B ∨ C) ∧ (B ∨ D).

10. Eliminujemy stałe T rue i F alse. Aktualna formuła jest koniunkcją klauzul. Usuwamy każdą klauzulę zawierającą literał T rue. Z pozostałych klauzul usuwamy każdy literał F alse.

11. Dodajemy kwantyfikatory uniwersalne. Aktualna formuła jest postaci C_{1} ∧ ⋯ ∧ C_{k}, gdzie C_{1}, …, C_{k} są klauzulami. Zastępujemy ją formułą ∀ x_{1} C_{1} ∧ ⋯ ∧ ∀ x_{k} C_{k}, gdzie x_{i} jest listą wszystkich zmiennych występujących w C_{i}.

Uwaga: Kroki 1 i 7 nie zachowują równoważności. (Zachowują spełnialność.)

Formułę w postaci klauzulowej

∀ x_{1} C_{1} ∧ ⋯ ∧ ∀ x_{m} C_{m} możemy zapisać jako zbiór klauzul, tzn. w postaci {C_{1}, …, C_{m}}. Możemy też zawsze opuścić kwantyfikatory. Piszemy l_{1}, …, l_{n} ∈ C, aby wyrazić fakt, że literały l_{1}, …, l_{n} występują w klauzuli C. Jeśli l_{1}, …, l_{n} ∈C, to C −{l_{1}, …, l_{n}} oznacza klauzulę otrzymaną z C w wyniku usunięcia l_{1}, …, l_{n}. Literał dodatni – formuła atomowa. Literał ujemny – negacja formuły atomowej. | l | oznacza formułę atomową literału l.

Podstawienie: Zbiór postaci

{x_{1}/t_{1}, … x_{n}/t_{n}} (1)

gdzie x_{1}, …, x_{n} są różnymi zmiennymi, natomiast t_{1}, … t_{n} są termami. Dopuszczamy podstawienie puste, oznaczane ϵ.

Niech θ będzie podstawieniem postaci (1) i niech α będzie wyrażeniem (tzn. formułą lub termem). Piszemy αθ na oznaczenie wyrażenia powstałego z α w wyniku jednoczesnego zastąpienia wszystkich wolnych wystąpień zmiennych x_{1}, …, x_{n} termami t_{1}, … t_{n}.

Na przykład, jeśli θ = {x/Sam, y/P am}, to

(Likes(x, y))θ = Likes(Sam, P am).

Podstawienie θ jest unifikatorem wyrażeń E_{1}, …, E_{n} jeśli E_{1}θ =E_{2}θ = ⋯ = E_{n}θ.

Podstawienie θ jest najogólniejszym unifikatorem wyrażeń E_{1}, …, E_{n}, jeśli dla każdego unifikatora tych wyrażeń, γ, istnieje podstawienie λ takie, że γ = θλ.

Reguła rezolucji

Definicja 1 Niech C_{1} i C_{2} będą klauzulami bez wspólnych zmiennych. Niech l_{1}, …, l_{n} ∈ C_{1} (n > 0) i l′_{1}, …, l′_{k} ∈ C_{2} (k > 0). Załóżmy ponadto, że wszystkie literały l_{1}, …, l_{n} są dodatnie i wszystkie literały l′_{1}, …, l′_{k} są ujemne, lub odwrotnie. Jeśli θ jest najogólniejszym unifikatorem zbioru {|l_{1} |, …, |l_{n} |, |l′_{1} |, …, |l′_{k} |}, to klauzulę

(C_{1}θ − {l_{1}θ, …, l_{n}θ}) ∨ (C_{2}θ − {l′_{1}θ, …, l′_{k}θ})

nazywamy binarną rezolwentą klauzul C_{1} i C_{2}.

Przykład Niech

C_{1} = P (x) ∨ P (y) ∨ Q(B).
C_{2} = R(A) ∨ ¬P (F (A)).

Klauzula Q(B) ∨ R(A) jest binarną rezolwentą klauzul C_{1} i C_{2}. (l_{1} = P (x), l_{2} = P (y), l′_{1} = ¬P (F (A)); θ = {x/F (A), y/F (A)}.)

Definicja 2 Rezolwentą klauzul C_{1} i C_{2}, oznaczaną RES(C_{1}, C_{2}), nazywamy dowolną binarną rezolwentę wariantu klauzuli C_{1} i wariantu klauzuli C_{2}.

Definicja 3 Regułą rezolucji nazywamy regułę wnioskowania

\frac{C_{1}, C_{2}}{RES(C_{1}, C_{2})} .

Dowód rezolucyjny ze zbioru klauzul CL: Ciąg klauzul C_{1}, …, C_{n} taki, że C_{n} = ⊥ i dla każdego 1 ≤ i ≤ n, C_{i} ∈CL lub C_{i} jest rezolwentą C_{j} i C_{k}, gdzie j, k < i.

Twierdzenie Niech CL będzie zbiorem klauzul nie zawierających symbolu “=”. CL jest niespełnialny wtw gdy istnieje dowód rezolucyjny z CL.

Aksjomaty równości

CL – zbiór klauzul. Niech EQ(CL) – zbiór aksjomatów równości dla CL. EQ(CL) zawiera następujące klauzule:

x = x.

x ≠ y ∨ y = x.

x ≠ y ∨ y ≠ z ∨ x = z.

x_{1} ≠ y_{1} ∨ ⋯ ∨ x_{n} ≠ y_{n} ∨ ¬P (x_{1}, …, x_{n}) ∨ P (y_{1}, …, y_{n}), dla każdego n-argumentowego (n > 0) symbolu predykatowego P występującego w CL.

x_{1} ≠ y_{1} ∨ ⋯ ∨ x_{n} ≠ y_{n} ∨ (F (x_{1}, …, x_{n}) = F (y_{1}, …, y_{n})), dla każdego n-argumentowego (n > 0) symbolu funkcyjnego F występującego w CL.

Twierdzenie Niech CL będzie zbiorem klauzul z równością. CL jest niespełnialny wtw gdy istnieje dowód rezolucyjny z CL ∪ EQ(CL).

Rezolucja liniowa

Liniowym dowodem rezolucyjnym ze zbioru klauzul CL nazywamy dowód postaci

C_{0} ................... C_{1} C_{2} C_{n−1} C_{n}  B_{0} B_{1} B_{n−1}

gdzie:

1. C_{0} ∈ CL

2. Dla 0 ≤ i < n, B_{i} ∈ CL lub B_{i} = C_{J}, dla pewnego j < i.

3. Dla 1 ≤ i ≤ n, C_{i} jest rezolwentą C_{i−1} i B_{i−1}.

4. C_{n} = ⊥.

Twierdzenie Niech CL będzie zbiorem klauzul nie zawierających symbolu “=”. CL jest niespełnialny wtw gdy istnieje liniowy dowód rezolucyjny z CL.

Twierdzenie Niech CL będzie zbiorem klauzul z równością. CL jest niespełnialny wtw gdy istnieje liniowy dowód rezolucyjny ze zbioru CL ∪ EQ(CL).

Klauzulę C_{0} w liniowym dowodzie rezolucyjnym nazywamy klauzulą główną.

Twierdzenie Niech CL będzie niespełnialnym zbiorem klauzul i niech CL′ ⊆ CL. Jeśli zbiór CL − CL′ jest spełnialny, to istnieje liniowy dowód rezolucyjny z CL (ewentualnie z CL ∪ EQ(CL)) z klauzulą główną C ∈CL′.

Logiczne systemy wnioskowania

• Udowadniacze twierdzeń (theorem provers) – AURA, OT-TER, SCAN.

• Języki programowania w logice (logic programming languages) – PROLOG, LIFE, GÖDEL.

• Systemy produkcyjne (production systems) – OPS-5, CLIPS, SOAR .

• Ramy (frames) – OWL, KODIAK, FRAIL.

• Sieci semantyczne (semantic nets) – CG, NETL, SNEPS