Katedra Podstaw Konstrukcji Maszyn
Rok akademicki 1998/99
Metody i Techniki Sztucznej Inteligencji
Laboratorium nr 6
Automatyczne Dowodzenie Twierdzeń
1. Wprowadzenie
Celem ćwiczenia jest zapoznanie się z metodą automatycznego dowodzenia twierdzeń z wykorzystaniem języka Turbo Prolog.
Ćwiczenie obejmuje następujące zagadnienia:
pojęcie predykatu,
rachunek predykatów,
zasadę rezolucji,
wprowadzenie do języka Turbo Prolog,
automatyczne dowodzenie twierdzeń z wykorzystaniem języka Turbo Prolog.
2. Pojęcie predykatu
Przez predykat należy rozumieć nazwę reprezentującą własność lub relację.
Z punktu widzenia gramatyki predykat pełni rolę orzeczenia.
3. Rachunek predykatów
Rachunek predykatów jest rozszerzeniem rachunku zdań o dodatkowe kwantyfikatory: ∀ (dla każdego) i ∃ (istnieje). Z formalnego punktu widzenia predykat rozpatruje się jako funkcję odwzorowującą argumenty predykatu nazywane termami w wartość logiczną TRUE (prawda) lub FALSE (fałsz) i zapisuje się go podobnie jak funkcję w postaci PREDYKAT(ARGUMENT). Na przykład:
posiada_koła(samochód),
posiada_silnik(samochód),
jest_samochodem(fiatpunto).
Argumentami predykatu mogą być:
stałe (nazwy obiektów) jest_bratem(piotrek,paweł),
zmienne (symbole obiektów) jest_bratem(Osoba1,Osoba2) gdzie Osoba1 i Osoba2 są zmiennymi,
predykaty jest_samochodzem(posiada_koła(fiat) and posiada_silnik(fiat)).
Przyjmuje się zgodnie z ustaleniami dla języka PROLOG, że nazwy stałych rozpoczynane będą małą literą, a symbole zmiennych dużą literą.
Wyrażenia w rachunku predykatów nazywa się formułami. Najmniejsze wyrażenie czyli predykat z argumentami nazywa się formułą atomiczną. Budowane formuły mogą być negowane poprzez umieszczenie znaku negacji przed nią np.:
¬jest_samochodem(mig29).
Formuły mogą być łączone spójnikami rachunku zdań tworząc formuły złożone np.:
posiada_koła(Samochod) and posiada_silnik(Samochod).
Za pomocą formuł możemy budować reguły:
∀X[jest_samochodem(X) → posiada_silnik(X)]
co czytamy: dla każdego X jeżeli X jest samochodem to X posiada silnik.
4. Zasada rezolucji
Zasada rezolucji stosowana jest do weryfikacji hipotez na podstawie twierdzenia o dedukcji. Twierdzenie stosowane jest między innymi do automatyzacji procesu dowodzenia twierdzeń, które można sformułować następująco:
Jeżeli formuły {A1,A2,...,An} nie są sprzeczne, to formuła B jest ich konkluzją (tzn. wynika na podstawie przeprowadzonego wnioskowania z formuł A1,A2,...,An) wtedy i tylko wtedy, gdy formuły {A1,A2,...,An,¬B} są sprzeczne.
5. TURBO PROLOG
5.1. Wprowadzenie do programowania w języku Turbo Prolog
Język Prolog (ang. PROgramin in LOGig) należy do języków wysokiego rzędu. Programowanie w języku Prolog odbiega od metod programowania w językach C, Pascal czy innych, w których program realizowany jest jako ciąg odpowiednich działań w języku programowania.
Celem działania prostych programów napisanych w PROLOGu jest udzielenie odpowiedzi na pytanie, czy stwierdzenie sformułowane przez użytkownika uzupełniające zbiór innych stwierdzeń (aksjomatów) może być uznane za prawdziwe lub dla jakich warunków dane stwierdzenie może być uznane za prawdziwe.
Program w PROLOGu jest zapisem stwierdzeń o obiektach i relacjach (formalnych zależnościach) między obiektami oraz reguł dotyczących obiektów i relacji między nimi. Umożliwia on bezpośrednie zapisanie zdań rachunku predykatów w programie.
Program napisany w języku Turbo prolog przyjmuje postać:
domains Osoba, Sport = symbol predicates lubi(Osoba,Sport) cluases lubi(helena,tenis). lubi(jan,pilkenozna). lubi(tomek,koszykowke). lubi(piotrek,plywanie). lubi(bartek,X) if lubi(tomek,X).
|
Powyższy program jest zbiorem stwierdzeń, które w języku potocznym można zapisać następująco:
Helena lubi tenis, Jan lubi piłkę nożna, itd.
Zapisana jest także jedna reguła: lubi (bartek,X) if lubi (tomek,X) co można wypowiedzieć następująco - jeżeli Bartek lubi daną dyscyplinę sportu (X) to Tomek również ją lubi. Na tej podstawie jeżeli będziemy się chcieli dowiedzieć czy Bartek lubi koszykówkę to zadamy pytanie lubi (bartek, koszykowke)? Na postawione pytanie otrzymamy odpowiedź Tak. Na liście stwierdzeń nie znajdziemy takiego, które by wprost nas o tym informowało. Jednak ze stwierdzenia, że Tomek lubi koszykówkę i reguły lubi(bartek,X) if lubi(tomek,X) wynika, że Bartek też lubi koszykówkę.
Powyższy przykład programu jest jedynie drobnym przykładem zadań jakie można rozwiązywać stosując język prolog.
5.2. Części programu zapisanego w języku Turbo Prolog
Program zapisany w języku Turbo Prolog zawiera następujące części (sekcje)
5.2.1. Domains
Poniżej słowa kluczowego domains deklaruje się zmienne stosowane programie. Można stosować następujące typy zmiennych:
integer - liczby całkowite -32,768 do 32,768
char - pojedynczy znak
real - liczby zmiennoprzecinkowe ±1e-307 do ±1e+308
string - dowolny łańcuch tekstowy np. `Ala ma kota'
symbol - zmienna symboliczna. Może przyjmować wartości typu znakowego podobnie jak zmienna typu string. Różnica między typem string i symbol polega na tym, że niektórych wypadkach operacje na symbolach wykonywane są szybciej.
Przykład:
domains Osoba, Sport = symbol |
Możliwe jest definiowanie zmiennych złożonych, jednakże nie będą one stosowane podczas zajęć stąd w opisie zostały pominięte.
5.2.2. Predicates
Sekcja predicates zawiera deklaracje predykatów, do definicji których stosowane są zmienne zdefiniowane w sekcji domains.
Przykład:
predicates lubi (Osoba,Sport) |
Możliwe jest przeciążanie definicji predykatów tzn. definiowanie predykatów, które nazywają się tak samo a zawierają różną listę argumentów np.:
Przykład:
predicates lubi(Osoba,Sport) lubi(Osoba,Osoba) |
Definiowanie kilku predykatów o tych samych nazwach wymaga umieszczania ich deklaracji jedna pod drugą.
5.2.3. Clauses
Sekcja klauzul może zawierać zarówno stwierdzenia jak i reguły. Stwierdzenia i reguły zapisywane są przy użyciu wcześniej zadeklarowanych predykatów. Należy pamiętać, że zarówno stwierdzenia jak i reguły powinny być zakończone kropką.
Przykład:
lubi(jan,koszykowke). /*fakt*/ lubi(jan,X) if lubi (helena,X) and lubi (tomek,X). /*reguła*/ |
Powyższy zapis reguły nie jest do końca zgodny ze standardem języka prolog. Standardowy zapis reguły wyglądał by następująco:
likes(john,X) :- likes(eddie,X) , likes(tom,X). /*reguła*/ |
Różnica polega na innym zapisie symboli:
Komenda |
Standard |
Borland Turbo Prolog |
if (jeżeli) |
:- |
if |
and (logiczny iloczyn) |
, |
and |
or (suma logiczna) |
; |
or |
Operatory porównania stosowane do budowania reguł:
Operator porównania |
znaczenie |
< |
mniejszy |
<= |
mniejszy lub równy |
= |
równy |
> |
większy |
>= |
większy lub równy |
<> (><) |
różny od |
5.2.4. Goal
W sekcji goal ustala się cel wykonania programu, którym najczęściej jest sprawdzenie prawdziwości stwierdzenia.
Przykład:
domains Obiekt = symbol predicates ma_kola(Obiekt) ma_kierownice(Obiekt) ma_podwozie(Obiekt) ma_nadwozie(Obiekt) jest_samochodem(Obiekt) test(Obiekt) clauses ma_kola(maluch). ma_kierownice(maluch). ma_podwozie(maluch). ma_nadwozie(maluch). jest_samochodem(X) if ma_kola(X) and ma_kierownice(X) and ma_nadwozie(X) and ma_podwozie(X). test(X) if jest_samochodem(X) and write(X+ „jest samochodem”) goal test(maluch). |
W powyższym przykładzie sprawdzamy czy stwierdzenie „maluch jest samochodem” jest prawdziwe. Po uruchomieniu programu uzyskamy odpowiedź „Maluch jest samochodem”, co oznacza, że stwierdzenie jest_samochodem(maluch) jest prawdziwe.
Sekcja goal nie jest obowiązkowa w programie. Jeżeli jej nie umieścimy to zaraz po uruchomieniu programu pojawi się napis zachęty goal:.
Określenie celu wykonania programu w jego wnętrzu lub w linii komend jest równoważne tzn. uzyskamy taki sam wynik.
5.3. Obsługa kompilatora
Okno programu kompilatora podzielone jest na cztery podokna:
Editor - jest oknem edycyjnym, w którym wpisujemy kod programu
Dialog - jest oknem, w którym prowadzony jest dialog programu z użytkownikiem
Messages - jest oknem, w którym umieszczane są komunikaty odnośnie kompilacji programu,
Trace - jest oknem, w którym można śledzić wykonywania programu
Menu edytora:
utworzenie nowego pustego pliku File | New File
załadowanie nowego pliku File | Pick
zachowanie utworzonego pliku File | Save
kompilacja programu Compile Memory
uruchamianie programu Run
wejście do menu realizowane jest przyciskiem F10
powrót z menu do okna edycyjnego następuje po wybraniu w menu pozycji Edit.
5.3. Przykład programu
Zadanie:
Udowodnić, że dziadkiem Elżbiety jest Paweł jeżeli znane są fakty:
Adam, Henryk, Paweł, Krzysztof są mężczyznami,
Barbara, Anna, Elżbieta, Agnieszka są kobietami,
Barbara jest matką Elżbiety
Agnieszka jest matką Adama
Paweł jest ojcem Adama
Henryk jest ojcem Barbary
Paweł jest ojcem Anny
Adam jest ojcem Elżbiety
Wiadomo że:
bratem X jest Y jeżeli X jest mężczyzną i rodzicem X jest P oraz rodzicem Y jest P i dodatkowo X i Y są dwiema różnymi osobami.
siostrą X jest Y jeżeli Y jest kobietą i rodzicem X jest P oraz rodzicem Y jest P a ponadto X i Y są dwiema różnymi osobami.
wujkiem X jest U jeżeli rodzicem X jest P i bratem P jest U
dziadkiem X jest G jeżeli rodzicem P jest G i matką X jest P
Na podstawie powyższych stwierdzeń i reguł można zbudować program:
domains Osoba=symbol predicates mezczyzna(Osoba)
kobieta(osoba) matka(Osoba,Osoba) /*matką osoby jest osoba*/ rodzicem(Osoba,Osoba) /*rodzicem osoby jest osoba*/ siostra(Osoba,Osoba) /* siostrą osoby jest osoba*/ bratem(Osoba,Osoba) /*bratem osoby jest osoba*/ wujek(Osoba,Osoba) /* wujkiem osoby jest osoba*/ dziadek(Osoba,Osoba) /*dziadkiem osoby jest osoba*/ clauses mezczyzna(adam). mezczyzna(henryk). mezczyzna(pawel). mezczyzna(krzysztof).
kobieta(barbara). kobieta(anna). kobieta(elzbieta). kobieta(agnieszka).
matka(elzbieta,barbara). matka(adam,agnieszka).
ojcem(adam,pawel). ojcem(barbara,henryk). ojcem(anna,pawel). ojcem(elzbieta,adam).
rodzicem(X,Y) if matka(X,Y). rodzicem(X,Y) if ojcem(X,Y). bratem(X,Y) if mezczyzna(X) and rodzicem(X,P) and rodzicem(Y,P) and X<>Y. siostra(X,Y) if kobieta(X) and rodzicem(X,P) and rodzicem(Y,P) and X<>Y. wujkiem(X,U) if rodzicem(X,P) and bratem(P,U). dziadkiem(X,G) if ojcem(P,G) and rodzicem(X,P). goal dziadkiem(elzbieta,pawel). |
Po wykonaniu programu otrzymamy odpowiedź YES co oznacza, że na podstawie faktów i użytych reguł dowiedzione jest, że dziadkiem Elżbiety jest Paweł.
Możliwe jest również zapytanie kto jest bratem Anny po wydaniu komendy:
goal: bratem(anna,X) X=adam 1 solution |
W ten sposób otrzymaliśmy odpowiedź, że bratem Anny jest Adam
6. Zadania do wykonania
Na zajęciach laboratoryjnych należy dowieść prawdziwości zadanego stwierdzenia stosując w tym celu język programowania Prolog. Stwierdzenia i aksjomaty zostaną przekazane przez prowadzącego zajęcia.
Literatura
Cholewa W., Pedrycz W. Systemy doradcze, Skrypt Politechniki Śląskiej nr 1447, Gliwice 1987.
Mulawka J.: Systemy ekspertowe, WNT Warszawa 1997
Turbo Prolog Reference Guide v.2.0.
Turbo Prolog. The natural laguage of artificial intelligence. Borland International.
Instrukcje są dostępne w Internecie pod adresem:
http://www.kpkm.polsl.gliwice.pl/dydkpkm/mitsi/lab/
1/6