AI_9_1

Jak wnioskowa

z kwantyfikatorami...

W j

zyku logiki pierwszego rz

du mo

na opisa

wiat w sposób

cisły, a zarazem bardzo zwi

zły.

Zwi

zło

ść

opisu osi

ga si

poprzez u

ycie obiektów,

relacji mi

dzy nimi, funkcji oraz

kwantyfikatorów

Wyst

powanie kwantyfikatorów uniemo

liwia

jednak prowadzenie wnioskowania w taki sposób,
jak w rachunku zda

F.A. Dul 2007

jak w rachunku zda

Zdania zapisane w j

zyku logiki pierwszego rz

musz

c najpierw by

przekształcone do postaci

umo

liwiaj

cej wnioskowanie.

Zdania FOL mo

na przekształci

do postaci

rachunku zda

, albo te

do takich postaci, które

umo

liwiaj

wnioskowanie bezpo

rednie w FOL

za pomoc

przekształconych metod wnioskowania.

9.1. Sprowadzenie wnioskowania logiki pierwszego

du do wnioskowania w rachunku zda

Wnioskowanie w logice pierwszego rz

du mo

e by

sprowadzone do wnioskowania w rachunku zda

Idea: nale

y zast

zdania kwantyfikowne przez zbiór zda

bez kwantyfikatorów.

Zbiór zda

zdekwantyfikowanych powinien by

równowa

wyj

ciowemu zbiorowi zda

kwantyfikowanych lub co najmniej

spełnialny.

© F.A. Dul 2007

• Eliminacja kwantyfikatorów ogólnych

Zast

pienie zmiennej przez

symbol podstawowy

(ground term)

• Eliminacja kwantyfikatorów szczegółowych

skolemizacja

spełnialny.

Podstawienie ogólne (universal instantiation, UI)

de podstawienie do zdania z kwantyfikatorem ogólnym

pewnego wyra

enia za zmienn

kwantyfikowan

wynika

z tego zdania, tj.

∀

—————————

Subst( {v/g},

)

dla ka

dej zmiennej v i ka

dego wyra

enia g.

Subst(

)

= podstawienie

9.1. Sprowadzenie FOL do PL

© F.A. Dul 2007

Przykład Podstawienie do zdania

∀

x Król(x)

∧

Chciwy(x)

⇒

Zły(x)

wyra

: {x/Jan}, {x/Ryszard} i {x/Ojciec(Jan)} daje zdania:

Król(Jan)

∧

Chciwy(Jan)

⇒

Zły(Jan)

Król(Ryszard)

∧

Chciwy(Ryszard)

⇒

Zły(Ryszard)

Król(Ojciec(Jan))

∧

Chciwy(Ojciec(Jan))

⇒

Zły(Ojciec(Jan))

Zdanie z kwantyfikatorem ogólnym jest równowa

ne zbiorowi

zda

z podstawieniami

wszystkich

obiektów z dziedziny.

9.1. Sprowadzenie FOL do PL

Podstawienie szczegółowe (existential instantiation, EI)

Dla ka

dego zdania

, zmiennej v i stałej k która

nie wyst

puje

w bazie wiedzy KB zachodzi wynikanie

∃

—————————

Subst( {v/k},

)

Przykład Podstawienie stałej C

do zdania

∃

x Korona(x)

∧

NaGłowie(x,Jan)

© F.A. Dul 2007

∃

x Korona(x)

∧

NaGłowie(x,Jan)

daje zdanie

Korona(C1)

∧

NaGłowie(C1,Jan)

Stała C

nazywa si

stał

Skolema

, za

procedura jej

podstawienia –

skolemizacj

Warunek niewyst

powania w bazie KB stałej Skolema której

chcemy u

jest bardzo wa

ny!

Niespełnienie tego warunku powoduje,

e relacja wynikania

zbioru zda

skolemizowanych z bazy KB nie jest spełniona.

9.1. Sprowadzenie FOL do PL

Ró

nice pomi

dzy podstawieniami: ogólnym (UI)

oraz szczegółowym (EI)

• Podstawienie ogólne (UI) mo

e by

wykonane wielokrotnie

w celu

dodania

nowych zda

do bazy wiedzy.

Nowa baza wiedzy KB jest równowa

na logicznie bazie

starej.

• Podstawienie szczegółowe (EI) mo

e by

wykonane

tylko raz

, w celu eliminacji kwantyfikatora szczegółowego.

© F.A. Dul 2007

tylko raz

, w celu eliminacji kwantyfikatora szczegółowego.

Nowa baza wiedzy KB

nie jest

równowa

na logicznie bazie

starej, ale jest spełnialna (tj. prawdziwa dla

pewnych

modeli)

eli baza wyj

ciowa była spełnialna.

9.1. Sprowadzenie FOL do PL

Sprowadzenie wnioskowania FOL do wnioskowania

w rachunku zda

Załó

my,

e baza wiedzy KB zawiera nast

puj

ce zdania

i wyra

enia:

Wykonanie

wszystkich

liwych podstawie

, tutaj:

∀

x Król(x)

∧

Chciwy(x)

⇒

Zły(x)

Król(Jan)
Chciwy(Jan)
Brat(Ryszard,Jan)

© F.A. Dul 2007

Król(Jan)

∧

Chciwy(Jan)

⇒

Zły(Jan)

Król(Ryszard)

∧

Chciwy(Ryszard)

⇒

Zły(Ryszard)

Król(Jan)
Chciwy(Jan)
Brat(Ryszard,Jan)

{x/Jan}, {x/Ryszard}

daje w wyniku now

baz

KB:

Nowa baza wiedzy jest ju

czysto

predykatowa

(KB PL)

– nie ma w niej kwantyfikatorów.

Predykatami s

Król(Jan), Chciwy(Jan), Zły(Jan),

etc.

9.1. Sprowadzenie FOL do PL

• Ka

da baza wiedzy zapisana w logice pierwszego rz

(KB FOL) mo

e by

sprowadzona do bazy predykatowej

(KB PL) w taki sposób,

e wynikanie jest zachowane, tj,

Zdanie wynika z przekształconej bazy KB wtedy
i tylko wtedy, gdy wynika z bazy pierwotnej.

• Zasada: przedstawienie w postaci predykatowej bazy

wiedzy KB PL, zapyta

, rezolucji, odpowiedzi.

• Problem: funkcje generuj

niesko

czone ci

gi wyra

, np.

© F.A. Dul 2007

• Problem: funkcje generuj

niesko

czone ci

gi wyra

, np.

Ojciec(Ojciec(Ojciec(Jan)))...

Twierdzenie (Turing, Church 1936) Wynikanie w logice
pierwszego rz

du jest

półrozstrzygalne

(semidecidable).

Oznacza to,

e :

istniej

algorytmy

które daj

odpowied

twierdz

na ka

zdanie wynikaj

ce z bazy KB FOL, ale

nie ma algorytmów

które odpowiadaj

przecz

co na ka

zdanie nie wynikaj

ce z bazy KB FOL.

9.1. Sprowadzenie FOL do PL

Problemy ze sprowadzeniem FOL do PL

• Sprowadzenie bazy FOL do postaci predykatowej prowadzi

do utworzenia wielu nieistotnych zda

Przykład Z bazy

∀

x Król(x)

∧

Chciwy(x)

⇒

Zły(x)

Król(Jan)

∀

y Chciwy(y)

Brat(Ryszard,Jan)

wynika w sposób oczywisty zdanie

© F.A. Dul 2007

wynika w sposób oczywisty zdanie

Zły(Jan),

ale równie

wiele zda

nieistotnych, np.

Zły(Ryszard).

• Problem liczby podstawie

Dla p zda

k-krotnych i n stałych istnieje

p·n

podstawie

Wnioskowanie w bazie predykatowej

Przekształcenie bazy zapisanej w j

zyku logiki

pierwszego rz

du do bazy predykatowej pozwala

prowadzi

wnioskowanie metodami rachunku zda

Jednak takie post

powanie mo

e by

wysoce

nieefektywne, gdy

eliminacja kwantyfikatorów

ogólnych mo

e spowodowa

lawinowy wzrost liczby

zda

w bazie przekształconej.

F.A. Dul 2007

zda

w bazie przekształconej.

Lepszym rozwi

zaniem jest

modyfikacja algorytmów

wnioskowania

w taki sposób, aby mo

na było

prowadzi

wnioskowanie bezpo

rednio w bazie FOL.

Osi

ga si

to poprzez zastosowanie operacji

podniesienia i unifikacji oraz wykorzystanie
uogólnionej reguły odrywania i algorytmu eliminacji
(rezolucji).

9.2. Podniesienie i unifikacja

Zamiast przekształca

baz

FOL do postaci PL, mo

przedefiniowa

reguły wnioskowania tak, aby były słuszne

dla logiki pierwszego rz

du u

ywaj

cej kwantyfikatorów:

ogólnych i szczegółowych.

Unifikacja

jest to procedura rekurencyjna pozwalaj

sprawdzi

, czy istnieje podstawienie sprowadzaj

ce dwa

wyra

enia do takiej samej postaci.

Unifikacja pozwala cz

sto istotnie zredukowa

liczb

zda

© F.A. Dul 2007

Unifikacja pozwala cz

sto istotnie zredukowa

liczb

zda

zawartych w bazie wiedzy KB.

Podniesienie

(lifting) - wykonanie podstawie

które pozwalaj

prowadzi

wnioskowanie w bazie FOL.

Przykład liftingu - uogólniona reguła odrywania (Generalized
Modus Ponens).

9.2. Podniesienie i unifikacja

Unifikacja

jest to procedura rekurencyjna pozwalaj

sprawdzi

, czy istnieje podstawienie sprowadzaj

ce dwa

wyra

enia do takiej samej postaci.

Przykłady:

• Kobieta(Anna)

ęŜ

czyzna(Jan)

nie unifikuj

;

• Kobieta(Anna)

Kobieta(Anna)

unifikuj

trywialnie;

• Kobieta(Anna)

Kobieta(Maria)

nie unifikuj

, gdy

maj

© F.A. Dul 2007

• Kobieta(Anna)

Kobieta(Maria)

nie unifikuj

, gdy

maj

ró

ne argumenty;

• Król(x)

Chciwy(x)

oraz

Król(Jan)

Chciwy(y).

Podstawienie

= { x/Jan, y/Jan }

unifikuje obie pary zda

Unifikacja zda

za pomoc

podstawienia

e by

zdefiniowana nast

puj

Unify(

) =

eli Subst(

) = Subst(

)

Unifikacja

θθθθ

Zna(Jan,x)

Zna(Jan,Maria)

{x/Maria}

Zna(Jan,x)

Zna(y,OJ)

{x/OJ,y/Jan}

Zna(Jan,x)

Zna(y,Matka(y))

{y/Jan,x/Matka(Jan)}

Zna(Jan,x)

Zna(x,OJ)

{brak}

9.2. Podniesienie i unifikacja

Przykłady problemów unifikacji:

© F.A. Dul 2007

Nie mo

na podstawi

{x/Jan}

bo otrzymamy

Zna(Jan,Jan)

niezgodne ze

Zna(Jan,OJ)

- wyst

piło nakładanie si

nazw

zmiennych.

Aby usun

ąć

konflikt nazw zast

pujemy zmienn

x w jednym

ze zda

(np. w drugim) inn

zmienn

, np.

. Otrzymujemy

Zna(Jan,x) , Zna(z

,OJ)

Jest to

standaryzacja

która eliminuje konflikty nazw.

Unifikacja

• Aby zunifikowa

Zna(Jan,x)

oraz

Zna(y,z),

na u

ró

nych podstawie

(unifikatorów), np.:

= { y/Jan, x/z }

→

Zna(Jan,z)

oraz

Zna(Jan,z),

lub

= { y/Jan, x/Jan, z/Jan }

→

Zna(Jan,Jan)

oraz

Zna(Jan,Jan)

9.2. Podniesienie i unifikacja

Przykłady problemów unifikacji:

© F.A. Dul 2007

→

Zna(Jan,Jan)

oraz

Zna(Jan,Jan)

• Pierwszy unifikator jest

ogólniejszy

drugi.

• Istnieje jedyny

unifikator najogólniejszy

(most general

unificator, MGU) okre

lony z dokładno

do zmiany

nazw zmiennych.

MGU = { y/Jan, x/z }

Uogólniona reguła odrywania (Generalized Modus
Ponens)

', p

', … , p

', ( p

∧

…

∧

⇒



Subst(

,q)

gdzie Subst(

’) = Subst(

) dla ka

dego i.

9.2. Podniesienie i unifikacja

Przykład

oznacza

Król(Jan)

oznacza

Król(x)

p '

oznacza

Chciwy(y)

oznacza

Chciwy(x)

© F.A. Dul 2007

oznacza

Chciwy(y)

oznacza

Chciwy(x)

oznacza

{x/Jan,y/Jan}

oznacza

Zły(x)

Subst(

,q)

oznacza

Zły(Jan)

• Uogólniona reguła odrywania (GMP) jest u

ywana dla

bazy wiedzy zło

onej z

klauzul Horna

(tj. zawieraj

cych

dokładnie jeden

literał niezanegowany)

• Zakłada si

e wszystkie zmienne s

kwantyfikowane

ogólnie.

Poprawno

ść

uogólnionej reguły odrywania

', p

', … , p

', ( p

∧

…

∧

⇒

q) l= Subst(

,q)

przy zało

eniu,

e Subst(

’) = Subst(

) dla ka

dego i.

9.2. Podniesienie i unifikacja

Nale

y wykaza

Lemat Dla ka

dego zdania p zachodzi p

Subst(

,p)

poprzez podstawienie uniwersalne.

Dowód poprawno

ci GMP (

oznaczenie: Subst(

,p)

≡

)

© F.A. Dul 2007

• (p

∧

…

∧

⇒

∧

…

∧

⇒

(z lematu)

• (p

∧

…

∧

⇒

= (p

θ ∧

…

∧

⇒

)

• p

', …, p

∧

…

∧

• p

∧

…

∧

θ ∧

…

∧

(z lematu)

• st

d, i na mocy zwykłej reguły odrywana wynika

', p

', … , p

', ( p

∧

…

∧

⇒

Dowód poprawno

ci GMP (

oznaczenie: Subst(

,p)

≡

)

9.3. Algorytmy FOL wnioskowania w przód i wstecz

Algorytmy wnioskowania w przód i wstecz dla FOL i logiki
zda

identyczne.

Wnioskowanie w przód dla KB FOL

• Zaczynamy od zda

w bazie KB FOL opisuj

cych fakty;

• Stosujemy uogólnion

reguł

odrywania dla FOL

do wyprowadzenia nowych zda

;

• Dodajemy nowe zdania do bazy KB FOL;
• Wnioskowanie ko

czymy, je

eli wyprowadzimy udowadnia-

© F.A. Dul 2007

Wnioskowanie wstecz dla KB FOL

• Zaczynamy od zdania, które jest zapytaniem do KB FOL;
• Stosujemy uogólnion

reguł

odrywania dla FOL

znajduj

c zdania z których wynika udowadniane zdanie;

• Wnioskowanie ko

czymy, je

eli przesłankami zdania

aktualnie dowodzonego b

zdania bazy KB FOL

które opisuj

fakty dowiedzione;

• Wnioskowanie ko

czymy, je

eli wyprowadzimy udowadnia-

ne zdanie lub gdy dalsze wnioskowanie nie jest mo

liwe;

Przykład wnioskowania z bazy wiedzy FOL

9.3. Algorytmy FOL wnioskowania w przód i wstecz

• Prawo USA stanowi,

e przest

pstwem jest sprzeda

broni do krajów wrogich.

• Kraj Nono, wróg USA, posiada pewn

liczb

rakiet.

• Wszystkie te rakiety zostały sprzedane Nono przez

niejakiego pułkownika Westa.

• Pułkownik West jest Amerykaninem.

Baza wiedzy KB FOL zawiera nast

puj

ce zdania:

© F.A. Dul 2007

• Pułkownik West jest Amerykaninem.

Dowie

ść

e w

wietle prawa ameryka

skiego pułkownik

West jest przest

Przykład wnioskowania z bazy wiedzy FOL

9.3. Algorytmy FOL wnioskowania w przód i wstecz

Baza wiedzy w postaci zda

FOL:

... jest przest

pstwem gdy Amerykanin sprzedaje bro

krajom wrogim:

American(x

∧

Sells(x,y,z) )

∧

Weapon(y)

∧

Hostile(z)

⇒

Criminal(x)

Nono … posiada pewn

liczb

rakiet, tj.,

∃

x Owns(Nono,x)

∧

Missile(x)

Owns(Nono,M

) i Missile(M

)

… wszystkie rakiety zostały sprzedanie Nono prze pułkownika Westa

Missile(x)

∧

Owns(Nono,x)

⇒

Sells(West,x,Nono)

© F.A. Dul 2007

Missile(x)

∧

Owns(Nono,x)

⇒

Sells(West,x,Nono)

Rakiety s

broni

Missile(x)

⇒

Weapon(x)

Wróg Ameryki jest wrogiem:

Enemy(x,America)

⇒

Hostile(x)

West jest Amerykaninem …

American(West)

Kraj Nono, wróg Ameryki …

Enemy(Nono,America)

Własno

ci wnioskowania w przód

9.3. Algorytmy FOL wnioskowania w przód i wstecz

• Wnioskowanie w przód jest poprawne i zupełne dla bazy

w postaci klauzul Horna pierwszego rz

du.

• Wnioskowanie w przód dla klauzuli Horna pierwszego

nie zawieraj

cych funkcji

wymaga sko

czonej

liczby kroków.

• Wnioskowanie w przód w przypadku ogólnym mo

e si

nie zako

czy

eli zapytanie nie wynika z bazy FOL.

• Nie mo

na temu zaradzi

; wynikanie z klauzulami Horna

© F.A. Dul 2007

• Nie mo

na temu zaradzi

; wynikanie z klauzulami Horna

pierwszego rz

du jest półrozstrzygalne (patrz twierdzenie

Turinga-Churcha).

Efektywno

ść

wnioskowania w przód

9.3. Algorytmy FOL wnioskowania w przód i wstecz

• Przyrostowe wnioskowanie w przód nie musi

dopasowywa

reguł w k-tym kroku je

eli w kroku k-1

nie została dodana nowa przesłanka.

• Dopasowanie reguł nast

puje wtedy, gdy przesłanka

zawiera nowo dodany literał pozytywny.

• Dopasowanie jest kosztowne.

• Indeksowanie

bazy wiedzy pozwala uzyska

informacje

o znanych faktach kosztem O(1).

© F.A. Dul 2007

• Indeksowanie

bazy wiedzy pozwala uzyska

informacje

o znanych faktach kosztem O(1).

Np. zapytanie Missile(x) zwraca Missile(M

• Dopasowanie przesłanek do znanych faktów jest

zadaniem NP-hard.

• Wnioskowanie w przód jest szeroko u

ywane

dedukcyjnych bazach wiedzy

Przykład zadania trudno dopasowalnego

9.3. Algorytmy FOL wnioskowania w przód i wstecz

Diff(wa,nt)

∧

Diff(wa,sa)

∧

Diff(nt,q)

∧

Diff(nt,sa)

∧

Diff(q,nsw)

∧

Diff(q,sa)

∧

Diff(nsw,v)

∧

Diff(nsw,sa)

∧

Diff(v,sa)

⇒

Colorable()

Diff(Red,Blue)

Diff (Red,Green)

Diff(Green,Red) Diff(Green,Blue)

© F.A. Dul 2007

• Colorable()

wynika z bazy wiedzy KB FOL wtedy i tylko

wtedy gdy zadanie poszukiwania z ograniczeniami
(CSP) ma rozwi

zanie.

• Zadanie CSP zawiera zadanie 3SAT jako przypadek

szczególny, zatem dopasowanie jest zadaniem NP-hard.

Diff(Blue,Red)

Diff(Blue,Green)

Własno

ci wnioskowania wstecz

9.3. Algorytmy FOL wnioskowania w przód i wstecz

• Przy rekurencyjnym dowodzeniu w gł

b pami

ęć

zale

liniowo od długo

ci dowodu.

• Wnioskowanie wstecz jest niezupełne z powodu

liwo

ci zap

tlenia si

algorytmu;

• Mo

na jednak temu zaradzi

poprzez sprawdzenie celu

aktualnego z celami składowanymi na stosie.

• Wnioskowanie wstecz mo

e by

nieefektywne gdy

wielokrotnie sprawdza cele ju

osi

gni

te.

© F.A. Dul 2007

• Wnioskowanie wstecz mo

e by

nieefektywne gdy

wielokrotnie sprawdza cele ju

osi

gni

te.

• Mo

na temu zaradzi

poprzez zapami

tywanie wyników

rednich, ale kosztem dodatkowej pami

ci.

• Wnioskowanie wstecz jest szeroko u

ywane

w programowaniu logicznym

9.5. Eliminacja (rezolucja)

∨

···

∨

···

∨

, m

∨

···

∨

···

∨



Subst(

, l

∨

···

∨

···

∨

···

∨

···

∨

m )

Zasada eliminacji pozwala dowodzi

twierdzenia

sformułowane w j

zyku logiki pierwszego rz

du.

Zasada rezolucji umo

liwia tak

e weryfikacj

poprawno

projektów układów elektronicznych oraz dowodzenie
poprawno

ci programów.

Zasada eliminacji dla logiki pierwszego rz

du ma posta

© F.A. Dul 2007



Subst(

, l

∨

···

∨

i-1

∨

i+1

∨

···

∨

···

∨

j-1

∨

j+1

∨

···

∨

)

gdzie

Unify(l

) =

Obie klauzule (alternatywy l

oraz m

) musz

standaryzowane, aby nie miały wspólnych zmiennych.

Eliminacja mo

e by

stosowana do bazy FOL przekształconej

do postaci koniunktywnej normalnej (CNF).

Rezolucja mo

e by

zastosowana do udowodnienia zdania

poprzez wykazanie,

e ( KB FOL

∧ ¬α

) jest niespełnialne.

9.5. Eliminacja (rezolucja)

Przykład
Dane s

zdania

Bogaty(x)

∨

Nieszcz

ęś

liwy(x)

Bogaty(Jan)

Podstawienie

= { x/Jan }

sprowadza klauzule

Bogaty(x) Bogaty(Jan)

do postaci komplementarnej.

Eliminacja

Bogaty(x)

∨

Nieszcz

ęś

liwy(x) Bogaty(Jan)



Nieszcz

ęś

liwy(Jan)

prowadzi wi

c do wniosku,

„Jan jest nieszcz

ęś

liwy”

mimo,

e jest bogaty.

Sprowadzenie zda

FOL do postaci CNF

9.5. Eliminacja (rezolucja)

• Zdanie

“Ka

dy kto kocha wszystkie zwierz

ta jest kochany przez kogo

”.

∀

x [

∀

y Animal(y)

⇒

Loves(x,y) ]

⇒

[

∃

y Loves(y,x) ]

• Eliminacja równowa

ci i implikacji

∀

x [

¬∀

Animal(y)

∨

Loves(x,y) ]

∨

[

∃

y Loves(y,x) ]

• Reguły negacji kwantyfikatorów,

¬∀

x p

≡

∃

¬∃

x p

≡

∀

• Przesuni

cie negacji do wn

trza wyra

∀

x [

∃

(

Animal(y)

∨

Loves(x,y)) ]

∨

[

∃

y Loves(y,x) ]

∀

x [

∃

¬¬

Animal(y)

∧ ¬

Loves(x,y) ]

∨

[

∃

y Loves(y,x) ]

∀

x [

∃

y Animal(y)

∧ ¬

Loves(x,y) ]

∨

[

∃

y Loves(y,x)]

Sprowadzenie zda

FOL do postaci CNF

9.5. Eliminacja (rezolucja)

• Standaryzacja: ka

dy kwantyfikator musi u

ywa

innej

zmiennej

∀

x [

∃

y Animal(y)

∧ ¬

Loves(x,y) ]

∨

[

∃

z Loves(z,x) ]

• Skolemizacja: ogólna forma podstawienia szczegółowego.

da zmienna szczegółowa jest zast

piona przez

funkcj

Skolema

zmiennej zewn

trznej kwantyfikatora

ogólnego:

∀

[ Animal(

F(x)

)

∧ ¬

Loves(x,

F(x)

) ]

∨

Loves(

G(x),

• Opuszczenie kwantyfikatora ogólnego

[ Animal(F(x))

∧ ¬

Loves(x,F(x)) ]

∨

Loves(G(x),x)

• Przekształcenie do postaci koniunkcji alternatyw:

[ Animal(F(x))

∨

Loves(G(x),x) ]

∧

[

Loves(x,F(x))

∨

Loves(G(x),x) ]

Programowanie logiczne vs. proceduralne

9.5. Eliminacja (rezolucja)

Programowanie logiczne

– identyfikacja zadania;

– zebranie informacji;

– kodowanie informacji

w j

zyku logiki bazy

wiedzy;

– kodowanie zadania

Programowanie proceduralne

– identyfikacja zadania;

– zebranie informacji;

– opracowanie algorytmu

rozwi

zania;

– programowanie

algorytmu;

– kodowanie zadania

jako zbioru faktów;

– zadawania pyta

;

– eliminacja błednych

faktów;

algorytmu;

– kodowanie zadania jako

zbioru danych;

– uruchomienie programu

dla zbioru danych;

– eliminacja błedów;

Łatwiej jest analizowa

Stolica(NY,US) ni

x = x+2

Programowanie logiczne: j

zyk PROLOG

Wnioskowanie bezpo

rednie w FOL

Przekształcenie algorytmów wnioskowania w taki
sposób, aby mo

na było prowadzi

wnioskowanie

w bazie FOL pozwala u

efektywnych metod

wnioskowania w przód i wstecz, a tak

e algorytmu

eliminacji (rezolucji) dla bazy w postaci Horna.

Przekształcenie algorytmów polega na zastosowaniu
operacji podniesienia i unifikacji oraz wykorzystanie

F.A. Dul 2007

operacji podniesienia i unifikacji oraz wykorzystanie
uogólnionej reguły odrywania.

Wnioskowanie przy u

yciu algorytmów

dostosowanych do FOL mo

e by

bardzo efektywne.

Wnioskowanie mo

e by

w pełni automatyczne.

Wnioskowanie automatyczne stwarza mo

liwo

ść

automatycznego dowodzenia twierdze

matematycznych.

9.6. Automatyczne dowodzenie twierdze

Programy dowodzenia twierdze

(

Theorem Provers

Automated Reasoners

) umo

liwiaj

dowodzenie twierdze

sformułowanych w j

zyku logiki pierwszego rz

du.

Najbardziej znane programy: O

TTER

, PTTP, O

NTIC

, S

URA

, EQP, S

PIN.

Idea programu O

TTER

Dane definiuj

ce dowodzony problem:

• Zbiór zda

opisuj

cych problem

(set of support, SOS)

• Aksjomaty u

ytkowe

, nie b

ce elementami SOS,

• Aksjomaty u

ytkowe

, nie b

ce elementami SOS,

opisuj

ce wiedz

ogóln

na temat problemu.

• Zbiór równa

demoduluj

cych (

demodulators

)

okre

laj

cych formy kanoniczne do których przekształcane

wszystkie zdania (np. x+0=x: x+0

→

x).

• Zbiór parametrów i klauzul steruj

cych.

Program O

TTER

stosuje rezolucj

do kolejnych zda

zbioru

opisuj

cego SOS wzgl

dem aksjomatów u

ytkowych.

Rezolucja klauzul SOS przebiega w kolejno

ci od najprostszej,

wybieranej heurystycznie za pomoc

algorytmu best-first.

Programy dowodzenia twierdze

pozwoliły uzyska

wiele

nych wyników matematycznych.

• 1969 – program S

udowadnia kilka lematów teorii warstw.

• 1979 – Natarjan Shankar przy u

yciu programu Boyera-

Moora dowodzi po raz pierwszy w sposób

cisły słynne

Twierdzenie Gödla o Niezupełno

ci.

• 1983 – program A

URA

udowadnia twierdzenia z wielu

dziedzin matematyki.

• Program O

TTER

(i jego nowsze wersje: M

ACE

2, EQP) jest

jednym z najlepszych programów dowodzenia twierdze

9.6. Automatyczne dowodzenie twierdze

jednym z najlepszych programów dowodzenia twierdze

Za pomoc

EQP dowiedziono w roku 1996 słynnej

hipotezy

Robbinsa

(o równowa

ci algebry Robbinsa i algebry

boolowskiej), nieudowodnionej od roku 1933, nawet przez

samego

Alfreda Tarskiego*

)

. Dowód uzyskany programem

EQP liczy tylko

17 linijek!

*) Alfred Tarski

(1901-1983) – wybitny polski logik,

wykładowca UW i liceum

eromskiego (do 1939),

oraz uniwersytetów Harvarda, Princeton i Berkeley.

Jako pierwszy sformułował definicj

prawdy.

Uwa

any za najwi

kszego logika po Arystotelesie.

Program dowodz

ce s

ywane w ró

nych dziedzinach

jako

asystenci

Człowiek-ekspert nadzoruje rozwi

zanie problemu wytyczaj

kierunki działa

, za

program-asystent rozwi

zuje problemy

szczegółowe.

Innymi zastosowaniami programów dowodz

cych

weryfikacja

oraz

synteza

układów elektronicznych

oraz oprogramowania.

• Program A

URA

posłu

ył do weryfikacji 16-bitowego układu

9.6. Automatyczne dowodzenie twierdze

• Program A

URA

posłu

ył do weryfikacji 16-bitowego układu

sumuj

cego (1983).

• Specjalne programy dowodz

ce słu

Ŝą

do weryfikacji

poprawno

ci układów VLSI, np. procesorów CPU.

• Program S

słu

y do weryfikacji poprawno

oprogramowania.
Za jego pomoc

weryfikowano w NASA oprogramowanie

Remote Agent

steruj

ce lotem sond mi

dzyplanetarnych,

m.in. sondy Deep Space 1 (1999).

Podsumowanie

• Algorytmy wnioskowania w logice pierwszego rz

nymi narz

dziami sztucznej inteligencji.

• Unifikacja pozwala znacznie zwi

kszy

efektywno

ść

wnioskowania w logice pierwszego rz

du.

• Uogólniona wersja Modus Ponens stanowi efektywn

reguł

wnioskowania w logice pierwszego rz

du.

• Algorytmy wnioskowania w przód i wstecz

najwa

niejszymi narz

dziami wnioskowania

najwa

niejszymi narz

dziami wnioskowania

automatycznego w logice pierwszego rz

du.

• Uogólnione zasady rezolucji pozwalaj

dowodzi

twierdze

w logice pierwszego rz

du w bazie wiedzy reprezentowanej

w postaci normalnej koniunktywnej.

• Automatyczne dowodzenie twierdze

umo

liwiło

udowodnienie interesuj

cych twierdze

matematycznych.

• Automatyczne dowodzenie twierdze

pomaga tak

przy syntezie i weryfikacji oprogramowania.