Logika domniemań

ang. Default logic (Reiter)

Domniemanie:

\frac{Bird(x) : F lies(x)}{F lies(x)}

Teoria domniemań: Aksjomaty + domniemania Definicja Domniemaniem nazywamy wyrażenie postaci

\frac{A(x) : B_{1}(x), …, B_{k}(x)}{C(x)}

gdzie A(x), B_{1}(x), …, B_{k}(x) i C(x) s _{}a formułami pierwszego rz_{}edu, a x = (x_{1}, …, x_{n}) jest krotk _{}a wszystkich zmiennych wolnych w nich wyst_{}epuj _{}acych.

A(x) – warunek wst_{}epny; B_{1}(x), …, B_{k}(x) – uzasadnienie; C(x) – konsekwencja.

Definicja Teoria domniemań jest to para T = ⟨A,D⟩, gdzie A jest zbiorem zdań pierwszego rz_{}edu, a D jest zbiorem domniemań.

Zbiór twierdzeń wyprowadzalnych z teorii domniemań T nazywamy rozszerzeniem T.

Rozszerzenie powinno zawierać wszystko to, co można wywnioskować z aksjomatów stosuj _{}ac klasyczn _{}a logik_{}e lub domniemania.

Jeśli E jest rozszerzeniem T = ⟨A,D⟩, to:

(1) E powinno być dedukcyjnie zamkni_{}ete wzgl_{}edem logiki klasycznej : E=Th(E);

(2) E powinno zawierać aksjomaty: A⊆E;

(3) E powinno zawierać maksymalny zbiór konkluzji, które można otrzymać stosuj _{}ac domniemania z D.

Zauważmy:

z (1)-(3) wynika, że rozszerzenie teorii ⟨A,D⟩ jest postaci Th(X∪A), gdzie X jest zbiorem konkluzji zastosowanych domniemań z D.

Przykład

A={(1) Basket − P layer(Bill)};

D=\{ \frac{Basket − P layer(x) : T all(x)}{T all(x)} ,

\frac{Basket − P layer(x) : Nimble(x)}{Nimble(x)} \}.

E=Th({(1) , T all(Bill), Nimble(Bill)}). Dodajmy do T

(2) ¬T all(Bill) ∨ ¬Nimble(Bill).

E1=Th((1),(2),T all(Bill)); E2=Th((1),(2),Nimble(Bill)).

Definicja Domniemanie A(x):B_{1}(x), …, B_{k}(x)/C(x) nazywamy otwartym wtedy i tylko wtedy, gdy conajmniej jedno z A(x), B_{1}(x), …, B_{k}(x), C(x) zawiera zmienn _{}a woln _{}a; w przeciwnym przypadku nazywamy zamkni_{}etym. Teoria domniemań jest otwarta wtt zawiera przynajmniej jedno domniemanie otwarte; w przeciwnym przypadku jest zamkni_{}eta .

Zamkni_{}ete teorie domniemań

Naturalne warunki, jakie należy nałożyć na rozszerzenie E teorii ⟨A,D ⟩ s _{}a nast_{}epuj _{}ace:

(1) E=Th(E);

(2) A⊆E;

(3) E powinno zawierać maksymalny zbiór konkluzji, które można otrzymać stosuj _{}ac domniemania z D.

Uwaga:

Konkluzja wyprowadzalna przez zastosowanie domniemania zamkni_{}etego jest to jego konsekwencja.

(3’) E powinno zawierać konsekwencje domniemań stosowalnych z D.

Pozostaje problem formalnej specyfikacji kryterium stosowalności domniemań.

\frac{A : B_{1}, …, B_{k}}{C}

(3”) Jeśli (A : B_{1}, …, B_{k}/C) ∈ D, A ∈ E i ¬B_{1} ∉ E, …, ¬B_{k} ∉ E, to C ∈ E.

Warunki domkni_{}ecia:

(1) E=Th(E);

(2) A⊆E;

(3”) Jeśli (A : B_{1}, …, B_{k}/C) ∈ D, A ∈ E i ¬B_{1} ∉ E, …, ¬B_{k} ∉ E, to C ∈ E.

Warunki domkni_{}ecia mówi _{}a co powinno być w rozszerzeniu, ale nie mówi _{}a czego ma nie być.

“Definicja” E jest rozszerzeniem zamkni_{}etej teorii domniemań wtt E jest najmniejszym zbiorem spełniaj _{}acym warunki domkni_{}ecia.

“Definicja” E jest rozszerzeniem zamkni_{}etej teorii domniemań wtt E jest minimalnym zbiorem spełniaj _{}acym warunki domkni_{}ecia.

T = ⟨{P (a)}, {P (a) : Q(a)/Q(a)}⟩

Zarówno

Th({P (a), Q(a)}) i Th({P (a), ¬Q(a)})

spełniaj _{}a warunki domkni_{}ecia.

Problem:

Załóżmy, że E i Γ(E) oznaczaj _{}a to samo roszerzenie ⟨A,D⟩. Jak zdefiniować Γ(E) za pomoc _{}a E?

Rozwi _{}azanie: Niech Γ(E) b_{}edzie najmniejszym zbiorem spełniaj _{}acym:

(1) Γ(E)=Th(Γ(E));

(2) A⊆ Γ(E);

(3) Jeśli (A : B_{1}, …, B_{k}/C) ∈ D, A∈Γ(E) i ¬B_{1} ∉ E, …, ¬B_{k} ∉ E, to C ∈ Γ(E).

Definicja Niech T = ⟨A,D⟩ bedzie zamkni_{}et _{}a teori _{}a domniemań nad L_{T}. Dla dowolnego zbioru zdań S⊆ L_{T}, niech Γ(S) b_{}edzie najmniejszym zbiorem zdań z L_{T} spełniaj _{}acym:

(1) Γ(S)=Th(Γ(S));

(2) A⊆ Γ(S);

(3) Jeśli (A : B_{1}, …, B_{k}/C) ∈ D, A∈Γ(S) i ¬B_{1} ∉ S, …, ¬B_{k} ∉ S, to C ∈ Γ(S).

Zbiór zdań E⊆ L_{T} jest rozszerzeniem dla T wtt E=Γ(E).

Przykład Rozważmy ponownie: T = ⟨{P (a)}, {P (a) : Q(a)/Q(a)}⟩. T generuje dwa minimalne zbiory spełniaj _{}ace warunki domkni_{}ecia: E1=Th({P (a), Q(a)}) i E2=Th({P (a), ¬Q(a)}).

Ponieważ Γ(E1)=Th({P (a), Q(a)})=E1 Γ(E2)=Th({P (a)})≠ E2 wi_{}ec tylko E1 jest rozszerzeniem T.

Przykład Niech T b_{}edzie teori _{}a z pustym zbiorem aksjomatów i jednym domniemaniem

\frac{p}{¬p} .

T nie ma rozszerzenia. Zauważmy bowiem, że jedynymi kandydatami s _{}a

E1=Th({¬p}) i E2=Th({}).

Ponieważ

Γ(E1)=Th({})≠E1
Γ(E2)=Th({¬p})≠E2

to ani E1 ani E2 nie jest rozszerzeniem T.

Twierdzenie Jeśli T = ⟨A,D⟩ jest zamkni_{}et _{}a teori _{}a domniemań, to zbiór zdań E jest rozszerzeniem T wtt E=⋃_{i=0}^{∞} E_{i}, gdzie

E_{0}=A, i dla i≥ 0

E_{i+1} =Th(E_{i}) ∪ {C : (A : B_{1}, …, B_{k}/C) ∈ D,

gdzie E_{i} ⊢ A i ¬B_{1}, …, ¬B_{k} ∉ E}.

Wniosek Zamkni_{}eta teoria domniemań ⟨A,D⟩ ma sprzeczne rozszerzenie wtt A jest sprzeczny.

Twierdzenie Jeśli E i F s _{}a rozszerzeniami zamkni_{}etej teorii domniemań i E⊆F, to E=F.

Domniemania otwarte i ich instancje

Instancja domniemania otwartego jest to wynik jednoczesnego zast _{}apienia wszystkich wolnych wyst _{}apień zmiennych poprzez termy stałe.

\frac{Bird(cousin(Bob)) : F lies(cousin(Bob))}{F lies(cousin(Bob))}

\frac{Bird(x) : F lies(x)}{F lies(x)}

T ⟶ CLOSED(T)

Przykład Niech T składa si_{}e z:

Bird(T weety) ∧ F ish(Nelly)

\frac{Bird(x) : Has − W ings(x)}{Has − W ings(x)} .

CLOSED(T):

Bird(T weety) ∧ F ish(Nelly)

\frac{Bird(T weety) : Has − W ings(T weety)}{Has − W ings(T weety)}

\frac{Bird(Nelly) : Has − W ings(Nelly)}{Has − W ings(Nelly)} .

Przykład Niech T składa si_{}e z: F ish(Bob) ∀x.F ish(x) ⊃ F ish(father(x))

\frac{F ish(x) : Swims(x)}{Swims(x)} .

CLOSED(T):

F ish(Bob) ∀x.F ish(x) ⊃ F ish(father(x))

\frac{F ish(Bob) : Swims(Bob)}{Swims(Bob)}

\frac{F ish(father(Bob)) : Swims(father(Bob))}{Swims(father(Bob))}

etc.

Przykład Niech T składa si_{}e z:

∃x.Butterfly(x)

\frac{Butterfly(x) : Brightly − Coloured(x)}{Brightly − Coloured(x)} .

Chcielibyśmy wywnioskować ∃x.Butterfly(x) ∧ Brightly − Coloured(x). CLOSED(T):

Butterfly(a)

\frac{Butterfly(a) : Brightly − Coloured(a)}{Brightly − Coloured(a)} .

Przykład Niech T składa si_{}e z:

Birthday(Bill)

\frac{: ∃x.F riend(x, Bill)}{∃x.F riend(x, Bill)}

\frac{Birthday(y) ∧ F riend(x, y) : Gives − Gift(x, y)}{Gives − Gift(x, y)}

Pierwsze domniemanie zostało zast _{}apione przez

\frac{: ∃x.F riend(x, Bill)}{F riend(b, Bill)}

a nast_{}epnie post_{}epujemy jak poprzednio.

Definicja Postaci _{}a Skolema zdania A nazywamy dowolne zdanie kwantyfikowane uniwersalnie, otrzymane z koniunkcyjnej postaci normalnej A drog _{}a skolemizacji.

Definicja Postać Skolema domniemania

\frac{A(x) : B_{1}(x), …, B_{k}(x)}{C(x)}

otrzymuje si_{}e przez zast _{}apienie C(x) przez dowoln _{}a postać Skolema formuły ∀x.C(x) i usuni_{}ecie kwantyfikatora ∀x z konsekwencji otrzymanego domniemania.

Definicja Postaci _{}a Skolema teorii domniemań T jest dowolna teoria otrzymana w wyniku zast _{}apienia domniemań i aksjomatów T przez ich postacie Skolema.

Definicja Niech T = ⟨A,D ⟩ b_{}edzie teori _{}a domniemań, TERMS(T) oznacza zbiór wszystkich termów stałych j_{}ezyka teorii T.

Definicja Niech T b_{}edzie teori _{}a domniemań. Zamkni_{}eciem T, oznaczanym CLOSED(T), nazywamy dowoln _{}a teori_{}e otrzyman _{}a w wyniku nast_{}epuj _{}acej konstrukcji:

1. Jeśli T jest zamkni_{}eta, to CLOSED(T)=T. W przeciwnym przypadku:

2. Zast _{}ap T jej postaci _{}a Skolema, T 1.

3. Niech T 2 b_{}edzie teori _{}a otrzyman _{}a z T 1 przez zast _{}apienie jej domniemań otwartych ich instancjami nad zbiorem TERMS(T 1). T 2 jest zamkni_{}eciem T.

Definicja Niech T b_{}edzie teori _{}a domniemań nad L_{T}. E jest rozszerzeniem dla T wtt E=E’∩L_{T} i E’ jest rozszerzeniem dla CLOSED(T).

Normalne teorie domniemań

Definicja Domniemanie postaci

\frac{A(x) : B(x)}{B(x)}

nazywamy normalnym. Teori_{}e ⟨A,D⟩ nazywamy normaln _{}a wtt każde domniemanie z D jest normalne.

Twierdzenie Każda zamkni_{}eta normalna teoria domniemań ma rozszerzenie .

Twierdzenie Jeśli zamkni_{}eta normalna teoria domniemań ma różne rozszerzenia E i F, to E∪F jest sprzeczne.

Przykład Rozważmy:

A=\{\} D=\{ \frac{: p}{¬r} , \frac{: r}{¬p} \}.

T ma dwa rozszerzenia.

E=Th({¬r}) i F=Th({¬p}).

Chociaż E∪F jest niesprzeczne, to ¬p i ¬r nie powinny być traktowane jako jednoczesne przekonania.

Twierdzenie (Semi-Monotoniczność) Niech D i D’ b_{}ed _{}a zbiorami zamkni_{}etych domniemań normalnych takich, że D’⊆D. Niech E’ b_{}edzie rozszerzeniem T ’=⟨A,D’⟩ i załóżmy, że T =⟨A,D⟩. To T ma rozszerzenie E takie, że E’⊆E.

Twierdzenie mówi, że żadne przekonanie wyprowadzalne z zamkni_{}etej normalnej teorii T nie może być unieważnione przez dodanie do T nowych domniemań zamkni_{}etych normalnych.

Problem reprezentacji

W jakim zakresie domniemania normalne s _{}a wystarczaj _{}ace w praktycznych zastosowaniach?

1. Bill jest usuni_{}ety ze szkoły średniej (dropout).

2. Na ogół, usuni_{}eci ze szkołyśredniej s _{}a dorośli.

3. Na ogół, dorośli s _{}a pracuj _{}acy.

A={Dropout(Bill)}

D=\{ \frac{Dropout(x) : Adult(x)}{Adult(x)} ,

\frac{Adult(x) : Employed(x)}{Employed(x)} \}.

Z teorii tej wynika, że Bill jest osob _{}a pracuj _{}ac _{}a.

\frac{Adult(x) : Employed(x) ∧ ¬Dropout(x)}{Employed(x)}

1. Bill jest 21-latkiem.

2. Każdy 21-latek jest dorosły.

3. Na ogół, dorośli s _{}a żonaci.

21 − Y ear − Old(Bill)

∀x.21 − Y ear − Old(x) ⊃ Adult(x)

\frac{Adult(x) : Married(x)}{Married(x)} .

Z teorii tej wynika, że Bill jest żonaty.

\frac{Adult(x):Married(x)∧¬21−Y ear−Old(x)}{Married(x)}

Sytuacja ogólna: Dana jest reguła, która w izolacji jest reprezentowana w sposób naturalny jako domniemanie normalne

\frac{A(x) : B(x)}{B(x)} .

Jeśli tak _{}a reguł_{}e umieścimy w kontekście, to mog _{}a wyst _{}apić pewne wyj _{}atkowe okoliczności, np. E(x), które czyni _{}a j _{}a niestosowaln _{}a. Najprostszym rozwi _{}azaniem jest zast _{}apienie domniemania normalnego przez

\frac{A(x) : B(x) ∧ ¬E(x)}{B(x)} .

Definicja Domniemanie postaci

\frac{A(x) : B(x) ∧ C(x)}{B(x)}

nazywamy semi-normalnym. Teoria domniemań jest semi-normalna wtt wszystkie jej domniemania s _{}a semi-normalne. Zauważmy, że domniemanie normalne A : B/B może być reprezentowane jako semi-normalne A : B ∧ T rue/B.

Semi-normalne teorie domniemań mog _{}a nie posiadać rozszerzenia:

Niech T = ⟨{},D⟩, gdzie D składa si_{}e z

d1= \frac{: p ∧ ¬q}{¬q} , d2= \frac{: q ∧ ¬r}{¬r}

d3= \frac{: r ∧ ¬p}{¬p} .

W ogólności, teorie semi-normalne nie maj _{}a własności semi-monotoniczności:

Niech T = ⟨{},: p ∧ q/q⟩. T ma jedno rozszerzenie:

E=Th({q}).

Dodaj _{}ac : ¬p/¬p do T, otrzymujemy teori_{}e z jednym rozszerzeniem

F=Th({¬p}).

(1) Czy teorie semi-normalne s _{}a wystarczaj _{}ace do pokrycia wszystkich naturalnie wyst_{}epuj _{}acych praktycznych zastosowań?

(2) W jakim zakresie efekty otrzymane przy użyciu domniemań semi-normalnych mog _{}a być osi _{}agni_{}ete w ramach normalnej reprezentacji?

Schemat translacji

(1) Zast _{}ap domniemanie postaci

d= \frac{A(x) : B(x)}{C(x)}

przez domniemanie semi-normalne

d1= \frac{A(x) : B(x) ∧ C(x)}{C(x)} .

Ten krok wydaje si_{}e być intuicyjnie zgodny, co prowadzi do nast_{}epuj _{}acej obserwacji: Wyrażenia potoczne, które mog _{}a być poprawnie wymodelowane poprzez domniemania z jednym uzasadnieniem, mog _{}a być wyrażone przez domniemania semi-normal-ne.

Ważne: Domniemanie i jego tłumaczenie nie musz _{}a być równoważne. Rozważmy d=: p/¬p i jego tłumaczenie d1=: p ∧ ¬p/¬p. Teoria ⟨{}, {d}⟩ nie ma rozszerzenia, natomiast teoria ⟨{}, {d1}⟩ ma rozszerzenie Th({}).

(2) Zast _{}ap domniemanie semi-normalne

d1= \frac{A(x) : B(x) ∧ C(x)}{C(x)}

przez domniemanie normalne

d1= \frac{A(x) : B(x) ∧ C(x)}{B(x) ∧ C(x)} .

To działa, jeśli zaakceptujemy: “Na ogół, jeśli A(x) i C(x), to B(x).

\frac{Adult(x):Married(x)∧¬21−Y ear−Old(x)}{Married(x)}

\frac{Adult(x):Married(x)∧¬21−Y ear−Old(x)}{Married(x)∧¬21−Y ear−Old(x)}

Oto przykład, gdzie schemat nie działa.

\frac{Has − Motive(x) : Guilty(x)}{Suspect(x)}

\frac{Has − Motive(x) : Guilty(x) ∧ Suspect(x)}{Suspect(x)}

\frac{Has − Motive(x) : Guilty(x) ∧ Suspect(x)}{Guilty(x) ∧ Suspect(x)}

Prace dotycz _{}ace logiki domniemań

• Semantyczna charakteryzacja rozszerzeń (Łukaszewicz 1985, Etherington 1987).

• Teoria dowodzenia dla DL (Reiter 1980).

• Zwi _{}azki pomi_{}edzy DL i AEL (Konolige 1988, Marek & Truszczynski 1989).

• Alternatywne sformułowania logiki domniemań:

– Łukaszewicz 1984.

– Brewka 1991.

Konkluzje

Zalety DL:

Przejrzystość koncepcji.

Wady DL:

(1) Brak naturalnej semantyki.

(2) Brak rozszerzenia dla pewnych teorii.

(3) DL nie radzi sobie z wnioskowaniem przez przypadki.

Na przykład, maj _{}ac A={bird ∨ rocket}

D=\{ \frac{bird : flies}{flies} , \frac{rocket : flies}{flies} \}

czujemy intuicyjnie, że flies powinno być dowodliwe. Niestety, nie jest.