Reprezentacja wiedzy w języku logiki

(1)

Reprezentacja wiedzy w języku logiki

Metody przeszukiwania w przestrzeni stanów sformułowane były w postaci dość ogólnej, jednak wymagały reprezentacji zagadnienia we właściwej formie, tzn.

przestrzeni stanów, zbioru operatorów, a dodatkowo przydatna/potrzebna była informacja heurystyczna w formie funkcji oceny stanów.

Ogólnie, format i sposób reprezentacji wiedzy o zagadnieniu są niezwykle istotne i mają bezpośredni wpływ na efektywność — lub w ogóle zdolność — znalezienia rozwiązania.

Istnieje szereg opracowanych ogólnych podejść do problemu reprezentacji, i różne reprezentacje mają zwykle związane z nimi techniki wnioskowania, czyli formowania pewnych ustaleń pomocniczych (wniosków), mogących służyć do znalezienia

ostatecznego rozwiązania problemu.

Jednym z najpopularniejszych schematów reprezentacji wiedzy jest język logiki matematycznej.

Metody oparte na logice — reprezentacja wiedzy w języku logiki 1

Dlaczego logika matematyczna jest dobrym językiem reprezentacji wiedzy dla sztucznej inteligencji?

Z jednej strony, język logiki jest zbliżony do sposobu w jaki ludzie myślą o świecie, i myśli swe wyrażają w zdaniach języka naturalnego. Czasami mówi się kolokwialnie, że człowiek myśli „logicznie”. Kategorie, którymi myśli i mówi człowiek obejmują takie konstrukcje jak: obiekty, związki między obiektami (relacje), stwierdzenia faktów prostych i złożonych, zdania, spójniki zdaniowe, wyrażenia faktów warunkowych, a nawet kwantyﬁkatory.

Z drugiej strony, logika matematyczna dostarcza precyzyjnego aparatu wnioskowania opartego na dowodzeniu twierdzeń. Ludzie, myśląc, również stosują podobne

wnioskowanie logiczne, zatem aparat logiki matematycznej wydaje się dobrą platformą reprezentacji wiedzy agenta inteligentnego, którego sposób wyrażania faktów

i wnioskowania byłby zbliżony do ludzkiego.

Metody oparte na logice — reprezentacja wiedzy w języku logiki 2

(2)

Przykład: świat wumpusa

Do sprawdzenia działania wielu metod przydatne jest środowisko testowe dostatecznie proste, aby można było intuicyjnie określać właściwe reprezentacje i sprawdzać proste koncepcje, ale jednocześnie dostatecznie bogate, aby pozwoliło konfrontować te metody z coraz bardziej realnymi przeszkodami.

Jednym z takich testowych środowisk podręcznikowych jest świat wumpusa.¹ W tym środowisku porusza się agent dążący do znalezienia złota (i bezpiecznego wyniesienia go z jaskini). Na przeszkodzie stoją zapadliny (pits), w które agent może wpaść, i potwór (tytułowy wumpus), który może agenta zjeść.

Agent może jedynie obracać się w prawo lub w lewo, poruszać się po jednym kroku do przodu, wystrzelić z łuku jedyną posiadaną strzałę (na wprost), podnieść złoto, gdy je znajdzie, i wyjść z jaskini, jeśli znajduje się w punkcie startowym.

1Przedstawione tu przykłady i diagramy świata wumpusa zaczerpnięte zostały z podręcznika Russella i Norviga „Arti- ﬁcial Intelligence A Modern Approach” i materiałów udostępnionych na stronie internetowej Stuarta Russella.

Metody oparte na logice — świat wumpusa 3

Agent otrzymuje pewne informacje o środowisku (dane otrzymywane z receptorów agenta nazywa się perceptami): wyczuwa smród wumpusa (stench) i powiew

powietrza z zapadlin (breeze), jeśli znajduje się w polu sąsiadującym z nimi. Ponadto zauważa złoto (gold), ale tylko jeśli jest w tym samym polu co ono. Nie może jednak sprawdzić swojej bezwzględnej pozycji (à la GPS), może jedynie sam swoją pozycję rejestrować. Ściany jaskini wyczuwa jedynie przez próby wejścia w nie, które powodują odbicia.

Breeze Breeze

Breeze

Breeze Breeze

Stench

Breeze

PIT

1 2 3 4

START

Gold Stench

(3)

Przykład: poruszanie się w świecie wumpusa

A OK

OK OK

OK

OK OK

A

B OK

OK OK

A

A B

P?

OK

OK OK

A

A B

P?

A S

OK

OK OK

A

A B

P?

A S

OK

P

W

OK

OK OK

A

A B

P?

A S

OK

P

W

A

Przykład: poruszanie się w świecie wumpusa (cd.)

OK

OK OK

A

A B

P?

A S

OK

P

W

A

OK

OK OK

A

A B

P?

A S

OK

P

W

A

OK OK

OK

OK OK

A

A B

P?

A S

OK

P

W

A

OK OK

A BGS

Jednak nie zawsze można skutecznie działać w świecie wumpusa posługując się tylko wnioskowaniem logicznym.

W niektórych przypadkach jedynym rozwiązaniem jest

„strzelanie”, czyli wybór ruchu na ślepo, i dopiero potem analizowanie sytuacji.

Oczywiście o ile przeżyjemy!!

A B OK

OK OK

A B

A P?

P?

P? A

S

(4)

Rachunek predykatów pierwszego rzędu — termy

Termy reprezentują w języku logiki obiekty, i mogą być: stałymi (oznaczają konkretny obiekt), zmiennymi (mogą przybierać wartości różnych obiektów), lub funkcjami

(wyznaczają jakiś obiekt na podstawie wartości swoich argumentów, inaczej, przypisują jednym obiektom inne).

Przykłady termów: A, 123, x, f(A), f(g(x)), +(x, 1)

Umownie zapisujemy termy stałe wielkimi literami, a zmienne małymi.

Zauważmy, że w powyższych przykładach ostatni term jest niejawnym zapisem następnika x, a nie operacją odejmowania. W czystej logice nie ma odejmowania.

Będziemy mieli do czynienia z tym problemem w wielu sytuacjach.

Metody oparte na logice — rachunek predykatów 7

Rachunek predykatów pierwszego rzędu — predykaty

Predykaty reprezentują relacje na zbiorze termów. Możemy je traktować jako funkcje mające wartość prawdy lub fałszu (1 lub 0), które przypisują prawdę każdej n-ce

termów spełniających relację, a fałsz każdej n-ce niespełniającej.

Zapis predykatu z zestawem termów nazywamy formułą atomową.

Przykłady formuł atomowych: P , Q(A), R(x, f(A)), > (x, 10)

Zapis funkcyjny: > (x, 10) jest odpowiednikiem relacji: x > 10. W arytmetyce

potraktowalibyśmy taki zapis jako nierówność i moglibyśmy ją rozwiązywać. Natomiast formuły logiczne możemy jedynie wartościować, to znaczy wyznaczać ich wartość logiczną prawdy lub fałszu. Gdy formuła zawiera zmienną to często nie da się wyznaczyć jej wartości logicznej.

(5)

Reprezentacja faktów za pomocą formuł

Jaki sens ma język logiki predykatów?

Możemy przy jego użyciu opisać fakty, które chcemy wyrazić, np.:

At(W umpus, 2, 2) At(Agent, 1, 1) At(Gold, 3, 2)

Wybór zestawu symboli, którymi zamierzamy opisać obiekty i relacje pewnego świata, nazywamy konceptualizacją. Na przykład, alternatywna do powyższej

konceptualizacja świata wumpusa mogłaby zawierać formuły:

AtW umpus(loc(2, 2)) AtAgent(loc(1, 1)) AtGold(loc(3, 2))

Powyższe konceptualizacje są podobne, aczkolwiek mają nieco odmienne właściwości, np. w drugiej wumpus, agent, ani złoto nie wystąpią w jawnej postaci. Ogólnie od przyjętej konceptualizacji może zależeć łatwość, a nawet możliwość wyrażania różnych faktów o dziedzinie problemowej.

Reprezentacja faktów za pomocą formuł (cd.)

Przykładem problemu konceptualizacyjnego świata wumpusa jest opis istnienia i położenia dziur. Możemy nadać dziurom prawa obywatelskie i tożsamość:

At(P it⁴,3, 3)

W ten sposób możemy łatwo opisać cały świat widziany z lotu ptaka, nadając poszczególnym dziurom dowolnie wybrane nazwy (termy stałe). Z punktu widzenia agenta poruszającego się w świecie wumpusa ta konceptualizacja jest jednak bardzo niewygodna. Trudno byłoby w ten sposób opisać świat stopniowo poznawany, gdy na początku agent nie zna nawet liczby dziur. Istnienie dziury trzeba wtedy opisać zmienną:

At(x, 3, 3)

Jednak z tego zapisu nie wynika, że x jest dziurą i wymaga to uzupełniających opisów.

Wygodną alternatywą jest postrzeganie dziur jako anonimowych, i tylko zapisywanie faktów istnienia lub nieistnienia dziur w konkretnych miejscach:

P itAt(3, 3) N oP itAt(1, 1)

(6)

Spójniki logiczne i formuły złożone

Formuły złożone języka predykatów pierwszego rzędu można konstruować za pomocą spójników logicznych takich jak: ¬, ∧, ∨, ⇒, ⇔. Jako szczególny przypadek, formułę która jest formułą atomową lub negacją formuły atomowej nazywamy literałem.

Przykłady formuł złożonych (pierwsza jest pojedynczym literałem):

¬At(W umpus, 1, 1) P itAt(2, 1) ∨ P itAt(1, 2)

[At(Agent, 1, 1) ∧ P itAt(2, 1)] ⇒ P ercept(Breeze)

Zauważmy, że ostatnia formuła jest zupełnie innej natury, niż dwie pierwsze. Dwie pierwsze formuły mogą stanowić fragment opisu świata otrzymanego i/lub

budowanego przez agenta inteligentnego w trakcie jego pracy w świecie wumpusa.

Natomiast ostatnia formuła wyraża jedno z praw świata wumpusa. Agent zna to prawo, i może posiadać taką formułę w swojej bazie wiedzy.

Fakty ogólnie słuszne w danej dziedzinie problemowej nazywamy aksjomatami świata. Natomiast fakty opisujące stan konkretnej instancji problemu, nazywamy incydentalnymi.

Warto jeszcze podkreślić, że ⇒ i ⇔ są tylko spójnikami logicznymi, tworzącymi z pary dowolnych formuł formułę złożoną. Nie mają one nic wspólnego z procesem

wnioskowania, który będzie rozważany poniżej.

(7)

Kwantyﬁkatory

Formuły złożone można również budować za pomocą kwantyﬁkatorów: ∀, ∃, które wiążą zmienne w formułach. Ogólny schemat formuły z kwantyﬁkatorem:

∀xP (x)

Zmienną niezwiązaną kwantyﬁkatorem w formule nazywamy wolną. Formuła:

∃yQ(x, y)

zawiera dwie zmienne, jedną wolną, a drugą związaną kwantyﬁkatorem.

Zdaniem nazywamy formułę bez wolnych zmiennych.

Przykłady:

∃x, y At(Gold, x, y)

∀x, y [At(W umpus, x, y) ∧ At(Agent, x, y)] ⇒ AgentDead

∀x, y [At(W umpus, x, y) ∧ At(Agent, −(x, 1), y)] ⇒ P ercept(Stench) Zwróćmy uwagę, że w ostatnim przykładzie −(x, 1) jest niejawnym zapisem współrzędnej na lewo od x, a nie odejmowaniem. W logice nie ma odejmowania.

Krótkie podsumowanie — pytania sprawdzające

1. Opracuj kompletną konceptualizację świata wumpusa w rachunku predykatów pierwszego rzędu. To znaczy: wprowadź symbole termów (stałych i funkcji

termowych), oraz symbole predykatów niezbędne do opisywania instancji problemów w tej dziedzinie.

Uwaga: nie rozważamy procesu poszukiwania rozwiązania, analizy alternatywnych ruchów i ich skutków, opisywania sekwencji kroków, itp. Poszukujemy jedynie formatu pozwalającego na statyczny opis stanu zagadnienia, tzw. snapshot.

2. Wykorzystując reprezentację opracowaną w poprzednim punkcie, opisz instancję problemu przedstawioną na stronie 4.

3. Spróbuj zapisać aksjomatykę świata wumpusa, to znaczy: ogólne reguły rządzące tym światem.

(8)

Semantyka — interpretacje

Deﬁnicja języka predykatów określiła jedną składową reprezentacji, tzn. jego składnię, inaczej syntaktykę. Drugą składową jest semantyka, czyli aparat pozwalający określać znaczenia.

Na pozór, znaczenie niektórych formuł mogłoby wydawać się jasne. Dotychczas intuicyjnie domyślaliśmy się co znaczy At(Agent, 2, 2). W ogólności to jednak nie wystarczy. Nawet ograniczając się do świata wumpusa, nie wiadomo której tury gry i którego stanu tej gry dotyczy podana formuła.

Interpretacja – przypisanie syntaktycznym elementom języka predykatów (termom i predykatom) obiektów z jakiejś konkretnej dziedziny (świata).

W oczywisty sposób, konkretna formuła zapisana przy użyciu pewnego zestawu

symboli może dotyczyć różnych dziedzin. Na przykład, formuła At(Agent, 2, 2) może odnosić się do pewnej tury wumpusa, sceny z ﬁlmu o agencie 007, jakiegoś agenta ze świata rzeczywistego, albo jeszcze innego agenta.

Możliwych interpretacji dla danej formuły może być bardzo wiele.

Metody oparte na logice — semantyka rachunku predykatów 15

Modele

Zauważmy, że interpretacja określa prawdziwość formuł atomowych. Jeśli w danej dziedzinie zachodzi relacja między pewnymi obiektami, to formuła zapisująca to za pomocą odpowiednich termów i predykatu jest prawdziwa w tej interpretacji.

Również na odwrót, mając zapisaną dowolną formułę, możemy wyznaczyć jej wartość logiczną sprawdzając czy w danej interpretacji zachodzi opisany przez formułę związek.

(Jednak gdy formuła zawiera zmienne wolne to jej prawdziwość może nie być określona przez interpretację.)

Konsekwentnie, korzystając z deﬁnicji spójników logicznych i kwantyﬁkatorów możemy wyznaczyć wartość logiczną dowolnej formuły (zdania) dla danej interpretacji. Możemy więc mówić, że interpretacje określają prawdziwość formuł zdaniowych (bez zmiennych wolnych).

Interpretację przypisującą danej formule wartość prawdy logicznej nazywamy interpretacją spełniającą, albo modelem tej formuły.

(9)

Spełnialność

Formułę nazywamy spełnialną, jeśli istnieje interpretacja spełniająca, czyli

przypisująca jej wartość prawdy logicznej (inaczej: jeśli istnieje model tej formuły).

Formuła jest niespełnialna, jeśli nie istnieje żadna spełniająca ją interpretacja

(model). Z kolei, jeśli formuła ma wartość prawdy dla każdej możliwej interpretacji, to nazywamy ją tautologią, albo formułą prawdziwą.

Rozważmy przykłady:

At(W umpus, 2, 2)

∃x, y At(Gold, x, y)

∀x, y [At(W umpus, x, y) ∧ At(Agent, x, y)] ⇒ AgentDead

Wszystkie podane formuły są spełnialne, ponieważ bez trudu możemy stworzyć sobie instancję świata wumpusa, w której będą zachodziły podane fakty. Jednak żadna nie jest tautologią. Co prawda ostatnie dwie formuły są prawdziwe w każdej instancji rozgrywki zgodnej z prawami świata wumpusa. Jednak bez trudu możemy wymyślić inny, podobny świat, gdzie nie będą one obowiązywały.

Przykładem tautologii może być znacznie mniej interesująca, chociaż

z matematycznego punktu widzenia fascynująca formuła: P∨¬P, gdzie P jest dowolnym 0-argumentowym predykatem, czyli stwierdzeniem dowolnego faktu.

Krótkie podsumowanie — pytania sprawdzające

1. Dla podanych poniżej formuł rachunku predykatów odpowiedz, czy dana formuła jest: spełnialna, niespełnialna, tautologią.

(a) P (b) P (x)

(c) ∀x P (x) (d) ∃x P (x)

(e) [P ⇒ Q] ∧ P ∧ ¬Q (f) [P ⇒ Q] ⇔ [¬P ∨ Q]

(10)

Wynikanie logiczne

W wielu sytuacjach agent chciałby przeprowadzić jakieś wnioskowanie. Na przykład:

w celu stwierdzenia zachodzenia faktów, o których agent nie ma informacji, ale które mogą wynikać z innych informacji, które agent posiada. Takie przypadki widzieliśmy na przykładach ze świata wumpusa. Inną sytuacją gdy agent mógłby chcieć wyciągać wnioski jest próba określenia możliwych skutków swoich działań — pożądanych bądź niepożądanych.

Chcemy mieć możliwość efektywnego sprawdzania, czy jedne fakty wynikają z innych.

Jednak logika pozwala jedynie określać wynikanie formuł.

Wynikanie logiczne formuły ϕ ze zbioru formuł ∆ zachodzi, gdy każda interpretacja spełniająca wszystkie formuły z ∆ spełnia też formułę ϕ, co zapisujemy:

∆ |= ϕ

Dlaczego właśnie tak deﬁniujemy wynikanie? Bo chcemy mieć uniwersalny aparat logiczny, prowadzący procesy wnioskowania poprawne dla wszystkich możliwych interpretacji. Ponieważ operujemy na formułach, chcemy mieć pewność, że proces wnioskowania jest słuszny również dla konkretnej dziedziny problemowej, z która ma do czynienia agent.

Metody oparte na logice — wnioskowanie 19

Dygresja — rachunek zdań

W logice istnieje język prostszy od rachunku predykatów zwany rachunkiem zdań.

Nie istnieją w nim termy, zatem predykaty ograniczone są do predykatów

0-argumentowych, zwanych zdaniami. Formuły atomowe stanowią pojedyncze symbole zdaniowe, a formuły złożone można budować za pomocą spójników, podobnie jak w rachunku predykatów. Kwantyﬁkatorów nie ma.

Semantyka rachunku zdań jest bardzo uproszczona. Zamiast rozpatrywać wszystkie możliwe interpretacje danej formuły wystarczy podzielić je na grupy, w których poszczególne symbole zdaniowe są prawdziwe lub nieprawdziwe. W efekcie, zamiast rozpatrywać interpretacje, można badać wszystkie możliwe kombinacje prawdy i fałszu symboli zdaniowych. Prostą procedurą takiego badania jest budowanie tabelek

zerojedynkowych.

W rachunku predykatów nie jest to możliwe, ponieważ wartość logiczna formuły zależy od wartości termów, które są argumentami predykatów. Niestety, rachunek zdań jest zbyt słaby (mówimy: niedostatecznie ekspresyjny) dla zastosowań praktycznych.

(11)

Reguły wnioskowania

Sprawdzanie wynikania przez interpretacje i niespełnialność może być uciążliwe. Jest to spowodowane koniecznością uwzględnienia wszystkich możliwych interpretacji, których może być bardzo dużo.

Zamiast sprawdzania wynikania logicznego, w logice stosuje się podejście zwane dowodzeniem twierdzeń. Wprowadza się reguły wnioskowania, które pozwalają z jednych formuł tworzyć inne za pomocą syntaktycznych przekształceń.

Na przykład, jedna z podstawowych reguł wnioskowania zwana modus ponens, albo regułą odrywania, ma postać:

ϕ, ϕ⇒ ψ ψ

W przypadku gdyby agent posiadał fakty: Susza i Susza ⇒ NiskieP lony, to podstawiając je do powyższego schematu miałby prawo wywieść nowy fakt:

N iskieP lony.

Dowodzenie twierdzeń

Dowodem formuły ϕ dla zbioru formuł ∆, zwanego zbiorem aksjomatów,

nazywamy ciąg formuł, z których ostatnią formułą jest ϕ, a z których każda spełnia jeden z warunków:

1. jest tautologią,

2. jest jednym z aksjomatów,

3. jest formułą otrzymaną z formuł poprzedzających ją w dowodzie (leżących bardziej na lewo) za pomocą jednej z posiadanych reguł wnioskowania.

Twierdzeniem zbioru formuł ∆ nazywamy każdą formułę ϕ która posiada dowód dla zbioru ∆. Wtedy mówimy, że formułę ϕ można wywieść ze zbioru aksjomatów ∆, co zapisujemy:

∆ ⊢ ϕ

Zbiór wszystkich twierdzeń zbioru formuł ∆ nazywamy teorią tego zbioru i oznaczamy T (∆).

(12)

Wnioskowanie przez dowodzenie twierdzeń

Początkowo wprowadziliśmy wynikanie logiczne (∆ |= ϕ) jako metodę wnioskowania, tzn. stwierdzania wynikania faktów. Jednak brak było wygodnej procedury efektywnego obliczania tego wynikania.

Dowodzenie twierdzeń (∆ ⊢ ϕ) oferuje potencjalnie dobrą procedurę wnioskowania dla agenta posługującego się logiką jako językiem reprezentacji. Chcąc wywieść jakiś pożądany fakt ze zbioru aksjomatów można w najgorszym przypadku systematycznie generować wszystkie możliwe skończone ciągi formuł spełniających deﬁnicję dowodu tego faktu. Jeśli istnieje dowód o długości N, to w tej procedurze zostanie on

wygenerowany. To już lepiej niż sprawdzanie wszystkich interpretacji, które nawet trudno sobie wyobrazić.

Jednak czy dowodzenie twierdzeń jest równie dobrą metodą sprawdzania wynikania faktów, które zachodzą w rzeczywistej dziedzinie problemowej?

Nie jest to wcale oczywiste.

Systemy dowodzenia twierdzeń

W logice zdeﬁniowano szereg systemów dowodzenia twierdzeń wprowadzających różne zestawy reguł wnioskowania, a także pewne formuły początkowe, które można w nich stosować (aksjomaty). W tym wykładzie nie będziemy zagłębiać się

w konstrukcję tych systemów, jednak musimy znać i rozumieć pewne ich własności.

Reguła wnioskowania jest poprawna jeśli można za jej pomocą wywieść fałsz jedynie z niespełnialnego zbioru przesłanek.

Zbiór reguł wnioskowania jest kompletny jeśli można z jego pomocą wywieść fałsz z każdego niespełnianego zbioru przesłanek.

System dowodzenia twierdzeń jest pełny jeśli jest poprawny i kompletny. W takim systemie ze zbioru przesłanek można wywieść fałsz wtedy i tylko wtedy gdy zbiór ten jest niespełnialny (pod warunkiem, że są to formuły zamknięte).

A więc to co byłoby potrzebne agentowi inteligentnemu, to jest pełny system dowodzenia twierdzeń, z efektywną obliczeniowo procedurą dowodową.

(13)

Krótkie podsumowanie — pytania sprawdzające

1. Wyjaśnij dlaczego wnioskowanie agenta o jego świecie powinno być oparte o wynikanie logiczne.

2. Na czym polega dowodzenie twierdzeń i jaką rolę pełnią w nim reguły wnioskowania?

3. Kiedy możemy zastosować dowodzenie twierdzeń w celu wnioskowania o własnościach zachodzących w jakiejś dziedzinie problemowej?

4. Odpowiedz czy zachodzą poniższe własności (w przypadku dowodliwości ⊢ przyjmij, że jedyną możliwą regułą dowodzenia jest modus ponens: ^ϕ,ϕ⇒ψ_ψ ):

{P, P ⇒ Q} |= P {P, P ⇒ Q} ⊢ P {P, P ⇒ Q} |= Q {P, P ⇒ Q} ⊢ Q {P, P ⇒ Q} |= P ∧ Q {P, P ⇒ Q} ⊢ P ∧ Q

Nie jest konieczne przeprowadzenie formalnego dowodu każdego z powyższych przypadków, wystarczy półformalne słowne uzasadnienie.

(14)

Postać dysjunkcyjna normalna (DNF)

Procedury automatycznego przetwarzania formuł logicznych wymagają zapisywania formuł w pewnych standardowych postaciach normalnych.

Formuły atomowe i ich negacje nazywamy literałami, np.: P, ¬Q(x, f(a)).

Formuła jest w postaci DNF (Disjunctive Normal Form) jeśli jest alternatywą koniunkcji literałów. Zarówno alternatywę jak i koniunkcję traktujemy tutaj jako spójniki n-arne, dla dowolnego n, niekoniecznie binarne, korzystając z ich łączności.

Dla każdej formuły logicznej istnieje równoważna jej logicznie formuła w postaci DNF.

Na przykład, formuła (¬P ∧ Q) ∨ R jest już w postaci DNF, natomiast formułę

¬P ∧ (Q ∨ R) można przekształcić do postaci DNF korzystając z rozdzielności koniunkcji względem alternatywy: (¬P ∧ Q) ∨ (¬P ∧ R).

Przekształcenie formuły do postaci DNF nie jest jednoznaczne; może istnieć wiele formuł w postaci DNF równoważnych danej formule.

Metody oparte na logice — postaci normalne formuł 27

Przekształcanie formuł do DNF

Jedną szczególną konstrukcję postaci DNF można otrzymać z zerojedynkowej tabelki deﬁniującej prawdziwość formuły w zależności od prawdziwości wchodzących w jej skład formuł atomowych.

Przykład:

(P ⇒ Q) ∧ (Q ⇒ P )

P Q P ⇒ Q Q ⇒ P (P ⇒ Q) ∧ (Q ⇒ P )

0 0 1 1 1

0 1 1 0 0

1 0 0 1 0

1 1 1 1 1

Wybierając wiersze tabeli, dla których formuła ma wartość prawdy (jedynka w ostatniej kolumnie), konstruujemy formułę w postaci DNF:

(¬P ∧ ¬Q) ∨ (P ∧ Q)

(15)

Postać koniunkcyjna normalna (CNF)

O formule, która jest koniunkcją alternatyw literałów mówimy, że jest w postaci CNF (Conjunctive Normal Form). Formuły, która są alternatywami literałów nazywamy klauzulami. Zatem formuła w postaci CNF jest koniunkcją klauzul. (Dlatego skrót CNF bywa również rozwijany jako Clausal Normal Form).

Przykład formuły w postaci CNF: (P ∨ Q ∨ ¬R) ∧ (P ∨ ¬Q ∨ R). CNF jest analogiczną, dualną do postaci DNF formą zapisu formuł. Może ona początkowo wydawać się mniej intuicyjna, jest jednak znacznie bardziej przydatna w systemach automatycznego dowodzenia twierdzeń.

Na przykład, postać CNF jest modularna, tzn. gdy chcemy dodać do posiadanej formuły w postaci CNF jakiś nowy fakt w postaci innej formuły CNF, to operacja ta jest trywialna i nie narusza postaci dotychczas posiadanej formuły, w odróżnieniu od DNF.

Przekształcanie formuł do CNF

Rozważmy ponownie przykładową formułę i jej zerojedynkową tabelę prawdy:

(P ⇒ Q) ∧ (Q ⇒ P )

P Q P ⇒ Q Q ⇒ P (P ⇒ Q) ∧ (Q ⇒ P )

0 0 1 1 1

0 1 1 0 0

1 0 0 1 0

1 1 1 1 1

Analogicznie do algorytmu konstrukcji postaci kanonicznej DNF formuły, możemy skonstruować postać CNF biorąc wiersze z zerową wartością formuły, i konstruując klauzule eliminujące te wiersze:

(¬P ∨ Q) ∧ (P ∨ ¬Q)

(16)

Puste koniunkcje i puste klauzule

Możemy mówić o pojedynczych literałach jako o 1-arnych (unarnych) koniunkcjach klauzul, albo klauzulach (alternatywach literałów). Co więcej, dopuszczamy również klauzule, oraz koniunkcje klauzul, 0-arne, czyli puste.

p1∧ p²∧ ... ∧ pn = ∧(p¹, p2, ..., p_n) p¹ ∨ p²∨ ... ∨ pn = ∨(p¹, p2, ..., p_n)

p∧ q = ∧(p, q) p∨ q = ∨(p, q)

p = ∧(p) p = ∨(p)

␣ = ∧() ␣ = ∨()

Zauważmy, że o ile prawdziwość niepustych koniunkcji lub klauzul zależy od

prawdziwości ich elementów, to puste koniunkcje oraz klauzule powinny mieć jakąś stałą interpretację logiczną. Przez proste uogólnienie deﬁnicji prawdziwości spójników możemy otrzymać fakt, że pusta koniunkcja jest formułą prawdziwą (tautologią), natomiast pusta klauzula jest formułą fałszywą (niespełnialną).

Przy zapisie formuł logicznych w postaci zbiorów lub list, puste koniunkcje i klauzule pojawiają się jako zbiory puste {} lub puste listy: () oraz NIL. Dodatkowo stosuje się symbol ✷ dla zapisu pustej klauzuli w notacji logicznej.

Przykład:

Weźmy formułę (P ∧ Q) zapisaną w postaci zbioru klauzul (jednoliterałowych):

{P, Q}. Dodanie do tego zbioru koniunkcji pustej: {P, Q} ∪ {} odpowiada w notacji logicznej operacji: (P ∧ Q) ∧ T ≡ (P ∧ Q) (gdzie T symbolizuje prawdę). Potwierdza to słuszność interpretacji pustej koniunkcji jako tautologii.

Analogicznie, możemy zapisać klauzulę (P ∨ Q) w postaci zbioru literałów: {P, Q}.

Dodanie do tego zbioru klauzuli pustej: {P, Q} ∪ {} odpowiada w notacji logicznej operacji: (P ∨ Q) ∨ F ≡ (P ∨ Q) (gdzie F symbolizuje fałsz). Tak więc również interpretacja pustej klauzuli jako formuły fałszywej jest poprawna.

(17)

Przekształcanie formuł logicznych do postaci klauzulowej

Formułę bez zmiennych wolnych możemy przekształcić do postaci klauzulowej (inaczej: prenex) gdzie wszystkie kwantyﬁkatory zapisane są przed formułą:

(i) przemianuj zmienne związane kwantyﬁkatorami na unikalne, (ii) zastąp koniunkcjami i alternatywami pozostałe spójniki logiczne, (iii) przesuń negacje do wewnątrz formuł (do symboli predykatów), (iv) wyodrębnij kwantyﬁkatory poza formułę,

(v) przekształć formułę do postaci koniunkcyjnej (CNF),

(vi) zastąp wszystkie kwantyﬁkatory egzystencjalne funkcjami Skolema.

Pierwsze pięć kroków są równoważnościowymi przekształceniami logicznymi (przy zachowaniu właściwej kolejności wyodrębnianych kwantyﬁkatorów w kroku (iv)). Krok (vi), tzw. skolemizacja, polega na zastąpieniu formuł postaci:

∀x¹∀x²...∀x_n∃y Φ(x¹, x2, ..., x_n, y) formułą

∀x¹∀x²...∀x_n Φ(x¹, x2, ..., x_n, f_y(x¹, x2, ..., x_n))

gdzie f_y jest nowo wprowadzonym symbolem funkcyjnym zwanym funkcją Skolema.

(W przypadku braku kwantyﬁkatorów ∀ będzie to stała Skolema.)

Twierdzenie Skolema

Ostatni krok w algorytmie przekształcenia formuły do postaci klauzulowej nie jest równoważnościowym przekształceniem logicznym. To znaczy, dla oryginalnej formuły logicznej Φ, i otrzymanej w wyniku przekształcenia jej postaci klauzulowej Φ^′,

w ogólności Φ 6≡ Φ^′.

Zachodzi jednak następująca własność, zwana twierdzeniem Skolema: dla

zamkniętej formuły Φ, jeśli Φ^′ jest jej postacią klauzulową, to Φ jest spełnialna wtedy i tylko wtedy gdy Φ^′ jest spełnialna.

Zatem, o ile nie możemy w ogólności posługiwać się postacią klauzulową Φ^′ zamiast oryginalnej formuły Φ, to jednak możemy posługiwać się tą postacią

dla celów dowodzenia spełnialności (lub niespełnialności).

Istnieje niezwykle przydatny schemat wnioskowania, wykorzystujący formuły w postaci klauzulowej, zapisywane często w postaci zbioru (lub listy) klauzul, gdzie poszczególne klauzule są zapisane w postaci zbiorów (lub list) literałów.

(18)

Krótkie podsumowanie — pytania sprawdzające

Przekształć do postaci prenex następujące formuły rachunku predykatów:

1. ∀x [(P (x) ⇒ Q(x)) ∧ (P (x) ⇒ R(x))]

2. ∀x [(P (x) ∧ Q(x)) ∨ (R(x) ∧ S(x))]

3. ∀x∃y [P (x) ⇒ Q(x, y)]

4. ∃x∀y [P (x, y) ⇒ Q(A, x)]

5. ∀x∃y [P (x, y) ⇒ Q(y, f(y))]

(19)

Rezolucja — przypadek klauzul podstawionych

Rezolucja dla dwóch klauzul podstawionych: gdy istnieje wspólny literał mający w dwóch klauzulach przeciwne znaki, to rezolucja tworzy nową klauzulę, zwaną rezolwentą, będącą połączeniem oryginalnych dwóch klauzul z wyłączeniem wspólnego literału.

Rozważmy przykład, dla klauzul:

P ∨ Q(A) oraz ¬S ∨ ¬Q(A) rezolucja utworzy rezolwentę P ∨ ¬S.

Zauważmy, że dla par klauzul: (P ∨ Q(A)), (¬S ∨ Q(A)) jak również dla:

(P ∨ Q(A)), (¬S ∨ ¬Q(B)) nie istnieją wspólne literały o przeciwnych znakach, zatem wykonanie rezolucji dla tych par klauzul nie jest możliwe.

Fakt: rezolwenta zawsze wynika logicznie z połączenia (koniunkcji) klauzul wyjściowych, zatem jako reguła wnioskowania rezolucja jest poprawna (sound).

Metody oparte na logice — rezolucja 37

Ciekawe przypadki szczególne rezolucji (symbol ❀ oznacza tu możliwość wykonania rezolucji i otrzymania wskazanego wyniku):

P oraz ¬P ∨ Q ❀ Q modus ponens

P ∨ Q oraz ¬P ∨ Q ❀ Q mocniejsza wersja P ∨ Q oraz ¬P ∨ ¬Q ❀ P ∨ ¬P tautologia

P ∨ Q oraz ¬P ∨ ¬Q ❀ Q ∨ ¬Q -”-

P oraz ¬P ❀ N IL sprzeczność

¬P ∨ Q oraz ¬Q ∨ R ❀ ¬P ∨ R przechodniość

(P ⇒ Q) (Q ⇒ R) (P ⇒ R) implikacji

(20)

Krótkie podsumowanie — pytania sprawdzające

Dla poniższych zbiorów formuł, zapisz wszystkie możliwe do otrzymania rezolwenty.

Jeśli nie jest możliwe wykonanie rezolucji, to wyjaśnij dlaczego nie. Porównaj otrzymane rezolwenty z wnioskami logicznymi, które możesz wyciągnąć intuicyjnie z podanych formuł.

Zwróć uwagę na przecinki, aby prawidłowo odczytać formuły w zbiorach.

1. { P ∨ Q ∨ R , ¬P ∨ ¬Q ∨ ¬R } 2. { P ∨ Q , P ∨ ¬Q , ¬P ∨ Q } 3. { P ⇒ (Q ∨ R) , ¬Q ∧ ¬R } 4. { P ⇒ Q , R ⇒ Q , P ∨ R }

(21)

Podstawienia zmiennych w formułach

Będziemy rozważali przekształcenia formuł polegające na zastępowaniu zmiennych w formułach innymi wyrażeniami (termami). Ponieważ zmienne w formułach w postaci prenex domyślnie związane są kwantyﬁkatorami uniwersalnymi, zastępowanie

zmiennych innymi termami oznacza branie szczególnych przypadków formuły.

Podstawieniem (substitution) nazwiemy zbiór odwzorowań określających termy podstawiane pod poszczególne zmienne. Podstawiane termy nie mogą zawierać zastępowanej zmiennej. Przykład podstawienia: s = {x 7→ A, y 7→ f(z)}.

Wykonanie podstawienia polega na syntaktycznym zastąpieniu wszystkich

wystąpień danej zmiennej w formule związanym z nią termem. Wszystkie zastąpienia wykonywane są jednocześnie, czyli wynikiem wykonania podstawienia

s= {x 7→ y, y 7→ A} na termie f (x, y) będzie term f (y, A).

Zauważ, że w ten sposób nie ma znaczenia w jakiej kolejności zmienne są zastępowane, pomimo iż podstawienie jest zbiorem (nieuporządkowanym).

Metody oparte na logice — uniﬁkacja 41

Złożeniem podstawień s¹ i s² (zapisywanym: s¹s2) nazwiemy podstawienie uzyskane przez zastosowanie podstawienia s² do termów z s¹, oraz dopisanie do otrzymanego zbioru wszystkich par z s² ze zmiennymi nie występującymi w s¹.

Φs¹s2 = (Φs¹)s² s1(s²s3) = (s¹s2)s³

(22)

Uniﬁkacja

Uniﬁkacją nazywamy takie podstawienie termów pod zmienne w zbiorze formuł, aby sprowadzić wszystkie formuły w zbiorze do identycznych (lub równoważnych logicznie, patrz wyjaśnienie niżej) formuł, czyli zbioru singletonowego.

Uniﬁkator zbioru formuł to jest podstawienie redukujące zbiór do

jednoelementowego. Zbiór jest uniﬁkowalny jeśli istnieje jego uniﬁkator.

Na przykład: zbiór {P (x), P (A)} jest uniﬁkowalny, i jego uniﬁkatorem jest s= {x 7→ A}.

Podobnie, zbiór {P (x), P (y), P (A)} jest uniﬁkowalny, a jego uniﬁkatorem jest s= {x 7→ A, y 7→ A}.

Zbiór {P (A), P (B)} nie jest uniﬁkowalny, podobnie jak zbiór {P (A), Q(x)}.

Uniﬁkacja (cd.)

Uniﬁkacja jest ogólną procedurą, ale tutaj będziemy wykonywać uniﬁkacje wyłącznie na zbiorach klauzul. Rozważmy poniższe, przykładowe zbiory klauzul:

Φ = {P ∨ Q(x), P ∨ Q(A), P ∨ Q(y)}

Ψ = {P ∨ Q(x), P ∨ Q(A), P ∨ Q(f (y))}

Ω = {P ∨ Q(x), P ∨ Q(A) ∨ Q(y)}

Zbiór Φ jest unifikowalny, jego unifikatorem jest s = {x 7→ A, y 7→ A}, a zunifikowanym zbiorem jest singletonowy zbiór Φs = {P ∨ Q(A)}.

Zbiór Ψ nie jest uniﬁkowalny.

Zbiór Ω jest bardziej skomplikowanym przypadkiem. Stosując czysto syntaktyczną unifikację, nie jest on unifikowalny, bo po wykonaniu samego podstawienia formuły nie są identyczne. Jednak stosując semantyczną unifikację, jest on unifikowalny, ponieważ po wykonaniu podstawienia formuły są logicznie równoważne. Będziemy dopuszczali unifikację semantyczną z zastosowaniem łączności i przemienności alternatywy.

(23)

Najogólniejszy uniﬁkator (mgu)

Najogólniejszym unifikatorem unifikowalnego zbioru formuł, albo mgu (most general unifier), nazywamy najprostszy (minimalny) unifikator dla tego zbioru.

Dla uniﬁkowalnego zbioru formuł zawsze istnieje jego mgu, a dowolny uniﬁkator dla tego zbioru można otrzymać przez złożenie mgu z jakimś innym podstawieniem.

Algorytm uniﬁkacji pozwala wyznaczyć mgu zbioru formuł.

Krótkie podsumowanie — pytania sprawdzające

Dla poniższych zbiorów klauzul odpowiedz, czy dany zbiór jest unifikowalny. Jeśli tak, to podaj jego unifikator. Spróbuj podać zarówno mgu, jak i inny unifikator, który nie jest mgu. Jeśli zbiór nie jest unifikowalny, to krótko uzasadnij dlaczego.

1. {P (x) , P (f(x))}

2. {P (x, y) , P (y, x)}

3. {P (x, y) , P (y, f(x))}

4. {P (x, y) , P (y, f(y))}

5. {P (x, y) , P (y, z) , P (z, A)}

(24)

Rezolucja — przypadek ogólny

Rezolucja w ogólnym przypadku: gdy dla dwóch klauzul (zbiorów literałów) {L_i} i {Mi} istnieją ich podzbiory {li} i {mi}, zwane literałami kolidującymi, takie, że zbiór {li} ∪ {¬mi} daje się zuniﬁkować i s jest jego mgu, wtedy ich rezolwentą jest zbiór [{Li} − {li}]s ∪ [{Mi} − {mi}]s.

Mogą istnieć różne rezolwenty danych klauzul dla różnych wyborów podzbiorów ich literałów. Na przykład, rozważmy następujące klauzule:

P[x, f (A)] ∨ P [x, f (y)] ∨ Q(y) oraz ¬P [z, f (A)] ∨ ¬Q(z) Wybierając {li} = {P [x, f (A)]} oraz {mi} = {¬P [z, f (A)]} otrzymujemy rezolwentę:

P[z, f (y)] ∨ ¬Q(z) ∨ Q(y)

Natomiast wybierając {li} = {P [x, f (A)], P [x, f (y)]} oraz {mi} = {¬P [z, f (A)]}

otrzymujemy:

Q(A) ∨ ¬Q(z)

Krótkie podsumowanie — pytania sprawdzające

Dla poniższych zbiorów klauzul, zapisz wszystkie możliwe do otrzymania rezolwenty.

Dla każdej rezolwenty zanotuj, z których klauzul została otrzymana, i jakie było zastosowane podstawienie. Jeśli nie jest możliwe wykonanie rezolucji, to wyjaśnij dlaczego nie.

1. {¬P (x) ∨ Q(x) , P (A)}

2. {¬P (x) ∨ Q(x) , ¬Q(x)}

3. {¬P (x) ∨ Q(x) , P (f(x)) , ¬Q(x)}

(25)

Rezolucja jako reguła wnioskowania

Rezolucja jest poprawną regułą wnioskowania ponieważ klauzula otrzymana z pary klauzul w wyniku zastosowania rezolucji, wynika z nich logicznie. Jednak nie jest kompletna, to znaczy nie możemy z jej pomocą wygenerować z danej formuły ∆ każdego wniosku ϕ, takiego że ∆ ⊢ ϕ.

Na przykład, dla ∆ = {P, Q} nie możemy rezolucją wywieść formuł P ∨ Q ani P ∧ Q, a dla ∆ = {∀xR(x)} nie możemy wywieść formuły ∃xR(x).

Jednak jeśli zastosujemy rezolucję w procedurze dowodzenia nie wprost, czyli przez zaprzeczenie tezy i wyprowadzenie sprzeczności, reprezentowanej przez klauzulę pustą (oznaczaną ✷), to możemy udowodnić nią każde twierdzenie. Zatem w tym sensie rezolucja jest kompletna (refutation complete).

Rozważmy powyższe przykłady. Dla ∆ = {P, Q} zaprzeczeniem formuły P ∨ Q są klauzule ¬P i ¬Q i każda z nich pozwala natychmiast wygenerować klauzulę pustą z odpowiednią klauzulą z ∆. Zaprzeczeniem formuły P ∧ Q jest klauzula ¬P ∨ ¬Q i możemy uzyskać klauzulę pustą w dwóch krokach rezolucji. Dla ∆ = {∀xR(x)}

zaprzeczeniem formuły ∃xR(x) jest ¬R(y), która uniﬁkuje się z klauzulą R(x) otrzymaną z ∆ i daje klauzulę pustą w jednym kroku rezolucji.

Dowodzenie twierdzeń oparte na rezolucji

Podstawowy schemat wnioskowania opartego na rezolucji, gdy posiadamy zbiór

aksjomatów ∆ i chcemy z niego wywieść formułę ϕ, jest następujący. Łączymy zbiory klauzul otrzymanych z ∆ i ¬ϕ, i próbujemy wywieść sprzeczność (klauzulę pustą) z otrzymanego łącznego zbioru klauzul, przez zastosowanie rezolucji na kolejnych parach wybranych klauzul. W tym procesie uzyskana w bieżącym kroku rezolucji nowa klauzula zostaje każdorazowo dołączona do głównego zbioru klauzul, i procedura jest powtarzana.

Podstawowy wynik logiki matematycznej tu wykorzystywany jest następujący. Jeśli uruchomimy rezolucję na zbiorze klauzul otrzymanym z niespełnialnej formuły,

z jakimś systematycznym algorytmem generowania rezolwent, to w pewnym momencie otrzymamy klauzulę pustą. I na odwrót, jeśli ze zbioru klauzul otrzymanego z jakiejś formuły można procedurą rezolucji wygenerować klauzulę pustą, to ten zbiór klauzul, ale także oryginalna formuła, są niespełnialne. Obejmuje to również klauzule otrzymane w wyniku skolemizacji, a więc jest zarazem potwierdzeniem poprawności tej procedury.

(26)

Dowodzenie twierdzeń: przykład

Wiadomo, że:

1. Kto potraﬁ czytać ten jest oświecony. (∀x)[R(x) ⇒ L(x)]

2. Delﬁny nie są oświecone. (∀x)[D(x) ⇒ ¬L(x)]

3. Niektóre delﬁny są inteligentne. (∃x)[D(x) ∧ I(x)]

Należy udowodnić twierdzenie:

4. Są tacy inteligentni co nie potraﬁą czytać. (∃x)[I(x) ∧ ¬R(x)]

Po konwersji do postaci prenex CNF otrzymujemy klauzule:

C1: ¬R(u) ∨ L(u) z pierwszego aksjomatu C2: ¬D(v) ∨ ¬L(v) z drugiego aksjomatu C3a: D(A) z trzeciego aksjomatu, cz.1 C3b: I(A) z trzeciego aksjomatu, cz.2 NT: ¬I(w) ∨ R(w) z negacji twierdzenia

Z kolejnych kroków rezolucji otrzymujemy:

C5: R(A) rezolwenta klauzul C3b i NT C6: L(A) rezolwenta klauzul C5 i C1 C7: ¬D(A) rezolwenta klauzul C6 i C2

C8: ✷ rezolwenta klauzul C7 i C3a

C3a C2 C1 C3b NT

❊❊

❊

❊❊

❊❊❊

❊❊

❊

❊❊

❊❊❊

w=A

❊❊

❊

❊❊

❊❊❊ u=A

❉❉

❉

❉❉

v=A

✂✂

✂

C5✂✂

✂✂

✂✂✂

C6✂

✂✂

C7✂✂

✂✂

✂✂✂

C8=✷

(27)

Dowodzenie twierdzeń: poważniejszy przykład

Rozważmy przykład z matematyki.² Chcemy udowodnić, że przekrój dwóch zbiorów zawiera się w dowolnym z nich. Zaczynamy od wypisania aksjomatów, z których rozumowanie będzie musiało korzystać. W tym przypadku są to deﬁnicje pojęć przekroju i zawierania się zbiorów.

∀x∀s∀t (x ∈ s ∧ x ∈ t) ⇔ x ∈ s ∩ t

∀s∀t (∀x x ∈ s ⇒ x ∈ t) ⇔ s ⊆ t Formuła do udowodnienia:

∀s∀t s ∩ t ⊆ s

2Przykład zapożyczony z książki Geneseretha i Nilssona „Logical Foundations of Artiﬁcial Intelligence”.

Po przetworzeniu do postaci klauzul otrzymujemy:

1. {x 6∈ s, x 6∈ t, x ∈ s ∩ t} z definicji przekroju 2. {x 6∈ s ∩ t, x ∈ s} z definicji przekroju 3. {x 6∈ s ∩ t, x ∈ t} z definicji przekroju 4. {F (s, t) ∈ s, s ⊆ t} z definicji zawierania się 5. {F (s, t) 6∈ t, s ⊆ t} z definicji zawierania się 6. {A ∩ B 6⊆ A} z zaprzeczenia tezy

Zauważmy funkcje Skolema w klauzulach 4 i 5, oraz stałe Skolema w klauzuli 6. Dalej następuje wywód prowadzący dosyć prosto do klauzuli pustej.

7. {F (A ∩ B, A) ∈ A ∩ B} z klauzul 4. i 6.

8. {F (A ∩ B, A) 6∈ A} z klauzul 5. i 6.

9. {F (A ∩ B, A) ∈ A} z klauzul 2. i 7.

10. {} z klauzul 8. i 9.

To koniec dowodu. Cel osiągnięty. Trochę trudno poczuć satysfakcję jaka zwykle

towarzyszy osiągnięciu tradycyjnego dowodu matematycznego. Również aby prześledzić rozumowanie i np. je sprawdzić, trzeba się trochę napracować, aczkolwiek w przypadku tego dowodu jest to jeszcze względnie proste.

(28)

Krótkie podsumowanie — pytania sprawdzające

Dla podanych poniżej zbiorów aksjomatów ∆ i formuły ϕ, spróbuj udowodnić ∆ ⊢ ϕ metodą rezolucji nie wprost. Zacznij od zaprzeczenia formuły celowej, następnie z otrzymanego zaprzeczenia i zbioru aksjomatów utwórz podstawowy zbiór klauzul.

1. ∆ = {∀x(Lubi(x, Wino) ⇒ Lubi(Rychu, x)), Lubi(Zdzich, Wino)}

ϕ = Lubi(Rychu, Zdzich)

2. ∆ = {∀x(Lubi(x, Rychu) ⇒ Lubi(Rychu, x)), ¬Lubi(zona(Zdzich), Rychu)}

ϕ = Lubi(Rychu, zona(Zdzich))

ϕ = (Lubi(Rychu, Zdzich) ∨ Lubi(Rychu, zona(Zdzich))

ϕ = (Lubi(Rychu, Zdzich) ∧ Lubi(Rychu, zona(Zdzich))

(29)

Inżynieria wiedzy

Przedstawiony formalizm logiki predykatów pierwszego rzędu, wraz z rezolucją jako metodą dowodzenia twierdzeń nie wprost, pozwala na budowę inteligentnych agentów efektywnie rozwiązujących stawiane im problemy. Budowa takiego agenta wymaga konstrukcji reprezentacji, którą można sformułować w postaci następującego procesu, zwanego inżynierią wiedzy:

identyﬁkacja problemu

określenie zakresu pytań, na które agent będzie musiał znajdować odpowiedzi, rodzaju faktów, którymi będzie mógł się posługiwać, itp.; na przykład,

w odniesieniu do świata wumpusa, musimy określić, czy agent ma umieć planować działania, czy np. tylko tworzyć reprezentację stanu świata rozpoznanego

w dotychczasowych działaniach?

pozyskanie wiedzy

twórca oprogramowania agenta (inżynier wiedzy) może nie rozumieć wszystkich niuansów opisywanego świata, i musi współpracować z ekspertami aby pozyskać całą niezbędną wiedzę

Metody oparte na logice — inżynieria wiedzy 57

deﬁnicja słownika reprezentacji

pojęcia i obiekty z dziedziny problemowej muszą zostać opisane formułami

logicznymi; konieczne jest zdeﬁniowanie słownika predykatów i termów, tzn. funkcji termowych oraz stałych; ten etap może się okazać kluczowy dla zdolności do

efektywnego rozwiązywania problemów, np. w świecie wumpusa, czy zapadliny lepiej przedstawić jako obiekty, czy własności miejsc

kodowanie wiedzy ogólnej

kodowanie aksjomatów zawierających ogólną wiedzę o dziedzinie problemowej, regułach rządzących światem, istniejących heurystykach, itp.

kodowanie wiedzy szczególnej

zapis konkretnego problemu do rozwiązania przez agenta, w tym zadanych mu faktów o konkretnych obiektach, oraz postawionego zadania jako pytania do odpowiedzenia lub, ogólniej, twierdzenia do udowodnienia

przedstawienie zapytań do urządzenia wnioskującego

uruchomienie procedury dowodzenia na skonstruowanej bazie wiedzy + faktach

(30)

debugowanie bazy wiedzy

niestety, podobnie jak w przypadku zwykłych programów, rzadko kiedy

skonstruowany system będzie od razu poprawnie działał; mogą zdarzyć się takie problemy, jak brak kluczowych aksjomatów, albo aksjomaty nieprecyzyjnie sformułowane, które pozwalają na udowodnienie zbyt mocnych twierdzeń

(31)

Algorytmy pomocnicze: relacja równości

Jedną ze szczególnych relacji występujących w formułach logicznych jest relacja równości (identyczności) termów.

Przykład:

∆ = {=(żona(Zdzich), Gabrysia), Posiada(żona(Zdzich), alfa-8c)}.

Czy to znaczy, że Gabrysia posiada Alfę 8c Competizione?

Czy możemy to udowodnić metodą rezolucji?

Posiada(Gabrysia, alfa-8c)?

Niestety, nie. Procedura dowodowa rezolucji nie traktuje predykatu równości w żaden szczególny sposób i nie wykorzysta posiadanej informacji o identyczności termów. Aby dowód w powyższym przykładzie był możliwy musielibyśmy sformułować dodatkowy aksjomat równości:

∀x, y, z [Posiada(x, y) ∧ =(x, z) ⇒ Posiada(z, y)]

Metody oparte na logice — algorytmy pomocnicze 61

Za pomocą sformułowanego powyżej aksjomatu równości można udowodnić, że Gabrysia posiada Alfę, jak również podobne fakty o posiadaniu dla innych posiadaczy określanych jawnie lub niejawnie. Jednak aby móc podobne wnioskowanie rozciągnąć na równoważność przedmiotu posiadania, niezbędny jest jeszcze inny aksjomat:

∀x, y, z [Posiada(x, y) ∧ =(y, z) ⇒ Posiada(x, z)]

Co gorsza, aby system mógł sprawnie posługiwać się znanymi faktami tożsamości termów w odniesieniu do wszystkich relacji, analogiczne aksjomaty równości należałoby napisać dla wszystkich symboli predykatów. Niestety, w języku logiki pierwszego rzędu nie można tego wyrazić jedną wspólną formułą.

Alternatywnym rozwiązaniem jest wbudowanie obsługi równości termów w procedurę dowodzenia. Istnieje kilka rozwiązań tego problemu: reguła redukcji formuł ze względu na relację równości zwana demodulacją, uogólniona reguła rezolucji uwzględniająca relację równości zwana paramodulacją, oraz wbudowanie relacji równości

w procedurę uniﬁkacji.

(32)

Algorytmy pomocnicze: odzyskiwanie odpowiedzi z drzewa rezolucji

Rozważmy następujący przykład, wiemy że:

Gdzie jest Jaś, tam jest Raﬁk. (∀x)[JestW(Jaś, x) ⇒ JestW(Raﬁk, x)]

Jaś jest w szkole. JestW(Jaś, Szkoła) Chcemy znaleźć odpowiedź na pytanie:

Gdzie jest Raﬁk? (∃x)[JestW(Raﬁk, x)]

Formuła logiczna odpowiadająca oryginalnemu pytaniu różni się nieco od niego, ale dowód znajduje się łatwo:

¬JestW(Jaś,x)∨JestW(Raﬁk,x) ¬JestW(Raﬁk,y)

❛❛❛❛❛❛

❛❛❛❛

❛❛

✁

✁✁

JestW(Jaś,Szkoła) ¬JestW(Jaś,x)

❡

❡❡

✟✟

✟✟ NIL

Niestety, nie daje on odpowiedzi na pierwotnie postawione pytanie.

Odzyskiwanie odpowiedzi z drzewa rezolucji (c.d.)

¬JestW(Jaś,x)∨JestW(Raﬁk,x) ¬JestW(Raﬁk,y)

❛❛❛❛

✄

✄✄

JestW(Jaś,Szkoła) ¬JestW(Jaś,x)

❡

❡❡

✟✟

NIL ⇒

¬JestW(Jaś,x)∨JestW(Rafik,x) ¬JestW(Rafik,y)∨JestW(Rafik,y) PPPPPP

PPPPPPPPP

✄

✄✄

JestW(Jaś,Szkoła) ¬JestW(Jaś,x)∨JestW(Raﬁk,x)

❜❜

✧✧

✧✧ JestW(Raﬁk,Szkoła)

• Podstawowa procedura zamienia dowód nie wprost na kompletny dowód tezy wprost.

• Jeśli twierdzenie zawiera alternatywy (po zaprzeczeniu stają się koniunkcjami) to w wyniku tej procedury otrzymujemy złożoną formułę, która może być trudna do interpretacji.

• Jeśli twierdzenie zawiera kwantyﬁkator ogólny to po zaprzeczeniu pojawiają się w niej stałe lub funkcje Skolema, które lądują w odpowiedzi, ale mogą być zamienione na zmienne kwantyﬁkowane uniwersalnie.

(33)

Algorytmy pomocnicze: strategie przyspieszające rezolucję

W dowodzeniu twierdzeń z wykorzystaniem rezolucji w procedurze dowodowej nie wprost, dążymy do wygenerowania klauzuli pustej, wskazującej na sprzeczność. Aby mieć pewność, że taką klauzulę wygenerujemy, zakładając, że jest to w ogóle możliwe, musimy generować rezolwenty w jakiś systematyczny sposób, na przykład realizując przeszukiwanie wszerz. Jednak przy większych bazach danych, ten sposób może prowadzić do generowania bardzo wielu wniosków, z których większość może nie mieć nic wspólnego z dowodzonym twierdzeniem.

Poszukuje się zatem strategii przyspieszających, które pozwoliłyby odciąć i nie generować niektórych rezolwent. Strategie takie mogą być pełne, tzn. dające

gwarancję znalezienia rozwiązania (fałszu) jeśli to tylko możliwe, albo niepełne, czyli nie dające takiej gwarancji (ale typowo znacznie skuteczniejsze).

Strategie przyspieszające:

• preferencja pojedynczych literałów (normalnie niepełna, ale pełna jeśli jest traktowana tylko jako preferencja)

• strategia zbioru podtrzymania (set of support): tylko rezolucje z klauzulami z pewnego zbioru, początkowo uzyskanego z zaprzeczonej tezy (pełna)

• rezolucja wejściowa (input resolution) zezwala tylko na rezolucje z użyciem klauzuli wejściowej (pełna tylko w niektórych przypadkach, np. dla hornowskich baz danych)

• rezolucja liniowa (niepełna)

• eliminacja powtórzeń i specjalizacji (pełna)

(34)

Nierozstrzygalność rachunku predykatów

Rachunek predykatów wydaje się językiem reprezentacji dobrze nadającym się do wyrażania faktów i wnioskowania w systemach sztucznej inteligencji. Należy jednak zdawać sobie sprawę z pewnych jego ograniczeń, które zawężają jego użyteczność praktyczną.

Twierdzenie Churcha (1936, o nierozstrzygalności rachunku predykatów): nie istnieje procedura pozwalająca w ogólnym przypadku sprawdzać prawdziwości formuł rachunku predykatów. Mówimy, że rachunek predykatów jest nierozstrzygalny (undecidable).

Ta własność w istotny sposób ogranicza możliwości wnioskowania o faktach

wyrażanych w języku predykatów. Co prawda istnieje szereg klas formuł, dla których procedura decyzyjna istnieje. Poza tym rachunek predykatów ma własność

półrozstrzygalności (semidecidability), co oznacza, że istnieje procedura

pozwalająca stwierdzić niespełnialność dowolnej formuły niespełnialnej w skończonej liczbie kroków. Niestety, dla formuł, które nie są niespełnialne, ta procedura może nigdy się nie zatrzymać.

Metody oparte na logice — nierozstrzygalność i niezupełność 67

Niezupełność w rachunku predykatów

Ktoś mógłby myśleć, że nierozstrzygalność rachunku predykatów można pokonać, korzystając z półrozstrzygalności. Chcąc udowodnić formułę ϕ ze zbioru aksjomatów

∆, uruchamiamy równolegle dwa dowody: ∆ ⊢ ϕ i ∆ ⊢ ¬ϕ. Na mocy

półrozstrzygalności, przynajmniej jeden z tych dowodów powinien zakończyć się powodzeniem. Niestety, to również może się nie udać.

Twierdzenie Gödla (1931, o niezupełności): w rachunku predykatów można

sformułować teorie niezupełne, czyli takie, w których istnieją formuły zamknięte, których nie można wywieść, ani nie można wywieść ich zaprzeczenia. Co więcej, takie teorie są dość proste, na przykład taką teorią jest teoria liczb naturalnych, generowana opisującym je zbiorem aksjomatów.

Teorię T nazywamy rozstrzygalną jeśli istnieje algorytm pozwalający dla dowolnej formuły zamkniętej ϕ stwierdzić, czy ϕ ∈ T , czy ϕ 6∈ T . Teorie niezupełne są więc w oczywisty sposób nierozstrzygalne.

Twierdzenie Gödla ma taki skutek, że jeśli po pewnej liczbie kroków dowodu ∆ ⊢ ϕ (i, być może, równoległego dowodu ∆ ⊢ ¬ϕ), nadal nie ma rozwiązania, to nie możemy mieć pewności, czy dowód jednak się zakończy (przynajmniej jeden z nich), czy mamy do czynienia z teorią niezupełną.

Metody oparte na logice — nierozstrzygalność i niezupełność 68

(35)

Zmiany zachodzące w czasie

Rachunek predykatów dobrze spisuje się jako język reprezentacji dla dziedzin

statycznych, gdzie nic się nie dzieje, i wszystko co jest prawdziwe, pozostaje takie na zawsze. Świat realny niestety taki nie jest.

Na przykład, jeśli formuła: JestW(Jaś, Szkoła) poprawnie opisuje stan bieżący jakiegoś powszedniego dnia przed południem, to niestety, musimy się liczyć z tym, że Jaś

pójdzie w pewnym momencie do domu. Jeśli aksjomatyka dobrze opisuje skutki działań agentów, to system mógłby nawet wywnioskować nowy fakt: JestW(Jaś, Dom).

Niestety, wtedy w bazie danych powstanie sprzeczność, która dla systemu logicznego jest katastrofą. System dowodzenia zawierający fałsz w swoich aksjomatach może udowodnić dowolne twierdzenie!

Ćwiczenie: załóżmy, że w zbiorze aksjomatów ∆ istnieją, między innymi, dwie klauzule:

P i ¬P . Przedstaw dowód dowolnej formuły Q. Wskazówka: najpierw udowodnij, że P ∨ ¬P ∨ Q jest tautologią (zdaniem zawsze prawdziwym) dla dowolnych P i Q.

Można to sprawdzić wykonując dowód |= (P ∨ ¬P ∨ Q), czyli dowodząc tezy

z pustym zbiorem aksjomatów. Następnie dodaj tak udowodnioną tautologię do bazy

∆ i przeprowadź dowód Q.

Metody oparte na logice — reprezentacja zmian 69

Logiki czasowe

Dla rozwiązania problemu reprezentacji zmian stworzono wiele specjalistycznych teorii logicznych, zwanych logikami czasowymi (temporal logics). Zwykłe fakty wyrażane w tych logikach zachodzą w określonych momentach czasowych. Natomiast czas, jego własności, i specjalne reguły wnioskowania dotyczące jego upływu, są w logikach czasowych wbudowane w teorię (zamiast być reprezentowane jawnie, na równi z innymi własnościami świata).

Jedną z głównych kwestii, różniących te teorie, jest sama reprezentacja czasu. Może on być dyskretny lub ciągły, może być określany w postaci punktów lub przedziałów, może być ograniczony lub nieograniczony, itp. Co więcej, czas może być pojęciem liniowym, lub rozgałęzionym. Zwykle powinien jednak być uporządkowany, choć istnieją kołowe reprezentacje czasu.

Dla każdej z takich logik czasowych, aby dało się efektywnie wnioskować o tworzonych formułach, reprezentujących zjawiska, z którymi ma do czynienia inteligentny agent, musi istnieć procedura dowodowa. Konstrukcja takiej procedury może opierać się na rzutowaniu danej teorii do logiki predykatów pierwszego rzędu.

Metody oparte na logice — reprezentacja zmian 70

(36)

Rachunek sytuacji

Alternatywą do logik czasowych jest bezpośredni zapis momentów czasowych w języku reprezentacji. Przykładem takiego podejścia jest rachunek sytuacji:

At(Agent, [1, 1], S⁰) ∧ At(Agent, [1, 2], S¹) ∧ S¹ = Result(F orward, S⁰)

PIT

Gold

PIT

Gold

S

0

Forward S

1

Metody oparte na logice — rachunek sytuacji 71

Metody oparte na logice — rachunek sytuacji 72