Idea ADT

Twierdzenie (Church) 

Rachunek predykatów jest częściowo rozstrzygalny.
Tzn. istnieje algorytm, który dla dowolnej formuły  będącej tautologią, potrafi 

to stwierdzić

UWAGA: Dzięki twierdzeniu Posta (i odpowiadającemu mu twierdzeniu 
                  dla rachunku predykatów), sprawdzenie prawdziwości formuły  

    na podstawie prawdziwości formuł zawartych w zbiorze X  ( X|=  )

    można sprowadzić do zagadnienia poszukiwania wnioskowania 
    (dowodu)  ze zbioru X. Wnioskowanie jako operacja czysto 

    syntaktyczna dobrze poddaje się automatyzacji.

 

 

ADT - RP

W przypadku rachunku predykatów opracowano wiele metod 
ADT, np. procedura Herbranda (postać normalna, standardowa 
postać Skolema, sprzeczny zbiór formuł, Uniwersum Herbranda-
Skolema).

W naszych rozważaniach ograniczymy się do pokazania, jak 
realizować ADT 
w pewnym ograniczonym języku reprezentacji wiedzy 
nazywanym językiem
klauzul (w szczególności klauzul Horna).
Rozważać będziemy dwa sposoby dowodzenia: wstępujące i 
zstępujące.
W przypadku dowodów zstępujących wnioskować będziemy 
zgodnie z regułą
wnioskowania znaną jako „zasada rezolucji” („modus tollens”).

Klauzule definicje
Atom  P(t

1

, t

2

, .., t

n

)   P-predykat  t

i

 – termy

Klauzula  B

1

, B

2

, .., B

m

  A

1

, A

2

,.., A

n

   gdzie dowolne A

i

, B

j

  są 

atomami

Dokładniej
A

1

, A

2

,.., A

n 

– koniunkcja atomów

B

1

, B

2

, .., B

m 

– alternatywa atomów

 

 

Klauzule Horna

Klauzulę postaci

B  A

1

, A

2

,.., A

n 

 nazywamy klauzulą Horna

 

Jeśli klauzula B  A

1

, A

2

,.., A

n

 zawiera zmienne x

1

, x

2

, .., x

k

, to 

należy ją interpretować jako stwierdzenie, że:

dla wszystkich x

1

, x

2

, .., x

k

 zachodzi B jeśli A

1

, A

2

,.., A

n

 

 

Jeśli n=0, czyli mamy postać B, to zapis ten oznacza 
stwierdzenie faktu B

Jeśli w konkluzji nie występuje żaden atom, to mamy postać:

A

1

, A

2

,.., A

n  

którą interpretujemy jako – dla wszystkich x

1

, x

2

, .., x

k

  

nieprawda, że A

1

, A

2

,.., A

n

 

(pamiętając, że z prawej strony klauzuli mamy koniunkcję)

 

 

Przykłady

Baza związków rodzinnych:
Ojciec(zeus. ares).
Ojciec(ares, harmonia).
Ojciec(kadmos, semele).
Ojciec(zeus, dionizos).
Matka(afrodyta, harmonia).
Matka(hera, ares).
Matka(harmonia, semele).
Bog(zeus).
Bog(hera).
Bog(ares).
Bog(afrodyta).
Krolowa(harmonia).
Plec-zenska(X) <- Matka(X, Y).
Plec-meska(X) <- Ojciec(X, Y).
Dziecko(Y, X) <- Matka(X, Y).
Dziecko(Y, X) <- Ojciec(X, Y).
Wnuk(X, Y) <- Dziecko(X, Z), Dziecko(Z, Y).
Plec-meska(X), Plec-zenska(X) <- Czlowiek(X).

 

 

Sprzeczność zbioru 

klauzul

Zbiór klauzul S jest sprzeczny wttw nie jest niesprzeczny 
Sprzeczność zbioru klauzul można wykazać drogą:

-

semantyczną

-

syntaktyczną (już wiemy, że ta lepiej nadaje się do 
algorytmizacji)

Metoda semantyczna

Zbiór klauzul S jest niesprzeczny, jeśli w pewnej Interpretacji 

wszystkie

klauzule tego zbioru są prawdziwe.

 

 

Uniwersum Herbranda-Skolema

Uniwersum zbioru klauzul

S – zbiór klauzul

H

0

={ stałe występujące w S}  lub H

0

={a} jeśli w S nie ma 

stałych (stała Skolema)

H

k+1

=H

k

{ f(t

1

, t

2

,..,t

n

) : t

i

H

k

 }

H=



N

k

k

H



Uniwersum Herbranda-Skolema

Uniwersum zbioru klauzul S – zbiór wszystkich termów 

ustalonych, które daje się

zbudować ze stałych i symboli funkcyjnych występujących w 

klauzulach zbioru S

UWAGA !!: Jeśli chcemy wykazać, że w języku klauzul zbiór założeń S
implikuje pewną konkluzję  , to zakładamy, że konkluzja ta nie jest 

prawdziwa i pokazujemy, że negacja konkluzji jest sprzeczna z założeniami.

Czyli, że zbiór klauzul S{}

jest sprzeczny 

dotyczy metody semantycznej i syntaktycznej

 

 

Interpretacja (dopuszczalna) zbioru 

klauzul

Za interpretację zbioru klauzul S będziemy uważać przypisanie 

każdemu

n-argumentowemy symbolowi predykatowemu występującemu w 

klauzulach 

pewnej relacji między indywiduami należącymi do Uniwersum.

Wykazanie sprzeczności zbioru klauzul metodą semantyczną 

sprowadza się do 

pokazania, że w żadnej interpretacji nie są one (te klauzule) 

wszystkie

jednocześnie prawdziwe.

 

 

Przykład – Omylnego Greka

Przykład (Omylny Grek):
1. Czlowiek(kowalski).
2. Czlowiek(sokrates).
3. Grek(sokrates).
4. Omylny(X) <- Czlowiek(X).      

Pytam, czy na podstawie tych założeń mogę

wyciągnąć konkluzję, że istnieje omylny Grek.

Dołączam klauzulę
5. <- Omylny(X), Grek(X).
Sprawdzam czy zbiór klauzul 1-5 jest sprzeczny

Uniwersum {kowalski, sokrates}  - nie ma symboli funkcyjnych, więc jest prosto

Ile tutaj jest możliwych różnych Interpretacji ?
3 – symbole predykatowe, 2 – stałe, 2 – wartości logiczne
Zatem każdemu z trzech symboli predykatowych może być przypisana jedna 
z czterech różnych interpretacji, zatem:

4*4*4=64   - tyle jest Interpretacji

 

 

Przykład cd.

Przykład (Omylny Grek):
1. Czlowiek(kowalski).
2. Czlowiek(sokrates).
3. Grek(sokrates).
4. Omylny(X) <- Czlowiek(X).      
5. <- Omylny(X), Grek(X).

Rozpatrzmy najpierw tylko pierwsze cztery klauzule.
Istnieją tylko dwie interpretacje, w których klauzule 1-4 są wszystkie jednocześnie
prawdziwe.

pierwsza
Czlowiek(sokrates)      

prawda

Omylny(sokrates)

prawda

Grek(sokrates)

prawda

Czlowiek(kowalski) prawda
Omylny(kowalski)

prawda

Grek(kowalski)

prawda

druga
Czlowiek(sokrates)      

prawda

Omylny(sokrates)

prawda

Grek(sokrates)

prawda

Czlowiek(kowalski) prawda
Omylny(kowalski)

prawda

Grek(kowalski)

fałsz

 

 

Przykład - koniec

Przykład (Omylny Grek):
1. Czlowiek(kowalski).
2. Czlowiek(sokrates).
3. Grek(sokrates).
4. Omylny(X) <- Czlowiek(X).      
5. <- Omylny(X), Grek(X).

Dla zbioru klauzul 1-5 Uniwersum oraz liczba interpretacji są identyczne jak dla
1-4.
Ale w żadnej z owych dwóch interesujących nas Interpretacji klauzule 1-5 nie są
wszystkie jednocześnie prawdziwe. W szczególności X=sokrates czyni fałszywą
klauzulę 5 w obu interesujących nas interpretacjach 

Zatem stwierdzenie, że istnieje omylny grek jest logiczną 

konsekwencją zbioru

klauzul 1-4

Taki sposób dowodzenia daje się automatyzować

- 

Algorytm Gilmore`a  - nieefektywny obliczeniowo

-

Reguły Davisa i Putmana – pozwalają zmniejszyć liczbę 
klauzul w zbiorze S
np. poprzez usunięcie z niego wszystkich tautologii

 

 

Metoda syntaktyczna

Dowodzenie (wnioskowanie) metodą syntaktyczną 

przeprowadzać będziemy

za pomocą reguły wnioskowania, znanej jako modus tollens (lub 

ogólniej zasady

rezolucji)

Zasada rezolucji dla KRZ:     p , q

i

 , r

j

 - zdania

p  q

1

 ..q

n

 , p  r

1

 .. r

m

      q

1

 q

n

  r

1

 .. r

m

W szczególnym przypadku zasada rezolucji redukuje się do 

reguły odrywania

rezolwenta

,    



Modus tollens

, 

  

 



Modus ponens

UWAGA:  Zasada rezolucji stanowi zatem uogólnienie reguły odrywania.

 

 

Metoda syntaktyczna

Twierdzenie 
Rezolwenta  formuł ,  jest ich logiczną konsekwencją

W systemach dowodzących opartych na zasadzie rezolucji gra 

ona (klauzula pusta)

niebagatelną rolę, ponieważ jej wyprowadzenie ze zbioru formuł 

S oznacza

sprzeczność zbioru klauzul S. 

Jeśli przesłankami rezolucji są dwie pojedyncze klauzule (atomy), 

to ich 

rezolwenta jest klauzulą pustą (ozn.  ).

Klauzula pusta jest fałszywa przy każdej interpretacji.

, 



 

 

Metoda syntaktyczna – 

dowód wstępujący

Dowodzenie sprzeczności metodą wstępującą rozpoczyna się od 

początkowego

zbioru klauzul, kończy z chwilą wyprowadzenia takich wniosków, 

które

bezpośrednio zaprzeczają negacji dowodzonej tezy.

Przy czym krok wnioskowania polega na dopasowaniu (w 

możliwie ogólny 

sposób) odpowiedniej liczby predykatów – konkluzji klauzuli – do 

warunków

klauzuli i wyprowadzenia nowej konkluzji.

Dowód wstępujący to dowód w sensie dowodu formalnego, 

którego definicja dla

KRZ podawana była na trzecim wykładzie.

Startujemy z aksjomatów (którymi są klauzule znajdujące się w 

zbiorze S)

i stosując dopuszczalne reguły wnioskowania postępujemy tak, 

aby otrzymać

klauzulę, której prawdziwość chcemy dowieść (lub klauzulę 

pustą, jeśli do zbioru S dołączyliśmy zaprzeczenie klauzuli, 
której prawdziwość chcemy dowieść).

 

 

Przykład dowodu wstępującego

Zakładamy, że dostępna jest baza wiedzy nt. związków rodzinnych (slajd nr 9)
to jest nasz zbiór S.

Mamy wykazać, że harmonia jest wnuczką zeusa.

Czyli, że ze zbioru  S{ <-Wnuk(harmonia, zeus) } da się wyprowadzić klauzulę

pustą.

Ojciec(zeus,ar
es)

Ojciec(ares,harmon
ia)

Dziecko(ares, 
zeus)

Dziecko(harmonia, ares)

Wnuk(harmonia,zeus
)

<- 
Wnuk(harmonia,zeus
)



 

 

Efektywność metody wstępującej

W poprzednim drzewie dowodowym tak dobieraliśmy 

początkowe fakty i 

reguły wnioskowania (tutaj klauzule w postaci implikacji), aby 

owe drzewo było

jak najmniejsze.
Metoda algorytmiczna musiałaby rozważać wszystkie drogi, 

również te nie- 

prowadzące do celu.
Klauzule rozpatrywane byłyby po kolei (tak jak występują w 

zbiorze S).

Wniosek, iż taka metoda byłaby złożona obliczeniowo, jest jak 

najbardziej 

uprawniony.

Efektywniejsza jest metoda zstępująca.

 

 

Metoda syntaktyczna – dowód 

zstępujący

Dowodzenie sprzeczności metodą zstępującą, polega na 

rozpoczęciu dowodu od

negacji należącej do początkowego zbioru klauzul (tej negacji, 

którą dołączyliśmy

do zbioru S).
Następnie implikacji i asercji (czyli po prostu faktów) używa się 

do

wyprowadzenia nowych negacji z negacji już istniejących 

(stosujemy zasadę

rezolucji).
Dowód kończy się z chwilą wyprowadzenia klauzuli pustej. 

Dokładniej – wnioskowanie zstępujące polega na dopasowaniu 

wybranego 

warunku negacji do konkluzji pewnej implikacji, wyprowadzeniu 

nowej negacji

przez zastąpienie wybranego warunku, warunkami tej 

(dopasowanej) implikacji

i zastosowaniu do niej podstawienia dopasowującego.

Jeśli implikacja jest asercją (faktem), to w wybrany warunek jest 

usuwany, a

podstawienie dopasowujące stosuje się do pozostałej części 

negacji.

Jeśli wybrany warunek jest jedynym warunkiem negacji, 

wówczas nowo

wyprowadzana negacja jest klauzulą pustą.  

 

 

Przykład

Baza wiedzy ta sama (ten sam zbiór S), zadanie : 
Szukamy wszystkich dziadków harmonii.
Czyli, że ze zbioru  S{ <-Wnuk(harmonia, U) } da się wyprowadzić klauzulę

pustą. Dokładnie dla jakich U da się to zrobić

 

 

Efektywność metody 

zstępującej

Przedstawione na poprzednim slajdzie drzewo dowodowe 

również może wyglądać

inaczej.
Postać drzewa przeszukiwania zależeć będzie od strategii 

dopasowywania

implikacji 

Drzewa dowodowe możemy zbudować stosując strategie 

przeszukiwania:

„w głąb” i „wszerz”.
Z punktu widzenia szybkości znalezienia odpowiedzi, strategia 

„w głąb” jest

bardziej efektywna.

                             W punktach oznaczonych okręgami (tam, gdzie ścieżka się

rozgałęzia) wykonano tzw. nawroty. Znaczy to, że w danym 
węźle udało się dopasować więcej niż jedną implikację.

    

Na czerwono zaznaczono ścieżkę, która zostanie zbadana 
w pierwszej kolejności.

 

 

Rodzaje twierdzeń

Przeprowadzając dowód pokazujący, że klauzula  jest logiczną 

konsekwencją

zbioru formuł S, formuła  pełni rolę tezy twierdzenia, a zbiór 

formuł S jest 

zbiorem założeń owego twierdzenia – stąd tytuł wykładu 

Automatyczne

Dowodzenie Twierdzeń.

UWAGA:  Możemy formułować twierdzenia dwojakiego rodzaju:
                   i) wynikiem dowodu jest odpowiedź TAK/NIE (teza nie zawiera

        zmiennych)
    ii) wynikiem są te wartości zmiennej (zmiennych) występujących w tezie,

                      które czynią twierdzenie prawdziwym (przy spełnionych założeniach)

Przykład:
i)

Wnuk(harmonia, zeus)    - czy harmonia jest wnuczką zeusa

ii) Wnuk(harmonia, U)        - czyją harmonia jest wnuczką

UWAGA: Odpowiedź w obu przypadkach zależy jedynie od postaci zbioru
założeń S !!! Czyli bez odpowiedniej informacji w tym zbiorze wynikiem
dla pkt. i) może być odpowiedź NIE.

 

 

Strategia tworzenia bazy 

wiedzy

UWAGA: We wnioskowaniu zstępującym przyjmuje się następującą strategię
                  tworzenia drzewa dowodowego:

    i) pierwsza klauzula z procedury, którą można dopasować

                  ii) pierwszy podcel w przesłankach nowej negacji 

Baza związków rodzinnych:
Ojciec(kadmos, semele).
Ojciec(zeus, dionizos).
Ojciec(ares, harmonia).
Ojciec(zeus.ares).
Matka(afrodyta, harmonia).
Matka(harmonia, semele).
Matka(hera, ares).
Dziecko(Y, X) <- Matka(X, Y).
Dziecko(Y, X) <- Ojciec(X, Y).
Wnuk(X, Y) <- Dziecko(X, Z),
                          Dziecko(Z, Y).

 

 

Formalizacja pojęć

Załóżmy, że dany jest zbiór klauzul Hornowskich S oraz 

dana jest strategia

wyboru jednego z warunków negacji (strategia tworzenia 

drzewa

dowodowego).

Definicja
Ciąg negacji C

1

, C

2

, ..,C

n

 jest zstępującym dowodem klauzuli C

1

 

ze zbioru 

klauzul S jeśli:
i)

C

1

 należy do zbioru S.

ii) Dla każdego i=2,..,n, klauzula C

i  

otrzymywana jest z C

i-1

 

przez zastosowanie

        wnioskowania zstępującego (zasady rezolucji) z użyciem 

jednej z klauzul

        zbioru S.
i)

Ze zbioru C

1

, C

2

, ..,C

n

 da się już wywieść klauzulę pustą. 

 

 

Formalizacja pojęć cd.

W kwestii dowodów
Gdy dana jest negacja  A

1

,...,A

i-1

, A

i

, A

i+1

,.., A

m

  oraz implikacja

B  B

1

,..,B

n

 , która nie ma z negacją wspólnych zmiennych (jeśli 

są, to

przemianować).

Nową negację możemy otrzymać, jeśli A

i

 pasuje do konkluzji B.

Nowa negacja jest postaci:
 ( B

1

,..,B

n

,...,A

i-1

, A

i

, A

i+1

,.., A

m

 )  

gdzie  jest podstawieniem dopasowującym A

1 

do B

Definicja
Podstawienie : X T  to funkcja przypisująca zmiennym termy

UWAGA: W przypadku konkretnego zbioru S rozpatrujemy oczywiście tylko
                  zmienne i termy występujące w S

.

 

 

Formalizacja pojęć cd.

Przykład
Jeśli E jest wyrażeniem (termem, atomem, klauzulą), to wynikiem podstawienia
={ X

1

=t

1

,..., X

m

=t

m

 }  jest wyrażenie E identyczne z E, poza tym, że

( X

i

=t

i

 ) wszędzie tam, gdzie w E występuje X

i

, w E występuje t

i

. 

O wyrażeniu E mówimy, że jest konkretyzacją wyrażenia E
Definicja
Podstawienie  uzgadnia dwa wyrażenia E i E`, jeśli czyni je (te 

wyrażenia) 

identycznymi

Przykład
Wnuk(harmonia, U).      Wnuk(harmonia, X).                  U:=Z, X:=Z
Wnuk(harmonia, U) .     Wnuk(harmonia, zeus).   U:=zeus
Wnuk(harmonia, U) .    Wnuk(achilles, U).                  nie da się uzgodnić

 

 

Formalizacja pojęć cd.

Definicja
Podstawienie  dopasowuje wyrażenia E i E` (tzn. jest 

najbardziej ogólnym

podstawieniem uzgadniającym (ozn. MGU)), jeśli spełnia dwa 

następujące

warunki:
i)

 uzgadnia E i E`

ii) Jeśli    E=E`,  to istnieje pewne  takie, że

        E=(E`)

Stwierdzenie
Każde dwa wyrażenia, które można uzgodnić, można również 

dopasować.

UWAGA: W języku prolog w czasie wnioskowania szukamy MGU.
                  Istnieje algorytm znajdowania (jeśli istnieje) MGU.

Przykład

Ojciec(zeus, U).

                           

Ojciec(X, Y)

 <- Dziecko(Y,X),Plec-meska(X).

Można dopasować
Ojciec(zeus, ares).  X:=zeus, U:=ares, Y:=ares           
Ojciec(zeus, V).      X:=zeus, U:=V, Y:=V               <- to jest MGU