Metoda tablic semantycznych

1 Metoda tablic semantycznych

Zarówno metoda tablic semantycznych, jak i rezolucji, to dosy¢

sprawny algorytm do badania speªnialni±ci formuª, a wi¦c i tautologii. Chodzi w niej o wskazanie, je±li istnieje, modelu dla formuªy. Opiera si¦ on o banaln¡ obserwacj¦: koniunkcja zmiennych zdaniowych i ich negacji jest speªnialna (i ma tylko jeden model) wtw, gdy w niej nie wyst¦puje para zmienna i jej negacja.

Denicja

Literaªem nazywamy zmienn¡ zdaniow¡ lub jej negacj¦. Zmienn¡

nazywamy literaªem pozytywnym, a jej negacj¦ literaªem

negatywnym. Dla formuªy A zbiór {A, ¬A} nazywamy par¡ formuª (lieraªów, je±li A jest literaªem) komplementarnych.

Przykªad Rozwa»my formuª¦ A = q ∧ (¬p ∨ ¬q). Z jednej strony przy warto±ciowaniu v mamy v(A) = 1 wtw, gdy v(q) = 1 i v(¬p ∨ ¬q) = 1, bo A jest koniunkcj¡. Z analizy ¬p ∨ ¬q mamy dwie mo»liwo±ci:

1 v(q) = 1 i v(¬q) = 1;

2 v(q) = 1 i v(¬p) = 1;

Oczywi±cie pierwsza nigdy nie wyst¦puje, bo mamy par¦

komplementarnych literaªów, a druga daje jedyny model dla A.

Z drugiej strony A ≡ q ∧ ¬p ∨ q ∧ ¬q ≡ q ∧ ¬p i warto±ciowanie v takie, »e v(q) = 1 i v(¬p) = 1 jest jedynym modelem dla ostatniej formuªy.

Powy»szy przykªad unaocznia dwie rzeczy:

1 Je±li analizowana formuªa A jest alternatyw¡ koniunkcji literaªów, to jest ona speªnialna wtw, gdy która± z koniunkcji nie zawiera pary literaªów komplementarnych. Ponadto ka»da taka koniunkcja wyznacza pewien model dla A.

2 Dla ka»dej formuªy A mo»na efektywnie wyznaczy¢

równowa»n¡ z ni¡ formuª¦ B, która jest alternatyw¡ koniunkcji literaªów: jest w postaci normalnej alternatywnej (PNA).

otrzymanej alternatywy zawieraj¡ par¦ literaªów komplementarnych.

Cz¦sto przedstawia si¦ dziaªanie tego algorytmu gracznie buduj¡c tabel¦, której elementy ªaczy si¦ strzaªkami, które opisuj¡ jak powstaj¡ umieszczane w niej formuªy. Uwzgl¦dniaj¡c umieszczone straªki otrzymujemy drzewo. Dla przykªadu:

q ∧ (¬p ∨ ¬q)

q, (¬p ∨ ¬q)

wwppppppppppp

N''N NN NN NN NN N

q, ¬q q, ¬p

× 

Elementami tablicy s¡ zbiory formuª, które tak dªugo

przeksztaªcamy, a» ustalimy, czy zawieraj¡ par¦ komplementarn¡.

Tak¡ gaª¡¹ budowanej struktury nazywamy domkni¦t¡, co

odpowiednio zaznaczamy symbolem ×. W przeciwnym przypadku tak¡ gaª¡» nazywamy otwart¡ i oznaczymy ten fakt symbolem . B¦dziemy rozwa»a¢ tylko tablice zako«czone, czyli o ka»dym li±ciu b¦d¡cym typu × lub .

Oto przykªad dla formuªy niespeªnialnej (p ∨ q) ∧ (¬p ∧ ¬q)



(p ∨ q), (¬p ∧ ¬q)



(p ∨ q), ¬p, ¬q uulllllllllllll

R ))R RR RR RR RR RR R

p, ¬p, ¬q q, ¬p, ¬q

× ×

Zanim opiszemy algorytm musimy jeszcze sklasykowa¢ formuªy:

1 formuªa jest typu α, je±l jest koniunkcj¡ podformuª α1, α₂;

2 formuªa jest typu β, je±li jest alternatyw¡ podformuª β₁, β₂. B¦dziemy te» formuª¦ postaci ¬¬A traktowa¢ jak formuª¦ typu α oraz wykorzystywa¢ znane nam prawa de Morgana.

α α₁ α₂

¬¬A A

A₁∧A₂ A₁ A₂

¬(A₁∨A₂) ¬A₁ ¬A₂

¬(A1 →A2) A1 ¬A2

β β₁ β₂

B1∨B2 B1 B2

¬(B₁∧B₂) ¬B₁ ¬B₂ B₁ →B₂ ¬B₁ B₂

Opis algorytmu tabel semantycznych Wej±cie: Formuªa A.

Wyj±cie: Tabela T dla A, w której ka»da gaª¡¹ jest oznaczona jako domkni¦ta lub otwarta.

Tabel¦ buduje si¦ rozpoczynaj¡c od korzenia zawieraj¡cego zbiór {A} i dodaj¡c nowe wiersze przez analiz¦ pewnego li±cia l wedªug reguª (U(l) oznacza zbiór formuª tego li±cia):

1 Je±li zbiór formuª U(l) zawiera tylko literaªy, to sprawdzamy, czy zawiera literaªy komplementarne. Je±li tak, to oznaczamy go (i gaª¡¹ przez niego wyznaczon¡) jako domkni¦ty

(domkni¦t¡); je±li nie jako otwarty (otwart¡).

2 Je±li U(l) nie jest zbiorem literaªów, to wybieramy formuª¦, która nie jest literaªem.

1 Je±li jest ona typu α, to tworzymy nowy wierzchoªek l⁰ b¦d¡cy potomkiem l zawieraj¡cy zbiór

U(l⁰) = (U(l) \ {α}) ∪ {α1, α₂}

2 Je±li jest ona typu β, to tworzymy dwa nowe wierzchoªki l⁰,l⁰⁰ b¦d¡ce potomkami l zawieraj¡ce zbiory

U(l⁰) = (U(l) \ {β}) ∪ {β₁} U(l⁰⁰) = (U(l) \ {β}) ∪ {β₂}

Obecnie zajmiemy si¦ dowodem caªkowitej poprawno±ci tego algorytmu. Niech T b¦dzie tabel¡ semantyczn¡ jakiejkolwiek formuªy A o wierzchoªku l. Dla zbioru U(l) symbolem F_l oznaczamy koniunkcj¦ wszystkich formuª z tego zbioru.

Lemat

1 Niech l⁰ b¦dzie wierzchoªkiem powstaªym z l przez zastosowanie kroku 2.(a). Wtedy F_l ≡F_l⁰.

2 Niech l⁰,l⁰⁰ b¦d¡ wierzchoªkami powstaªym z l przez zastosowanie kroku 2.(b). Wtedy F_l ≡F_l⁰ ∨F_l⁰⁰.

Dowód Mo»emy zaªo»y¢, »e U(l) = {A₁, . . . ,A_n}i wybran¡ w kroku algorytmu formuª¡ jest A₁.

1 A₁ jest typu α, przykªadowo A₁ = ¬(α₁∨ α₂). Wtedy A1 ≡ ¬α₁∧ ¬α₂ oraz

F_l =A₁∧ . . . ∧A_n≡ ¬α₁∧ ¬α₂∧ . . . ∧A_n=F_l⁰

2 A₁ jest typu β, przykªadowo A₁ = α₁ → α₂. Wtedy A₁ ≡ ¬α₁∨ α₂ oraz

F_l = A₁∧ . . . ∧A_n ≡ (¬α₁∨ α₂) ∧A₂∧ . . . ∧A_n

≡ (¬α₁∧A₂∧ . . . ∧A_n) ∨ (α₂∧A₂∧ . . . ∧A_n)

≡ F_l⁰∨F_l⁰⁰

wykazanie, »e zawsze si¦ on zatrzymuje. W naszym wypadku chodzi o to, »e konstruowane drzewo jest sko«czone. Zanim to wyka»emy zauwa»my, »e li±cie oznakowane zawieraj¡ tylko literaªy.

St¡d wa»ne jest pytanie, kiedy formuªa odpowiadaj¡ca takiemu li±ciowi ma model.

Lemat

Zbór U(l) literaªów ma model wtw, gdy nie zawiera pary literaªów komplementarnych.

Dowód Je±li U(l) = {A1, . . . ,An} i np. A2 = ¬A1,to F_l =A₁∧A₂. . . ∧A_n=A₁∧ ¬A₁. . . ∧A_n≡0 bo 0 ∧ A ≡ 0.

Je±li U(l) nie zawiera pary takich literaªów, to istnieje zbiór zmiennych zdaniowych {z₁, . . . ,z_n}taki, »e A_i ∈ {z_i, ¬z_i} dla ka»dego i = 1, . . . , n. Wtedy nast¦puj¡ce warto±ciowanie jest modelem F_l

v(z_i) =

 1 A_i =z_i 0 A_i = ¬z_i

Algorytm tworzenia tabel semantycznych si¦ zatrzymuje.

Dowód Niech T b¦dzie tabel¡ formuªy A, a l jej wierzchoªkiem.

Niech b(l) równa si¦ liczbie wyst¡pie« operatorów ∨, ∧, → w formuªach zbioru U(l), a n(l) oznacza ilo±¢ negacji w tym zbiorze.

Niech w(l) = 3b(l) + n(l). Wtedy dla potomka l⁰ wierzchoªka l w(l) > w(l⁰). Zaªó»my przykªadowo, »e l⁰ powstaª przez

zastosowanie algorytmu do formuªy ¬(A₁∨A₂). Stosuj¡c prawo de Morgana znika jeden symbol ∨, ale pojawia si¦ dodatkowo negacja, czyli:

w(l⁰) =3(b(l) − 1) + n(l) + 1 = 3b(l) + n(l) − 2 < w(l).

Pozostaªe przypadki analizuje si¦ podobnie. Je±li l jest korzeniem T , to poniewa» w zbiorach pojawiaj¡cych si¦ w tabeli s¡ tylko zmienne wyst¦puj¡ce w U(l) drzewo to musi by¢ sko«czone.

Przykªad

Niech A = (p → q) → ((q → r) → (p → r)) A

 ))RRRRRRRRRRRRRRRR

¬(p → q)



(q → r) → (p → r)

 ((PPPPPPPPPPPPP

p, ¬q ¬(q → r)



p → r

 ""EEEEEEEEE

 q, ¬r ¬p q

Je±li zastanowimy si¦ nad modelami dla A, to z analizy li±ci tej tablicy mamy, »e modelami s¡ takie waro±ciowania v zmiennych p, q, r, które speªniaj¡ jeden z podanych warunków:

1 v(p) = 1, v(q) = 0;

2 v(q) = 1, v(r) = 0;

3 v(p) = 0;

4 v(q) = 1.

a oczyw±cie ka»de warto±ciowanie speªnia jeden z nich.

Prze±led¹my jeszcze dziaªanie algorytmu na formule ¬A, czyli chcemy wykaza¢, »e nie jest ona speªniala (A jest tautologi¡).

¬A

p → q, ¬((q → r) → (p → r))

p → q, q → r, ¬(p → r))

p → q, q → r, p, ¬r

 ++VVVVVVVVVVVVVVVVVV

¬p, q → r, p, ¬r q, q → r, p, ¬r

 ((QQQQQQQQQQQQQ

q, ¬q, p, ¬r q, r, p, ¬r

Oczyw±cie dwa li±cie (drugi i trzeci od lewej) s¡ domkni¦te, ale pierwszy nie zostaª zanalizowany poprawnie, gdy» zawiera formuª¦, która nie jest literaªem! Ale nie ma potrzeby tego robi¢, gdy» ju»

zawiera par¦ formuª komplementarnych.

Wida¢, »e dziaªanie algorytmu tablic semantycznych mo»na usprawni¢ na kilka sposobów:

1 Mo»na oznacza¢ li±¢ jako domkni¦ty, gdy zawiera par¦ formuª komplementarnych.

2 Kopiowanie niezmodykowanych formuª nie jest konieczne.

Wystarczy przechowywa¢ zbiór wska¹ników do formuª.

3 Stosowanie ró»nych heurystyk daje mniejsze drzewa. Na przykªad, najpierw nale»y stosowa¢ reguªy typu α, a potem typu β, dzi¦ki czemu unika si¦ powstawania duplikatów formuª.

Twierdzenie

Niech T b¦dzie tabel¡ zako«czon¡ dla formuªy A. Forrmuªa A jest niespeªnialna wtw, gdy ka»dy jej li±¢ jest domkni¦ty.

Wniosek

Metoda tabel semantycznych jest procedur¡ decyzyjn¡

rozstrzygaj¡c¡ prawdziwo±¢ formuª rachunku zda«.

Dowód Z tw. o zatrzymywaniu mamy, »e konstrukcja tabeli dla 6 A ko«czy si¦ utworzeniem tabeli sko«czonej. Z poprzedniego wniosku mamy, »e A jest prawdziwa wtw, gdy tabela jest domkni¦ta.

Dowód poprawno±ci

Poka»emy ogólniejsz¡ wªasno±¢: jesli poddrzewo o korzeniu n jest domkni¦te, to zbiór formuª U(n) jest niespeªnialny.

Indukcja po wysoko±ci h drzewa U(n).

Podstawa indukcji. Je±li h = 0, to n jest li±ciem. Wtedy T jest domkni¦ta, a U(n) zawiera par¦ literaªów komplementarnych.

Zatem U(n) jest niespeªnialny.

Krok indukcyjny. Je±li h > 0, to do tworzenia potomka u»yto reguªy typu α lub β.

Przypadek 1. U»yto reguªy typu α. U(n) = {A1∧A2} ∪U0, a U(n⁰) = {A₁,A₂} ∪U₀. Wysoko±¢ n⁰ wynosi h − 1 i z zaªo»enia indukcyjnego otrzymujemy, »e U(n⁰) jest niespeªnialny, gdy»

poddrzewo o korzeniu n⁰ jest domkni¦te.We¹my dowolne warto±ciowanie v zbioru U. Mamy jeszcze dwa przypadki:

1 Dla pewnej formuªy A₀∈U₀ mamy v(A₀) =0.

2 Dla jednej z formuª A1,A2 mamy v(Ai) =0

Za ka»dym razem otrzymujemy, »e v(A) = 0, dla dobranych A, a z dowolno±i warto±ciowania otrzymujemy, »e U(n) jest niespeªnialny.

X

Trzeba wykaza¢ te», »e je±li A jest formuª¡ niespeªnialn¡, to ka»da tabela dla A jest domkni¦ta. To jest trudne zadanie. Z tego powodu wyka»emy nieco inne twierdzenie.

Mianowicie, wyka»emy, je±li pewna tabela dla formuªy A jest otwarta, to A jest speªnialna.

Denicja

Mówimy, »e zbiór formuª U jest zbiorem Hintikki wtw, gdy

1 Dla ka»dego atomu p wyst¦puj¡cego w pewnej formule z U zachodzi p /∈ U lub ¬p /∈ U.

2 Je±li α ∈ U jest typu α, to α1, α₂ ∈U.

3 Je±li β ∈ U jest typu β, to β1 ∈U lub β2 ∈U.

Twierdzenie

Niech l bedzie otwartym li±ciem w zako«czonej tabeli semantycznej T . Niech U = S_iUi, po wszystkich i na gaª¦zi z korzenia do wierzchoªka l. Wtedy U jest zbiorem Hintikki.

Dowód

Je±li literaª m wyst¡pi pierwszy raz w U(n), to wyst¡pi na drodze z U(n) do U(l). Oznacza to, »e wszystkie literaªy z U nale»¡ do U(l). Gaª¡¹ ta jest otwarta, wi¦c nie zawiera pary literaªów komplementarnych, czyli pierwszy warunek zachodzi.

Niech α ∈ U b¦dzie typu α, a w pewnym wierzchoªku n u»yto reguªy typu α. Z konstrukcji tabeli wynika, »e oba jej skladniki nale»¡ do U(n⁰) ⊆U, czyli warunek drugi te» jest speªniony.

Trzeci przypadek rozwa»amy analogicznie.

Twierdzenie

Lemat Hintikki Ka»dy zbiór Hintikki jest speªnialny.

N

iech {p1, . . . ,pn} b¦dzie zbiorem wszystkich formuª atomowych wyst¦puj¡cych w formuªach ze zbioru U. Deniujemy

warto±ciowanie wzorami:

v(p) =







1 p ∈ U

0 ¬p ∈ U

1 p 6∈ U i ¬p 6∈ U

Dowód twierdzenia o peªno±ci. Z przedostatniego twierdzenia wiemy, »e zbiór formuª U wyst¦pujacych w otwartej gaª¦zi drzewa T jest zbiorem Hintikki. Z nast¦pnego, istnieje model U, a A wyst¦puje w korzeniu T . St¡d A ∈ U i model U jest modelem A. a poniewa»