Wnioskowanie w rachunku zda

Bazy wiedzy

Inference engine

Knowledge base

domain−specific content

domain−independent algorithms

Baza wiedzy = zbiór zda« w jzyku formalnym

Deklaratywne podej± ie do budowania systemu:

Powiedz systemowi to o potrzebuje wiedzie¢

Potem system mo»e Zapyta¢ si o robi¢  odpowiedzi powinny wynika¢

z bazy wiedzy

Poziom wiedzy

to o jest wiadome, niezale»nie od tego jak jest zaimplementowane

Poziom implementa ji

Swiat Wumpusa: opis

Warto± i wypªaty

zªoto +1000, ±mier¢ -1000

-1 za krok, -10 za u»y ie strzaªy

Reguªy

Pola s¡siaduj¡ e z Wumpusem maj¡ zapa h

Pola wokóª puªapek s¡ wietrzne

Zªoto si bªysz zy

Strzaª w kierunku Wumpusa zabija go

Strzaª wykorzystuje jedyn¡ strzaª

Podniesienie powoduje zabranie zªota,

je±li jest na tym samym polu

Upusz zenie powoduje pozostawienie zªota

Breeze

Breeze

Breeze

Breeze

Breeze

Stench

Stench

Breeze

PIT

PIT

PIT

1

2

3

4

1

2

3

4

START

Gold

Stench

Obserwa je Wiatr, Bªysk, Zapa h

Swiat Wumpusa: eksploracja

A

OK

OK

OK

Swiat Wumpusa: eksploracja

OK

OK

OK

A

A

B

Swiat Wumpusa: eksploracja

OK

OK

OK

A

A

B

P?

P?

Swiat Wumpusa: eksploracja

OK

OK

OK

A

A

B

P?

P?

A

S

Swiat Wumpusa: eksploracja

OK

OK

OK

A

A

B

P?

P?

A

S

OK

P

W

Swiat Wumpusa: eksploracja

OK

OK

OK

A

A

B

P?

P?

A

S

OK

P

W

A

Swiat Wumpusa: eksploracja

OK

OK

OK

A

A

B

P?

P?

A

S

OK

P

W

A

OK

OK

Swiat Wumpusa: eksploracja

OK

OK

OK

A

A

B

P?

P?

A

S

OK

P

W

A

OK

OK

A

BGS

Logika

Logika jest formalnym jzykiem reprezenta ji informa ji takim, w którym mog¡ by¢ wy i¡gane wnioski

Syntaktyka deniuje zdania w jzyku

Semantyka deniuje zna zenie zda«;

tzn. deniuje prawdziwo±¢ zda« w opisywanym ±wie ie

Np. jzyk arytmetyki

x

+ 2 ≥ y

jest zdaniem;

x2 + y >

nie jest zdaniem

x

+ 2 ≥ y

jest prawdziwe wtw

x

+ 2

jest nie mniejsze ni» li zba

y

x

+ 2 ≥ y

jest prawdziwe w ±wie ie, gdzie

x

= 7, y = 1

Logiczna konsekwencja

Logi zna konsekwen ja ozna za, »e jeden fakt wynika z innego:

KB

|= α

α

jest logi zn¡ konsekwen j¡ bazy wiedzy

KB

wtedy i tylko wtedy

α

jest prawdziwe we wszystki h ±wiata h, w który h

KB

jest prawdziwe Np. logi zn¡ konsekwen j¡ baza wiedzy

KB

zawieraj¡ ej Giants wygrali

i Reds wygrali jest zdanie Giants lub Reds wygrali

Np.

4 = x + y

jest logi zn¡ konsekwen j¡

x

+ y = 4

Logi zna konsekwen ja jest rela j¡ pomidzy zdaniami (syntakty zn¡)

która opiera si na semanty e

Modele

Logi y my±l¡ zazwy zaj w termina h modeli, które formalnie s¡ ustruktural-nionymi ±wiatami wzgldem który h mo»na wyzna za¢ prawdziwo±¢

Mówimy, »e

m

jest modelem zdania

α

je±li

α

jest prawdziwe w

m

M

(α)

jest zbiorem wszystki h modeli

α

Wtedy

KB

|= α

wtw

M

(KB) ⊆ M (α)

Np.

KB

= Giants i Reds wygrali

α

= Giants wygrali

M( )

M(KB)

x

x

x

x

x

x

x

x

x

x

x

x

x

x

x

x

x

x

x

x

x

x

x

x

x

xx

x

x

x

x

x

x

x

x

x

x

x

x

x

x

x

x

x

x

x

x

Swiat Wumpusa: logiczna konsekwencja

Sytua ja po zbadaniu pola [1,1℄,

przesuni iu w prawo i wykry iu wiatru w

[2,1℄

Rozwa»amy mo»liwe modele dla pól '?'

doty z¡ e informa ji, zy na ty h pola h s¡

puªapki

A

A

B

?

?

?

Modele w swiecie Wumpusa

1

2

3

1

2

Breeze

PIT

1

2

3

1

2

Breeze

PIT

1

2

3

1

2

Breeze

PIT

PIT

PIT

1

2

3

1

2

Breeze

PIT

PIT

1

2

3

1

2

Breeze

PIT

1

2

3

1

2

Breeze

PIT

PIT

1

2

3

1

2

Breeze

PIT

PIT

1

2

3

1

2

Breeze

Modele w swiecie Wumpusa

1

2

3

1

2

Breeze

PIT

1

2

3

1

2

Breeze

PIT

1

2

3

1

2

Breeze

PIT

PIT

PIT

1

2

3

1

2

Breeze

PIT

PIT

1

2

3

1

2

Breeze

PIT

1

2

3

1

2

Breeze

PIT

PIT

1

2

3

1

2

Breeze

PIT

PIT

1

2

3

1

2

Breeze

KB

Modele w swiecie Wumpusa

1

2

3

1

2

Breeze

PIT

1

2

3

1

2

Breeze

PIT

1

2

3

1

2

Breeze

PIT

PIT

PIT

1

2

3

1

2

Breeze

PIT

PIT

1

2

3

1

2

Breeze

PIT

1

2

3

1

2

Breeze

PIT

PIT

1

2

3

1

2

Breeze

PIT

PIT

1

2

3

1

2

Breeze

KB

1

KB

= reguªy ±wiata Wumpusa + obserwa je

Modele w swiecie Wumpusa

1

2

3

1

2

Breeze

PIT

1

2

3

1

2

Breeze

PIT

1

2

3

1

2

Breeze

PIT

PIT

PIT

1

2

3

1

2

Breeze

PIT

PIT

1

2

3

1

2

Breeze

PIT

1

2

3

1

2

Breeze

PIT

PIT

1

2

3

1

2

Breeze

PIT

PIT

1

2

3

1

2

Breeze

KB

Modele w swiecie Wumpusa

1

2

3

1

2

Breeze

PIT

1

2

3

1

2

Breeze

PIT

1

2

3

1

2

Breeze

PIT

PIT

PIT

1

2

3

1

2

Breeze

PIT

PIT

1

2

3

1

2

Breeze

PIT

1

2

3

1

2

Breeze

PIT

PIT

1

2

3

1

2

Breeze

PIT

PIT

1

2

3

1

2

Breeze

KB

2

KB

= reguªy ±wiata Wumpusa + obserwa je

Wnioskowanie

KB

⊢

i

α

= zdanie

α

mo»e by¢ wyprowadzone z

KB

pro edur¡

i

Konsekwen je

KB

to stóg siana, a

α

to igªa.

Logi zna konsekwen ja = igªa w stogu siana;

Wwnioskowanie = metoda na jej znalezienie

Poprawno±¢:

i

jest poprawne, je±li

zawsze kiedy

KB

⊢

i

α

, to te»

KB

|= α

Peªno±¢:

i

jest peªne je±li

zawsze kiedy

KB

|= α

, to te»

KB

⊢

i

α

Cel: zdeniowa¢ logik, w której mo»na wyrazi¢ mo»liwie jak najwi ej i dla

której istnieje poprawna i peªna pro edura dowodzenia.

Tzn. ta pro edura odpowie na ka»de pytanie, które wynika z tego, o wiadomo

Logika zdaniowa: syntaktyka

Logika zdaniowa jest najprostsz¡ logik¡  ilustruje podstawowe pomysªy

Symbole zdaniowe

P

1

,

P

2

itd. s¡ zdaniami

Je±li

S

jest zdaniem,

¬S

jest zdaniem (nega ja)

Je±li

S

1

i

S

2

s¡ zdaniami,

S

1

∧ S

2

jest zdaniem (koniunk ja) Je±li

S

1

i

S

2

s¡ zdaniami,

S

1

∨ S

2

jest zdaniem (alternatywa) Je±li

S

1

i

S

2

s¡ zdaniami,

S

1

⇒ S

2

jest zdaniem (implika ja)

Logika zdaniowa: semantyka

Ka»dy model okre±la warto±¢ prawda/faªsz dla ka»dego symbolu zdaniowego

Np.

P

1

,2

P

2

,2

P

3

,1

true true f alse

(Dla ty h symboli 8 mo»liwy h modeli, mog¡ by¢ wyli zone automaty znie.)

Reguªy do okre±lenia prawdziwo± i zda« wzgldem modelu

m

:

¬S

jest prawdziwe wtw

S

jest nieprawdziwe

S

1

∧ S

2

jest prawdziwe wtw

S

1

jest prawdziwe i

S

2

jest prawdziwe

S

1

∨ S

2

jest prawdziwe wtw

S

1

jest prawdziwe lub

S

2

jest prawdziwe

S

1

⇒ S

2

jest prawdziwe wtw

S

1

jest nieprawdz. lub

S

2

jest prawdziwe tzn. jest nieprawdz. wtw

S

1

jest prawdziwe i

S

2

jest nieprawdz.

S

1

⇔ S

2

jest prawdziwe wtw

S

1

⇒ S

2

jest prawdziwe i

S

2

⇒ S

1

jest prawdziwe Prosty rekuren yjny pro es okre±laj¡ y prawdziwo±¢ dowolnego zdania, np.

Tabela prawdziwosci dla lacznikow zdaniowych

P

Q

¬P

P

∧ Q P ∨ Q P ⇒ Q P ⇔ Q

f alse f alse true

f alse f alse

true

true

f alse true

true

f alse

true

true

f alse

true f alse f alse f alse

true

f alse

f alse

Zdania w swiecie Wumpusa

Nie h

P

i,j

jest prawdziwe je±li w

[i, j]

jest puªapka. Nie h

B

i,j

jest prawdziwe je±li w

[i, j]

jest wiatr.

¬P

1

_,1

¬B

1

_,1

B

2

_,1

Zdania w swiecie Wumpusa

Nie h

P

i,j

jest prawdziwe je±li w

[i, j]

jest puªapka. Nie h

B

i,j

jest prawdziwe je±li w

[i, j]

jest wiatr.

¬P

1

_,1

¬B

1

_,1

B

2

_,1

Puªapki wywoªuj¡ wiatr na s¡siedni h pola h

B

1

,1

⇔

(P

1

,2

∨ P

2

,1

)

B

2

_,1

⇔

(P

1

_,1

∨ P

2

_,2

∨ P

3

_,1

)

Tabela prawdziwosci dla wnioskowania

B

1

_,1

B

2

_,1

P

1

_,1

P

1

_,2

P

2

_,1

P

2

_,2

P

3

_,1

KB

α

1

f alse f alse f alse f alse f alse f alse f alse f alse

true

f alse f alse f alse f alse f alse f alse

true

f alse

true

. . . . . . . . . . . . . . . . . . . . . . . . . . .

f alse

true

f alse f alse f alse f alse f alse f alse

true

f alse

true

f alse f alse f alse f alse

true

true

true

f alse

true

f alse f alse f alse

true

f alse

true

true

f alse

true

f alse f alse f alse

true

true

true

true

f alse

true

f alse f alse

true

f alse f alse f alse

true

. . . . . . . . . . . . . . . . . . . . . . . . . . .

Rownowaznosc logiczna

Dwa zdania s¡ logi znie równowa»ne wtw prawdziwe w ty h samy h modela h:

α

≡ β

wtedy i tylko wtedy

α

|= β

and

β

|= α

(α ∧ β) ≡ (β ∧ α)

przemienno±¢

∧

(α ∨ β) ≡ (β ∨ α)

przemienno±¢

∨

((α ∧ β) ∧ γ) ≡ (α ∧ (β ∧ γ))

ª¡ zno±¢

∧

((α ∨ β) ∨ γ) ≡ (α ∨ (β ∨ γ))

ª¡ zno±¢

∨

¬(¬α) ≡ α

elimna ja podwójnej nega ji

(α ⇒ β) ≡ (¬β ⇒ ¬α)

zaprze zenie

(α ⇒ β) ≡ (¬α ∨ β)

elimina ja implika ji

(α ⇔ β) ≡ ((α ⇒ β) ∧ (β ⇒ α))

elimina ja równowa¹no± i

¬(α ∧ β) ≡ (¬α ∨ ¬β)

prawo de Morgana

¬(α ∨ β) ≡ (¬α ∧ ¬β)

prawo de Morgana

(α ∧ (β ∨ γ)) ≡ ((α ∧ β) ∨ (α ∧ γ))

rozdzielno±¢

∧

wzgldem

∨

(α ∨ (β ∧ γ)) ≡ ((α ∨ β) ∧ (α ∨ γ))

rozdzielno±¢

∨

wzgldem

∧

Tautologie i spelnialnosc

Zdanie jest tautologi¡ je±li jest prawdziwe we wszystki h modela h,

np.

T rue

,

A

∨ ¬A

,

A

⇒ A

,

(A ∧ (A ⇒ B)) ⇒ B

Tautologie s¡ zwiaz¡ne z Twierdzeniem o Deduk ji:

KB

|= α

wtedy i tylko wtedy

(KB ⇒ α)

jest tautologi¡ Zdanie jest speªnialne je±li jest prawdziwe w niektóry h modela h

np.

A

∨ B

,

C

Zdanie jest niespeªnialne je±li nie jest prawdziwe w »adnym modelu np.

A

∧ ¬A

Speªnialno±¢ jest zwi¡zana z wnioskowaniem przez sprowadzenie do

sprze z-no± i:

Metody dowodzenia

Metody dowodzenia mo»na podzieli¢ na dwie kategorie:

Sprawdzanie modeli

 Przeszukiwanie przestrzeni warto± iowa«

Zastosowanie reguª wnioskowania

 Poprawne generowanie nowy h zda« ze stary h

 Dowód = i¡g zastosowa« reguª wnioskowania

Mo»na u»y¢ reguª jako operatorów w standardowy h

algorytma h przeszukiwania

Metody dowodzenia: algorytmy

Sprawdzanie modeli

 wyli zanie tabeli prawdziwo± i (zawsze wykªadni ze od

n

)

 poprawiony ba ktra king, np. alg. DavisPutnamLogemannLoveland

 przesz. heurysty zne w przestrzeni modeli (poprawne, ale niepeªne)

np. algorytmy hill- limbing podobne do min- oni ts

Zastosowanie reguª wnioskowania

 Forward haining (ograni zone do klauzul Horna)

 Ba kward haining (ograni zone do klauzul Horna)

Wnioskowanie przez wyliczanie

Wyli zanie wszystki h modeli w gª¡b jest poprawne i peªne

fun tion TT-Entails?(KB,

α

) returns true or false symbols

←

a list of the proposition symbols in KB and

α

return TT-Che k-All(KB,

α

,symbols,

[ ]

)

fun tion TT-Che k-All(KB,

α

,symbols,model) returns true or false if Empty?(symbols) then

if PL-True?(KB,model) then return PL-True?(

α

,model) else return true

else do

P

←

First(symbols); rest

←

Rest(symbols)

return TT-Che k-All(KB,

α

,rest,Extend (

P , true, model

) and TT-Che k-All(KB,

α

,rest,Extend (

P , false, model

)

Forward chaining i backward chaining

Posta¢ Horna (ograni zona)

KB = koniunk ja klauzul Horna

Klauzula Horna =

♦

symbol zdaniowy; lub

♦

(koniunk ja symboli)

⇒

symbol

Np.

C

∧ (B ⇒ A) ∧ (C ∧ D ⇒ B)

Modus Ponens (dla posta i Horna): peªne dla baz wiedzy Horna

α

1

, . . . , α

_n

,

α

1

∧ · · · ∧ α

_n

⇒ β

β

Mo»na u»y¢ algorytmów forward haining lub ba kward haining. Oba algorytmy s¡ naturalne i wykonuj¡ si w zasie liniowym

Forward chaining: algorytm

Pomysª: stosuje dowoln¡ reguª, której przesªanki s¡ speªnione w

KB

,

dodaje jej wniosek do

KB

, i powtarza, a» znajdzie odpowied¹

fun tion PL-FC-Entails?(KB,q) returns true or false

lo al variables: ount, a table, indexed by lause, initially the number of premises

inferred, a table, indexed by symbol, ea h entry initially false

agenda, a list of symbols, initially the symbols known to be true

while agenda is not empty do

p

←

Pop(agenda) unless inferred[p℄ do

inferred[p℄

←

true

for ea h Horn lause in whose premise p appears do

de rement ount[ ℄

if ount[ ℄ = 0 then do

if Head[ ℄ = q then return true

Push(Head[ ℄,agenda)

Forward chaining: przyklad

P

⇒ Q

L

∧ M ⇒ P

B

∧ L ⇒ M

A

∧ P ⇒ L

A

∧ B ⇒ L

A

B

Q

P

M

L

B

A

Forward chaining: przyklad

Q

P

M

L

B

A

2

2

2

2

1

Forward chaining: przyklad

Q

P

M

L

B

2

1

A

1

1

2

Forward chaining: przyklad

Q

P

M

2

1

A

1

B

0

1

L

Forward chaining: przyklad

Q

P

M

1

A

1

B

0

L

0

1

Forward chaining: przyklad

Q

1

A

1

B

0

L

0

M

0

P

Forward chaining: przyklad

Q

A

B

0

L

0

M

0

P

0

0

Forward chaining: przyklad

Q

A

B

0

L

0

M

0

P

0

0

Forward chaining: przyklad

A

B

0

L

0

M

0

P

0

0

Q

Dowod pelnosci

Forward Chaining wnioskuje ka»de atomowe zdanie, które jest logi zn¡

kon-sekwen j¡

KB

1. Algorytm osi¡ga punkt staªy gdzie nie mo»na wywnioskowa¢ »adnego nowego zdania

2. Rozwa»my stan ko« owy jako model

m

, przypisuj¡ y prawd/faªsz

do symboli

3. Ka»da klauzula w oryginalnej

KB

jest prawdziwa w

m

Dowód: Przypu±¢my

a

1

∧ . . . ∧ a

k

⇒ b

jest nieprawdziwe w

m

Wtedy

a

1

∧ . . . ∧ a

k

jest prawdziwe w

m

i

b

jest nieprawdziwe w

m

Zatem algorytm nie osi¡gn¡ª punktu staªego!

4. St¡d

m

jest modelem

KB

Backward chaining

Pomysª: wyprowadzanie wste z od zapytania

q

:

dowód

q

w ba kward haining przez

sprawdzenie, zy

q

jest ju» znane, lub

udowodnienie wszystki h przesªanek pewnej reguªy, która po i¡ga

q

Unikanie ptli: sprawdza, zy nowy pod el nie byª ju» w ze±niej wygenerowany

Unikanie powtórze«: sprawdza, zy dla nowego pod elu

1) byªa ju» udowodniona prawdziwo±¢, lub

Backward chaining: przyklad

Q

P

M

L

A

B

Backward chaining: przyklad

P

M

L

A

Q

B

Backward chaining: przyklad

M

L

A

Q

P

B

Backward chaining: przyklad

M

A

Q

P

L

B

Backward chaining: przyklad

M

L

A

Q

P

B

Backward chaining: przyklad

M

A

Q

P

L

B

Backward chaining: przyklad

M

A

Q

P

L

B

Backward chaining: przyklad

A

Q

P

L

B

M

Backward chaining: przyklad

A

Q

P

L

B

M

Backward chaining: przyklad

A

Q

P

L

B

M

Backward chaining: przyklad

A

Q

P

L

B

M

Forward chaining vs. backward chaining

Forward haining jest sterowany-danymi, por. automaty zne, nie±wiadome przetwarzanie, np. rozpoznawanie obiektów, rutynowe de yzje

Mo»e wykona¢ du»o pra y nieistotnej dla osi¡gni ia elu

Ba kward haining jest nakierowany na el, dobry do rozwi¡zywania proble-mów, np. Gdzie s¡ moje klu ze? Jak dostan si na studia?

Koszt ba kward haining mo»e by¢ du»o mniejszy ni» liniowy wzgldem

Rezolucja

Posta¢ normalna koniunk yjna (CNF  uniwersalna)

koniunk ja alternatyw literaªów

|

{z

}

klauzule

Np.

(A ∨ ¬B) ∧ (B ∨ ¬C ∨ ¬D)

Rezolu yjna reguªa wnioskowania (dla CNF):

ℓ

1

∨ · · · ∨ ℓ

_k

,

m

1

∨ · · · ∨ m

_n

ℓ

1

∨ · · · ∨ ℓ

_i−1

∨ ℓ

_i+1

∨ · · · ∨ ℓ

_k

∨ m

1

∨ · · · ∨ m

_j−1

∨ m

_j+1

∨ · · · ∨ m

_n

gdize

ℓ

i

i

m

j

s¡ dopeªniaj¡ ymi si literaªami. Np.

OK

OK

OK

A

A

B

P?

P?

A

S

OK

P

W

A

P

1

_,3

∨ P

2

_,2

,

¬P

2

_,2

P

1

_,3

Rezolucja: przeksztalcanie zdania do CNF

B

1

,1

⇔ (P

1

,2

∨ P

2

,1

)

1. Elimina ja

⇔

poprzez zast¡pienie

α

⇔ β

przez

(α ⇒ β) ∧ (β ⇒ α)

.

(B

1

_,1

⇒ (P

1

_,2

∨ P

2

_,1

)) ∧ ((P

1

_,2

∨ P

2

_,1

) ⇒ B

1

_,1

)

2. Elimina ja

⇒

poprzez zast¡pienie

α

⇒ β

przez

¬α ∨ β

.

(¬B

1

_,1

∨ P

1

_,2

∨ P

2

_,1

) ∧ (¬(P

1

_,2

∨ P

2

_,1

) ∨ B

1

_,1

)

3. Przesuni ie

¬

do wewn¡trz (prawa de Morgana i elim. podwójnej nega ji):

(¬B

1

_,1

∨ P

1

_,2

∨ P

2

_,1

) ∧ ((¬P

1

_,2

∧ ¬P

2

_,1

) ∨ B

1

_,1

)

4. Spªasz zenie przy pomo y rozdzielno± i (

∨

wzgldem

∧

):

Rezolucja: algorytm

Dowód przez zaprze zenie, tzn. pokazanie, »e

KB

∧ ¬α

niespeªnialne

fun tion PL-Resolution(KB,

α

) returns true or false

lauses

←

the set of lauses in the CNF representation of

KB

∧ ¬α

loop do

new

← { }

for ea h

C

i

,

C

j

in lauses do

resolvents

←

PL-Resolve(

C

i

,

C

j

)

if resolvents ontains the empty lause then return true

new

← new ∪ resolvents

if

new

⊆ clauses

then return false lauses

← clauses ∪ new

Rezolucja: przyklad

KB

= (B

1

,1

⇔ (P

1

,2

∨ P

2

,1

)) ∧ ¬B

1

,1

α

= ¬P

1

,2

P

_1,2

P

1,2

P

_2,1

P

1,2

B

1,1

B

1,1

P

2,1

B

1,1

P

1,2

P

2,1

P

2,1

P

1,2

B

1,1

B

1,1

P

1,2

B

1,1

P

2,1

B

1,1

P

2,1

B

1,1

P

_1,2

P

_2,1

P

_1,2

Procedura Davisa-Putnama

Podobnie jak przy rezolu ji:

 Sprowadzenie

KB

∧ ¬α

do posta i normalnej koniunk yjnej

Procedura Davisa-Putnama

fun tion PL-Davis-Putnam(KB,

α

) returns true or false

lauses

←

the set of CNF lauses representing

KB

∧ ¬α

(tautologies removed) sets

← {

lauses

}

newsets

← { }

while sets is not empty do

if

{ } ∈

sets then return false

sets

← {

lauses

∈

sets: lauses doesn't have ontradi tory unary lauses

p

and

¬p}

for ea h lauses

∈

sets do

while

∃

unary

l

∈

lauses do remove lauses ontaining

l

and o uren es of

¬l

while some

l

o urs in lauses but

¬l

doesn't do remove lauses ontaining

l

p

←

any propositional variable o uring in lauses

lauses

(p = true) ← {C

′

i

: C

i

∈

lauses

∧ p 6∈ C

i

∧ C

′

i

is

C

i

with removed

¬p}

lauses

(p = f alse) ← {C

′

i

: C

i

∈

lauses

∧ ¬p 6∈ C

i

∧ C

′

i

is

C

i

with removed

p

}

for ea h lauses

(. . .) ∈ {

lauses

(p = true)

, lauses

(p = f alse)}

do

lauses

(. . .) ← {C

i

∈

lauses

(. . .) : C

i

isn't super lauseof any

C

j

∈

lauses

(. . .)}

newsets

←

newsets

∪ {

lauses

(. . .)

}

sets

←

newsets newsets

← { }

return true