Closed World Assumption

na podstawie:

Witold Łukaszewicz: Nonmonotonic reasoning: Formalization of Common-Sense Reasoning, Ellis Horwood, 1990.

CWA

CWA - reguła niemonotoniczna do efektywnej reprezentacji światów z pełną informacją.

Obserwacja: Liczba negatywnych faktów o danej dziedzinie jest na ogół wielokrotnie większa niż pozytywnych.

W wielu naturalnych zastosowaniach ich reprezentacja explicite jest niemożliwa (klasyczne bazy danych).

Idea: Przyjmujemy założenie, że wszystkie pozytywne fakty są wyspecyfikowane, a jeśli jakiś pozytywny fakt nie może być wyprowadzony, to jest on fałszywy.

CWA

CWA - reguła niemonotoniczna do efektywnej reprezentacji światów z pełną informacją.

Obserwacja: Liczba negatywnych faktów o danej dziedzinie jest na ogół wielokrotnie większa niż pozytywnych.

W wielu naturalnych zastosowaniach ich reprezentacja explicite jest niemożliwa (klasyczne bazy danych).

Idea: Przyjmujemy założenie, że wszystkie pozytywne fakty są wyspecyfikowane, a jeśli jakiś pozytywny fakt nie może być wyprowadzony, to jest on fałszywy.

CWA

CWA - reguła niemonotoniczna do efektywnej reprezentacji światów z pełną informacją.

Obserwacja: Liczba negatywnych faktów o danej dziedzinie jest na ogół wielokrotnie większa niż pozytywnych.

W wielu naturalnych zastosowaniach ich reprezentacja explicite jest niemożliwa (klasyczne bazy danych).

Idea: Przyjmujemy założenie, że wszystkie pozytywne fakty są wyspecyfikowane, a jeśli jakiś pozytywny fakt nie może być wyprowadzony, to jest on fałszywy.

Koncepcja pochodzi od Reitera. Reguła dotyczy faktów atomowych. Odpowiada to klasycznym bazom danych.

Konwencje terminologiczne:

teoria - skończony zbiór zdań uniwersalnych I rzędu bez równości.

Zapewnia to, że postać klauzulowa jest równoważna wyjściowemu zbiorowi formuł.

reguła CWA = zbiór domniemań:

\{\frac{: ¬R(x̄)}{¬R(x̄)}, R ∈ L_{T}\}

Koncepcja pochodzi od Reitera. Reguła dotyczy faktów atomowych. Odpowiada to klasycznym bazom danych.

Konwencje terminologiczne:

teoria - skończony zbiór zdań uniwersalnych I rzędu bez równości.

Zapewnia to, że postać klauzulowa jest równoważna wyjściowemu zbiorowi formuł.

reguła CWA = zbiór domniemań:

\{\frac{: ¬R(x̄)}{¬R(x̄)}, R ∈ L_{T}\}

Naiwne CWA - NCWA

H(T ) - uniwersum Herbranda teorii T HB(T ) - baza Herbranda

Definicja 1 (Reiter 1978)

NCWA(T ) = T ∪ {¬A : T ⊬ A i A ∈ HB(T )}

Przykład 1

T = {∀x.P(x) ⇒ Q(x); P(a) ∧ R(b)} HB(T ) = {P(a), P(b), Q(a), Q(b), R(a), R(b)} NCWA(T ) = T ∪ {¬P(b), ¬Q(b), ¬R(a)}

Naiwne CWA - NCWA

H(T ) - uniwersum Herbranda teorii T HB(T ) - baza Herbranda

Definicja 1 (Reiter 1978)

NCWA(T ) = T ∪ {¬A : T ⊬ A i A ∈ HB(T )}

Przykład 1

T = {∀x.P(x) ⇒ Q(x); P(a) ∧ R(b)} HB(T ) = {P(a), P(b), Q(a), Q(b), R(a), R(b)} NCWA(T ) = T ∪ {¬P(b), ¬Q(b), ¬R(a)}

Naiwne CWA - NCWA

H(T ) - uniwersum Herbranda teorii T HB(T ) - baza Herbranda

Definicja 1 (Reiter 1978)

NCWA(T ) = T ∪ {¬A : T ⊬ A i A ∈ HB(T )}

Przykład 1

T = {∀x.P(x) ⇒ Q(x); P(a) ∧ R(b)} HB(T ) = {P(a), P(b), Q(a), Q(b), R(a), R(b)} NCWA(T ) = T ∪ {¬P(b), ¬Q(b), ¬R(a)}

Naiwne CWA - NCWA

H(T ) - uniwersum Herbranda teorii T HB(T ) - baza Herbranda

Definicja 1 (Reiter 1978)

NCWA(T ) = T ∪ {¬A : T ⊬ A i A ∈ HB(T )}

Przykład 1

T = {∀x.P(x) ⇒ Q(x); P(a) ∧ R(b)} HB(T ) = {P(a), P(b), Q(a), Q(b), R(a), R(b)} NCWA(T ) = T ∪ {¬P(b), ¬Q(b), ¬R(a)}

Własności NCWA

Czy zachowuje niesprzeczność?

Przykład 2

T = {A(Joe) ∨ A(Bill)}

NCWA(T ) = T ∪ {¬A(Joe), ¬A(Bill)}

Mamy sprzeczność, ale nie możemy powiedzieć, że T jest w pełni wyspecyfikowanym światem.

Twierdzenie 1

Jeśli T jest niesprzeczną teorią Horna, to NCWA(T) jest niesprzeczne.

Własności NCWA

Czy zachowuje niesprzeczność?

Przykład 2

T = {A(Joe) ∨ A(Bill)}

NCWA(T ) = T ∪ {¬A(Joe), ¬A(Bill)}

Mamy sprzeczność, ale nie możemy powiedzieć, że T jest w pełni wyspecyfikowanym światem.

Twierdzenie 1

Jeśli T jest niesprzeczną teorią Horna, to NCWA(T) jest niesprzeczne.

Terminologia cd. Zdanie I rzędu nazywamy pozytywnym ukonkretnionym ( w skrócie GPS), jeśli nie zawiera zmiennych i jego postać CNF zawiera wyłącznie literały pozytywne.

Twierdzenie 2

Załóżmy, że NCWA(T) jest niesprzeczne. Jesli A jest GPS, to

▶ NCWA(T ) ⊢ A wtt T ⊢ A ▶ NCWA(T ) ⊢ ¬A wtt T ⊬ A

Uwaga 1

NCWA, jeśli jest niesprzeczne, nie pozwala wyprowadzić żadnych nowych zdań pozytywnych.

Terminologia cd. Zdanie I rzędu nazywamy pozytywnym ukonkretnionym ( w skrócie GPS), jeśli nie zawiera zmiennych i jego postać CNF zawiera wyłącznie literały pozytywne.

Twierdzenie 2

Załóżmy, że NCWA(T) jest niesprzeczne. Jesli A jest GPS, to

▶ NCWA(T ) ⊢ A wtt T ⊢ A ▶ NCWA(T ) ⊢ ¬A wtt T ⊬ A

Uwaga 1

NCWA, jeśli jest niesprzeczne, nie pozwala wyprowadzić żadnych nowych zdań pozytywnych.

Semantyka NCWA

Definicja 2

Niech T będzie teorią, a M i N modelami Herbranda teorii T. M ≤ N wtedy i tylko wtedy, gdy M | P |≤ N | P | dla każdego predykatu P w teorii T .

M jest minimalnym modelem Herbranda dla T wtedy i tylko wtedy, gdy nie istnieje model herbranda N dla T taki, że N ≤ M i N ≠ M.

Definicja 2

Niech T będzie teorią, a M i N modelami Herbranda teorii T. M ≤ N wtedy i tylko wtedy, gdy M | P |≤ N | P | dla każdego predykatu P w teorii T .

M jest minimalnym modelem Herbranda dla T wtedy i tylko wtedy, gdy nie istnieje model herbranda N dla T taki, że N ≤ M i N ≠ M.

Definicja 2

Niech T będzie teorią, a M i N modelami Herbranda teorii T. M ≤ N wtedy i tylko wtedy, gdy M | P |≤ N | P | dla każdego predykatu P w teorii T .

M jest minimalnym modelem Herbranda dla T wtedy i tylko wtedy, gdy nie istnieje model herbranda N dla T taki, że N ≤ M i N ≠ M.

Twierdzenie 3

Dla dowolnej teorii T , NCWA(T) jest niesprzeczne wtedy i tylko wtedy, gdy T ma najmniejszy model Herbranda.

Każda niesprzeczna teoria Horna ma najmniejszy model Herbranda.

Wniosek 1

1. Najmniejszy model Herbranda dla T, jeśli istnieje, jest modelem Herbranda dla NCWA(T).

2. Jeśli NCWA(T) jest niesprzeczne, to NCWA(T) ma dokładnie jeden model Herbranda, mianowicie najmniejszy model Herbranda dla T.

Każda niesprzeczna teoria Horna ma najmniejszy model Herbranda.

Wniosek 1

1. Najmniejszy model Herbranda dla T, jeśli istnieje, jest modelem Herbranda dla NCWA(T).

2. Jeśli NCWA(T) jest niesprzeczne, to NCWA(T) ma dokładnie jeden model Herbranda, mianowicie najmniejszy model Herbranda dla T.

Każda niesprzeczna teoria Horna ma najmniejszy model Herbranda.

Wniosek 1

1. Najmniejszy model Herbranda dla T, jeśli istnieje, jest modelem Herbranda dla NCWA(T).

2. Jeśli NCWA(T) jest niesprzeczne, to NCWA(T) ma dokładnie jeden model Herbranda, mianowicie najmniejszy model Herbranda dla T.

Każda niesprzeczna teoria Horna ma najmniejszy model Herbranda.

Wniosek 1

1. Najmniejszy model Herbranda dla T, jeśli istnieje, jest modelem Herbranda dla NCWA(T).

2. Jeśli NCWA(T) jest niesprzeczne, to NCWA(T) ma dokładnie jeden model Herbranda, mianowicie najmniejszy model Herbranda dla T.

Twierdzenie 4

Załóżmy, że NCWA(T) jest niesprzeczne, a A jest ukonkretnionym zdaniem.

NCWA(T ) ⊢ A wtedy i tylko wtedy, gdy A jest prawdziwe w najmniejszym modelu Herbranda dla T.

Niestety, Twierdzenie 4 nie uogólnia się na dowolne zdania.

Przykład 3

T = {¬P(a)}

Zdanie ∀x.¬P(x) jest prawdziwe w najmniejszym modelu Herbranda dla T, ale NCWA ⊬ ∀x.¬P(x).

Twierdzenie 4

Załóżmy, że NCWA(T) jest niesprzeczne, a A jest ukonkretnionym zdaniem.

NCWA(T ) ⊢ A wtedy i tylko wtedy, gdy A jest prawdziwe w najmniejszym modelu Herbranda dla T.

Niestety, Twierdzenie 4 nie uogólnia się na dowolne zdania.

Przykład 3

T = {¬P(a)}

Zdanie ∀x.¬P(x) jest prawdziwe w najmniejszym modelu Herbranda dla T, ale NCWA ⊬ ∀x.¬P(x).

NCWA a Circ_{SO}

Oznaczenie: Circ_{SO}(T ) = Circ_{SO}(T ; P̄; ()), gdzie P̄ - krotka wszystkich predykatów z T .

Przykład 4

T = {P(a) ∧ Q(b)}

1. NCWA(T ) ≡ P(a) ∧ Q(b) ∧ ¬P(b) ∧ ¬Q(a)

2. Circ_{SO}(T ) ≡ ∀x(P(x) ⇔ x = a) ∧ ∀x(Q(x) ⇔ x = b)

▶ (1) ⇏ (2) i (2) ⇏ (1) ▶ NCWA(T ) ∧ ∀x.x = a ∨ x = b ⇒ (2) ▶ Circ_{SO}(T ) ∧ a ≠ b ⇒ (1)

Oznaczenie: Circ_{SO}(T ) = Circ_{SO}(T ; P̄; ()), gdzie P̄ - krotka wszystkich predykatów z T .

Przykład 4

T = {P(a) ∧ Q(b)}

1. NCWA(T ) ≡ P(a) ∧ Q(b) ∧ ¬P(b) ∧ ¬Q(a)

2. Circ_{SO}(T ) ≡ ∀x(P(x) ⇔ x = a) ∧ ∀x(Q(x) ⇔ x = b)

▶ (1) ⇏ (2) i (2) ⇏ (1) ▶ NCWA(T ) ∧ ∀x.x = a ∨ x = b ⇒ (2) ▶ Circ_{SO}(T ) ∧ a ≠ b ⇒ (1)

Oznaczenie: Circ_{SO}(T ) = Circ_{SO}(T ; P̄; ()), gdzie P̄ - krotka wszystkich predykatów z T .

Przykład 4

T = {P(a) ∧ Q(b)}

1. NCWA(T ) ≡ P(a) ∧ Q(b) ∧ ¬P(b) ∧ ¬Q(a)

2. Circ_{SO}(T ) ≡ ∀x(P(x) ⇔ x = a) ∧ ∀x(Q(x) ⇔ x = b)

▶ (1) ⇏ (2) i (2) ⇏ (1) ▶ NCWA(T ) ∧ ∀x.x = a ∨ x = b ⇒ (2) ▶ Circ_{SO}(T ) ∧ a ≠ b ⇒ (1)

Oznaczenie: Circ_{SO}(T ) = Circ_{SO}(T ; P̄; ()), gdzie P̄ - krotka wszystkich predykatów z T .

Przykład 4

T = {P(a) ∧ Q(b)}

1. NCWA(T ) ≡ P(a) ∧ Q(b) ∧ ¬P(b) ∧ ¬Q(a)

2. Circ_{SO}(T ) ≡ ∀x(P(x) ⇔ x = a) ∧ ∀x(Q(x) ⇔ x = b)

▶ (1) ⇏ (2) i (2) ⇏ (1) ▶ NCWA(T ) ∧ ∀x.x = a ∨ x = b ⇒ (2) ▶ Circ_{SO}(T ) ∧ a ≠ b ⇒ (1)

Zakładamy, że odtąd - T - teoria bez symboli funkcyjnych D(T ) = ∀x. ⋁_{i=1}^{n} x = c_{i} - aksjomat zamkniętości dziedziny U(T ) = ⋀_{1≤i<j≤n}^{n} c_{i} ≠ c_{j} - UNA

Definicja 3

Teoria T jest fixed-domain wtedy i tylko wtedy, gdy T = T ∪ D(T ) ∪ U(T ) ∪ EQ(T ).

Twierdzenie 5

Jeśli T jest teorią fixed-domain, a NCWA(T) jest niesprzeczne, to dla dowolnej formuły A

NCWA(T ) ⊢ A wtt Circ_{SO}(T ) ⊧ A

Uogólnione CWA - GCWA

NCWA wymaga kompletnej wiedzy o dziedzinie. W przeciwnym przypadku zastosowanie tego formalizmu jest ryzykowne.

GCWA - koncepcja - Minker; modyfikacje - Gelfond & Przymusińska

Przykład 5

T = {Course(c_{1}) ∧ Course(c_{2}), Student(Bill) ∨ Teacher(Bill)}

Teoria T nie może być rozważana jako świat wyspecyfikowany kompletnie. Racjonalne jest wywnioskowanie, że ¬Course(Bill), ¬Student(c_{1}), ¬Student(c_{2}), ¬Teacher(c_{1}) i ¬Teacher(c_{2}). Zastosowanie CWA prowadzi do sprzeczności. Chcielibyśmy zastosować CWA w sposób ograniczony.

Definicja 4

Niech T będzie teorią. Ukonkretniony atom A ∈ HB(T ) jest wolny dla negacji wtedy i tylko wtedy, gdy nie istnieje klauzula C = C_{1} ∨ … ∨ C_{n}(n ≥ 0) taka, że ∀i.C_{i} ∈ HB(T ) i

(i) T ⊢ A ∨ C (ii) T ⊬ C

NFREE(T) - zbiór wszystkich atomów z HB(T), które są wolne dla negacji w T.

Przykład 5 (cd.)

Definicja 4

Niech T będzie teorią. Ukonkretniony atom A ∈ HB(T ) jest wolny dla negacji wtedy i tylko wtedy, gdy nie istnieje klauzula C = C_{1} ∨ … ∨ C_{n}(n ≥ 0) taka, że ∀i.C_{i} ∈ HB(T ) i

(i) T ⊢ A ∨ C (ii) T ⊬ C

NFREE(T) - zbiór wszystkich atomów z HB(T), które są wolne dla negacji w T.

Przykład 5 (cd.)

Definicja 5 (Minker)

GCWA = T ∪ {¬A : A ∈ NFREE(T )}

Relacje między GCWA i NCWA

Twierdzenie 6

Dla dowolnej teorii T

(i) GCWA(T ) ⊆ NCWA(T ) (ii) jeżeli NCWA(T) jest niesprzeczne, to GCWA(T ) = NCWA(T ).

GCWA = T ∪ {¬A : A ∈ NFREE(T )}

Relacje między GCWA i NCWA

Twierdzenie 6

Dla dowolnej teorii T

(i) GCWA(T ) ⊆ NCWA(T ) (ii) jeżeli NCWA(T) jest niesprzeczne, to GCWA(T ) = NCWA(T ).

GCWA = T ∪ {¬A : A ∈ NFREE(T )}

Relacje między GCWA i NCWA

Twierdzenie 6

Dla dowolnej teorii T

(i) GCWA(T ) ⊆ NCWA(T ) (ii) jeżeli NCWA(T) jest niesprzeczne, to GCWA(T ) = NCWA(T ).

Twierdzenie 7

Dla dowolnej teorii T i dowolnego zdania A będącego GPS GCWA(T ) ⊢ A wtedy i tylko wtedy, gdy T ⊢ A.

Uwaga 2

GCWA nie pozwala wyprowadzić żadnych nowych zdań pozytywnych.

Uwaga 2

GCWA nie pozwala wyprowadzić żadnych nowych zdań pozytywnych.

Uwaga 2

GCWA nie pozwala wyprowadzić żadnych nowych zdań pozytywnych.

Semantyka GCWA - minimalne modele Herbranda.

Twierdzenie 9 (Minker)

Dla dowolnej teorii T i dowolnego zdania A ∈ HB(T ), A ∈ NFREE(T ) wtedy i tylko wtedy, gdy ¬A jest prawdziwa w każdym minimalnym modelu Herbranda.

Notacja:

T ⊧_{m} A - oznacza, że A jest prawdziwa w każdym minimalnym modelu Herbranda.

Z twierdzenia 7 i 9 wynika

Twierdzenie 10

Dla dowolnej teorii T i dowolnego ukonkretnionego literału A, GCWA(T ) ⊢ A wtedy i tylko wtedy, gdy T ⊧_{m} A.

Twierdzenie to, niestety, nie uogólnia sie na dowolne zdania ukonkretnione.

Przykład 6

T = {Bird(Tweety) ∨ Bird(Joe)}

Modele Herbranda:

M_{1} = {Bird(Tweety)}
M_{2} = {Bird(Joe)}
M_{3} = {Bird(Tweety), Bird(Joe)}

M_{1} i M_{2} są minimalne. Niech A = ¬(Bird(Tweety) ∧ Bird(Joe)) M_{1} ⊢ A i M_{2} ⊢ A. Ale NFREE(T ) = ∅, więc GCWA(T ) = T ⊬ A.

T = {Bird(Tweety) ∨ Bird(Joe)}

Modele Herbranda:

M_{1} = {Bird(Tweety)}
M_{2} = {Bird(Joe)}
M_{3} = {Bird(Tweety), Bird(Joe)}

M_{1} i M_{2} są minimalne. Niech A = ¬(Bird(Tweety) ∧ Bird(Joe)) M_{1} ⊢ A i M_{2} ⊢ A. Ale NFREE(T ) = ∅, więc GCWA(T ) = T ⊬ A.

T = {Bird(Tweety) ∨ Bird(Joe)}

Modele Herbranda:

M_{1} = {Bird(Tweety)}
M_{2} = {Bird(Joe)}
M_{3} = {Bird(Tweety), Bird(Joe)}

M_{1} i M_{2} są minimalne. Niech A = ¬(Bird(Tweety) ∧ Bird(Joe)) M_{1} ⊢ A i M_{2} ⊢ A. Ale NFREE(T ) = ∅, więc GCWA(T ) = T ⊬ A.

Związki z Circ_{SO} są dość słabe.

Przykład 6 (cd.)

GCWA(T ) ≡ Bird(Tweety) ∨ Bird(Joe) Circ_{SO}(T ) ≡ (∀x.Bird(x) ⇔ x = Tweety)

∨(∀x.Bird(x) ⇔ x = Joe) D(T ) ≡ ∀x.x = Tweety ∨ x = Joe) U(T ) ≡ Tweety ≠ Joe

Niestety, w przeciwieństwie do Twierdzenia 5, D(T ) ∧ U(T ) ⊬ GCWA(T ) ⇔ Circ_{SO}(T )

Zachodzi natomiast osłabiona wersja Twierdzenia 5.

Twierdzenie 11

Jeśli T jest teorią fixed-domain, a A jest literałem ukonkretnionym, to

GCWA(T ) ⊢ A wtt Circ_{SO}(T ) ⊧ A

Ostrożne CWA - CCWA (careful CWA)

Autorzy - Gelfond & Przymusińska Idea: Wybieramy predykaty, do których chcemy zastosować regułę CWA. Poza tym, inne wskazane predykaty mogą się zmieniać. Oznaczenia: T - teoria, R̄ - krotka symboli predykatowych z T .

R̄_{T}^{+} = {P(α) : P jest w R̄ i P(α) ∈ HB(T )}
R̄_{T}^{−} = {¬P(α) : P jest w R̄ i P(α) ∈ HB(T )}

Predykaty z T dzielimy na 3 rozłączne grupy: P̄ - zamykane Q̄ - zmieniane R̄ - pozostałe

Definicja 6

Niech T będzie teorią. Ukonkretniony atom A ∈ P̄^{+} jest wolny dla negacji względem P̄, Q̄, R̄ wtedy i tylko wtedy, gdy A ∈ P̄^{+} i nie istnieje klauzula C = C_{1} ∨ … ∨ C_{n}(n ≥ 0) taka, że ∀i.C_{i} ∈ P̄^{+} ∪ R̄^{+}∪ R̄^{−}

(i) T ⊢ A ∨ C (ii) T ⊬ C

NFREE(T ; P̄, Q̄, R̄) - zbiór wszystkich atomów z HB(T), które są wolne dla negacji w T.

Przykład 7

T = {B(Tweety) ∧ (∀x.B(x) ∧ ¬Ab(x) ⇒ F (x)} i P̄ = (Ab), Q̄ = {F }, R̄ = {B} P̄^{+} = {Ab(Tweety)} P̄^{+} ∪ R̄^{+}∪ R̄^{−} = {Ab(Tweety), B(Tweety), ¬B(Tweety)} NFREE(T ; P̄, Q̄, R̄) = {Ab(Tweety)}

Definicja 7

CCWA(T ; P̄, Q̄, R̄) = T ∪ {¬A : A ∈ NFREE(T ; P̄, Q̄, R̄)

Przykład 7

T = {B(Tweety) ∧ (∀x.B(x) ∧ ¬Ab(x) ⇒ F (x)} i P̄ = (Ab), Q̄ = {F }, R̄ = {B} P̄^{+} = {Ab(Tweety)} P̄^{+} ∪ R̄^{+}∪ R̄^{−} = {Ab(Tweety), B(Tweety), ¬B(Tweety)} NFREE(T ; P̄, Q̄, R̄) = {Ab(Tweety)}

Definicja 7

CCWA(T ; P̄, Q̄, R̄) = T ∪ {¬A : A ∈ NFREE(T ; P̄, Q̄, R̄)

Przykład 7 (cd.)

CCWA(T ; Ab, F , B) = T ∪ {¬Ab(Tweety)} ⊢ F (Tweety)

Własności CCWA

1. Dla dowolnej teorii T i dla P̄ - krotki wszystkich predykatów z T CCWA(T ; P̄, (), ()) = GCWA(T )

2. Jeśli A jest zdaniem ukonkretnionym nie zawierającym (w CNF) literałów z P̄^{−} ∪ Q̄^{+} ∪ Q̄^{−}, to CCWA(T ; P̄, Q̄, R̄) ⊢ A wtedy i tylko wtedy, gdy T ⊢ A.

3. Zachowuje niesprzeczność.

4. Semantyka CCWA - (P̄, Q̄) - minimalne modele Herbranda.

CCWA(T ; Ab, F , B) = T ∪ {¬Ab(Tweety)} ⊢ F (Tweety)

Własności CCWA

1. Dla dowolnej teorii T i dla P̄ - krotki wszystkich predykatów z T CCWA(T ; P̄, (), ()) = GCWA(T )

2. Jeśli A jest zdaniem ukonkretnionym nie zawierającym (w CNF) literałów z P̄^{−} ∪ Q̄^{+} ∪ Q̄^{−}, to CCWA(T ; P̄, Q̄, R̄) ⊢ A wtedy i tylko wtedy, gdy T ⊢ A.

3. Zachowuje niesprzeczność.

4. Semantyka CCWA - (P̄, Q̄) - minimalne modele Herbranda.

Modele Herbranda dla T :

M_{1} = {B(Tweety), F (Tweety)}
M_{2} = {B(Tweety), Ab(Tweety)}
M_{3} = {B(Tweety), Ab(Tweety), F (Tweety)}

M_{1} jest (Ab, F ) - minimalnym modelem Herbranda dla T .

5. Dla danej T ; P̄, Q̄, R̄ i A ∈ R̄^{+}∪ R̄^{−}∪ P̄^{+} ∪ P̄^{−} CCWA(T ; P̄, Q̄, R̄) ⊢ A wtedy i tylko wtedy, gdy T ⊧_{m}^{(P̄,Q̄)} A i nie uogólnia się na dowolne zdania ukonkretnione, a nawet na literały z Q̄^{+} ∪ Q̄^{−}.

6. Jeśli T jest fixed-domain i A ∈ R̄^{+}∪ R̄^{−}∪ P̄^{+} ∪ P̄^{−}, to CCWA(T ; P̄, Q̄, R̄) ⊢ A wtt Circ_{SO}(T ; P̄, Q̄) ⊧ A.

Rozszerzone CWA - ECWA (extended CWA)

Autor - Gelfond

Definicja 8

Niech T będzie teorią. Ukonkretnione zdanie A nie zawierające predykatów z Q̄ jest wolne dla negacji względem P̄, Q̄, R̄ wtedy i tylko wtedy, gdy nie istnieje klauzula C = C_{1} ∨ … ∨ C_{n}(n ≥ 0) taka, że ∀i.C_{i} ∈ P̄^{+} ∪ R̄^{+}∪ R̄^{−}

(i) T ⊢ A ∨ C (ii) T ⊬ C

NFREE_{s}(T ; P̄, Q̄, R̄) - zbiór wszystkich zdań, które są wolne dla negacji w T.

Przykład 8

Teoria z Przykładu 6: T = {Bird(Tweety) ∨ Bird(Joe)}

P̄ = {B}, Q̄ = R̄ = {}
A = B(Tweety) ∧ B(Joe)
A ∈ NFREE_{s}(T ; P̄, Q̄, R̄)
B(Tweety) ∉ NFREE_{s}(T ; P̄, Q̄, R̄)
B(Joe) ∉ NFREE_{s}(T ; P̄, Q̄, R̄)

Definicja 9

ECWA(T ; P̄, Q̄, R̄) = T ∪ {¬A : A ∈ NFREE_{s}(T ; P̄, Q̄, R̄)

ECWA(T ; P̄, Q̄, R̄) ⊢ ¬B(Tweety) ∨ ¬B(Joe)

ECWA(T ; P̄, Q̄, R̄) ⊬ ¬B(Tweety)

ECWA(T ; P̄, Q̄, R̄) ⊬ ¬B(Joe)

Własności ECWA

1. Jeśli A jest zdaniem ukonkretnionym nie zawierającym symboli predykatów z P̄^{−}∪ Q̄, to ECWA(T ; P̄, Q̄, R̄) ⊢ A wtedy i tylko wtedy, gdy T ⊢ A.

2. Zachowuje niesprzeczność.

3. Dla danej T ; P̄, Q̄, R̄ i zdania ukonkretnionego A nie zawierającego symboli predykatów z Q̄ A ∈ NFREE_{s}(T ; P̄, Q̄, R̄) wtt T ⊧_{m}^{(P̄,Q̄)} ¬A czyli ECWA(T ; P̄, Q̄, R̄) ⊢ A wtt T ⊧_{m}^{(P̄,Q̄)} A i nie uogólnia się na dowolne zdania.

4. Jeśli T jest fixed-domain i A jest dowolnym zdaniem, to ECWA(T ; P̄, Q̄, R̄) ⊢ A wtt Circ_{SO}(T ; P̄, Q̄) ⊧ A.

5. Dla dowolnej teorii T (bez symboli funkcyjnych) i dowolnych P̄, Q̄, R̄

D(T ), U(T ) ⊧ ECWA(T ; P̄, Q̄, R̄) ⇔ Circ_{SO}(T ; P̄, Q̄)