720154784

Wstęp do Metod Sztucznej Inteligencji

1.1 Przykłady programów opartych na szukaniu

Programy oparte na przeszukiwaniu przestrzeni stanów i tworzeniu drzewa możliwości należą do jednych z pierwszych prób rozwiązania zagadnień wymagających inteligencji. Wymienimy tutaj kilka wczesnych prób.

1.1.1. Teoretyk logiki

Logic Theorist (A. Newell, J.C. Shaw, H.A. Simon, 1956), był to jeden z pierwszych programów heurystycznych. Jego twórcy tak sformułowali swoje cele.

Nie jesteśmy zainteresowani metodami, które gwarantują rozwiązania lub wymagają wielu obliczeń. Chcielibyśmy raczej zrozumieć jak np. matematyk jest wstanie dowodzić twierdzeń, chociaż nie wie, kiedy zaczyna, w jaki sposób i czy w ogóle mu się to uda.

Heurystyki programu LT ograniczają przestrzeń poszukiwania rozwiązań przez odpowiednie dobranie sformułowania problemu; w ramach tej przestrzeni wykonuje się ślepe przeszukiwanie. Program dowodzi twierdzenia zawarte w Principia Mathemathica Whitheada i Russela dotyczące rachunku zdań. Opiera się na 5 aksjomatach:

1.    (p v p) => p

2.    p => (q v p)

3.    (pvq)=.(qv p)

4.    [pv(qvr)]=>[qv(pvr)]}

5.    (p => q) => [(r v p)] => (r v q)]

Typowe twierdzenia dowodzone przez LT:

2.01 (p => —i p) => —>p

2.31    [pv(qvr)]^[(pvq)vr)]

2.45    ~¹ (p v q) =^> —ip

Dane, którymi można się w danym momencie posłużyć to aksjomaty i twierdzenia poprzednio udowodnione. Z 52 twierdzeń z Principia Mathemathica Teoretyk Logiki udowodnił 38. Program działa rozumując od tyłu, twierdzenia usiłuje redukować do aksjomatów, stosuje przy tym 3 operatory redukcji:

Oderwanie: by pokazać X szukaj A => X i dowiedź A.

Łączenie w przód: by pokazać X postaci A C poszukaj coś (aksjomat, twierdzenie) postaci A => B i dowiedz B => C.

Łączenie w tył: by pokazać X postaci A ^ C poszukaj coś w postaci B => C i dowiedz A => B.

Problem: jak rozpoznać równoważność postaci przy różnych zmiennych? Jakie operatory można stosować?

Podstawienie: Zmienną zastąpić można podstawieniem, np. p => (qvp) podstawiamy p v q zamiast p i mamy (p v q) => [q v (p v q)].

Wymiana: operator wymienić można zgodnie z jego definicją w rachunku zdań tj. p => q na —ip v q (łatwo sprawdzić tabele wartości):

Ogólny algorytm: przeszukujemy przestrzeń stanów na ślepo, rozumując do tyłu. Test, czy dowód został już zakończony: przez porównanie z już udowodnionymi twierdzeniami i aksjomatami. Jeśli dowód nie jest jeszcze skończony do listy problemów dodajemy kolejny problem cząstkowy. Stosujemy oderwanie, łączenie wprzód i w tył aż do wyczerpania pamięci lub otwartych problemów.

Subtelności: by oszczędzić na czasie nie porównuje się po każdej transformacji ze wszystkimi twierdzeniami lub aksjomatami; wstępnie określa się podobieństwo, np. czy tyle samo argumentów.