Automatyczne dowodzenie twierdzeń, Robotyka, Metody sztucznej inteligencji


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:

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ć:

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:

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:

Menu edytora:

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)
ojcem(Osoba,Osoba) /* ojcem osoby jest 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

  1. Cholewa W., Pedrycz W. Systemy doradcze, Skrypt Politechniki Śląskiej nr 1447, Gliwice 1987.

  2. Mulawka J.: Systemy ekspertowe, WNT Warszawa 1997

  3. Turbo Prolog Reference Guide v.2.0.

  4. 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



Wyszukiwarka

Podobne podstrony:
Indukcja drzew decyzyjnych, Robotyka, Metody sztucznej inteligencji
Zapis reguł dokładnych przy użyciu języka CLIPS, Robotyka, Metody sztucznej inteligencji
sztuczna--, Robotyka, Metody sztucznej inteligencji
streszczenie, Robotyka, Metody sztucznej inteligencji, Wykład
Indukcja reguł metodą generowania pokryć, Robotyka, Metody sztucznej inteligencji
sztuczna---, Robotyka, Metody sztucznej inteligencji
msi2, Automatyka i Robotyka, Semestr 4, Metody sztucznej inteligencji
sciaga msi, Automatyka i Robotyka, Semestr 4, Metody sztucznej inteligencji
msi ściąga test, Automatyka i Robotyka, Semestr 4, Metody sztucznej inteligencji
Sprawozdanie Zbiory Rozmyte Język R MSI, Automatyka i Robotyka, Semestr 4, Metody sztucznej intelige
Opracowanie na kolokwium, Automatyka i Robotyka, Semestr 4, Metody sztucznej inteligencji
ciąga ze sztucznej inteligencji, Automatyka i Robotyka, Semestr 4, Metody sztucznej inteligencji
Micha, Automatyka i Robotyka, Semestr 4, Metody sztucznej inteligencji
MSI-program-stacjonarne-15h-2011, logistyka, semestr IV, sieci neuronowe w log (metody sztucznej int
MSI oprac, Mechatronika, Metody Sztucznej Inteligencji, msi materiały
Metody sztucznej inteligencji
Sztuczna inteligencja wyklad 2, WI, Semestr III N2, Metody sztucznej inteligencji
Sztuczna inteligencja lab 1, WI, Semestr III N2, Metody sztucznej inteligencji

więcej podobnych podstron