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

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:

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:

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:

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:

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:

Różnica polega na innym zapisie symboli:

Operatory porównania stosowane do budowania reguł:

5.2.4. Goal

W sekcji goal ustala się cel wykonania programu, którym najczęściej jest sprawdzenie prawdziwości stwierdzenia.

Przykład: