Rachunek zda«

(1)

Plan referatu Wprowadzenie Rachunek zda«

Logiczne Aspekty Informatyki

Barbara Klunder(umk)

14 pa¹dziernik 2009

(2)

1 Wprowadzenie Rachunek zda«

Rachunek predykatów Dowodzenie i programowanie

2 Rachunek zda«

Formuªy rachunku zda«

Speªnialno±¢, prawdziwo±¢ i logiczna równowa»no±¢

(3)

Rachunek zda«

Rozpoczynamy

Zajmowa¢ b¦dziemy si¦ logik¡ matematyczn¡. Nauk¦ t¦ wprowadzili staro»ytni Grecy. Logika byªa u»ywana do formalnego opisu

dedukcji, czyli wyprowadzania prawdziwych twierdze« (wniosków) ze stwierdze« przyjmowanych jako prawdziwe (aksjomatów).

Wielki rozkwit prze»ywaªa logika na przeªomie xix i xx wieku, kiedy to matematycy zaj¦li si¦ badaniem podstaw matematyki. W sytuacji gdy teorie stawaªy si¦ coraz bardziej skomplikowane problem poprawno±ci prowadzonych dowodów nabraª wielkiego znaczenia. Najwa»niejszym jednak jest wykazanie, »e zbiór zda«

dowodliwych równy jest zbiorowi zda« prawdziwych.

Logika jest te» cz¦sto stosowana w informatyce do ró»nych celów:

opisu budowy komputerów (bramki logiczne), stworzenia deklaratywnego j¦zyka programowania. opisu semantyki i

(4)

Rachunek zda«

Logika klasyczna zajmuje si¦ badaniem wyra»e« dwuwarto±ciowych, te dwie warto±ci nosz¡ nazw¦ prawdy i faªszu. Formalnie

wprowadza si¦ zbiór zmiennych zdaniowych, operatorów logicznych i wszystkich formuª rachunku zda«, czyli poprawnie zbudowanych wyra»e« logicznych. B¦dziemy posªugiwa¢ si¦ operatorami

∧, ∨, →, ¬czyli koniunkcj¡, alternatyw¡, implikacj¡, negacj¡ itp.

Rachunek zda« mo»e by¢ u»yty do opisu budowy komputerów cyfrowych, gdy» pracuj¡ one z dwoma poziomami napi¦cia

oznaczanymi symbolami 0 (faªsz) i 1 (prawda). Nale»y zaznaczy¢,

»e kwantowy model oblicze« badany intensywnie w ostatnich latach odrzuca to zaªo»enie i uwzgl¦dnia ci¡gªy charakter zycznych zjawisk zachodz¡cych w urz¡deniu elektronicznym jakim jest komputer. Ukªady cyfrowe opisuje si¦ za pomoc¡ elementów zwanych bramkami logicznymi, które symuluj¡ obliczanie warto±ci formuª rachunku zda«.

(5)

Rachunek zda«

Obwód

Na rysunku przedstawiony jest obwód (tzw. half adder)

wykorzystywany do budowy sumatorów. Realizuje on cz¦±ciowo dodawanie dwóch bitów (A i B), gdy» na wyj±ciu S pojawia si¦ A t B, czyli wykluczaj¡ca si¦ alternatywa A i B b¦d¡ca osatni¡ cyfr¡

sumy, a na C pojawia si¦ A ∧ B, czyli obliczane jest przeniesienie.

(6)

Rachunek zda«

Rachunek predykatów

Rachunek zda« jest zbyt ubogi aby wyrazi¢ wiele teorii matematycznych np. arytmetyk¦, w której mamy okre±lone dodawanie 2 + 3 i zdania typu 4 < 2 + 3. Oczyw±cie ka»dy z nas potra przyporz¡dkowa¢ warto±¢ logiczn¡ zdaniu 4 < 2 + 3. Ale wyra»enie logiczne x < y staje si¦ zdaniem, prawdziwym lub nie, po nadaniu warto±ci zmiennym x i y. Formalnie < jest operatorem ze zbioru N × N w zbiór {0, 1} warto±ci logicznych. To jest podej±cie wygodne dla informatyka. Nale»y jednak zaznaczy¢, »e dokonali±my w ten sposób uto»samienia podzbioru <⊂ N × N z jego funkcj¡

charakterystyczn¡. Systemy logiczne dopuszczaj¡ce takie operatory nazywamy rachunkami predykatów lub logikami pierwszego rz¦du.

(7)

Rachunek zda«

U»ycie predykatów dla nadania semantyki instrukcji

Wszystkie j¦zyki imperatywne wysokiego poziomu daj¡ mo»liwo±¢

budowania wyra»e« arytmetycznych, ich porównywania i wykorzystywania wyra»e« typu x < y + 1 w instrukcjach warunkowych i p¦tli.

U»ycie predykatów dla opisu semantyki instrukcji Dla instrukcji

if x >= 0 then y := sqrt(x) else y := abs(x) mo»na poda¢ formuª¦ opisuj¡c¡ wykonanie tej instrukcji, gdzie x⁰,y⁰ oznaczaj¡ warto±¢ zmiennych x, y po jej wykonaniu:

∀_x∀_y(x⁰ =x ∧ (x > 0 → y⁰=p

(x)) ∧ (x < 0 → y⁰ = |x|))

(8)

Rachunek zda«

U»ycie predykatów dla werykacji programu Niech P b¦dzie nast¦puj¡cym programem:

while a <> b do

if a > b then a := a − b else b := b − a;

Jego specykacja opisana jest formuª¡:

{a > 0 ∧ b > 0} P {a = nwd(a, b)}

(9)

Rachunek zda«

Deklaratywny styl programowania

Dziedzina informatyki zwana sztuczn¡ inteligencj¡ zajmuje si¦

zagadnieniem mo»liwo±ci na±ladowania przez komputer procesów my±lowych czªowieka. Czy komputer jest w stanie odkrywa¢ dowody twierdze«, czyli prowadzi¢ bardzo wyranowane rozumowania?

Co prawda udowodnimy, »e nie zawsze, ale istniej¡ systemy dowodzenia twierdze«, przy pomocy których udowodniono nawet nowe twierdzenia a cz¦sto przypomina si¦ o wykorzystaniu

komputerów do rozwi¡zania zagadnienia czterech barw (porównaj http://www.wiw.pl/deltacztery_barwy.asp ) Badania w tej dziedzinie doprowadziªy do opracowania nowej, efektywnej metody dowodzenia pewnych twierdze« zwanej rezolucj¡.

(10)

Rachunek zda«

Zastosowanie tej metody nazywane jest programowaniem w logice.

W j¦zykach programowania w logice, z których najpopularniejszym jest prolog, zadaniem programisty jest podanie formuª poprawnie opisuj¡cych zale»no±ci pomi¦dzy danymi wej±ciowymi i

wyj±ciowymi. Nast¦pnie uruchamiany jest system dowodzenia w celu znalezienia odpowiedzi. To podej±cie nosi nazw¦

programowania deklaratywnego.

(11)

Zdania

Denicja

Zdania Niech P b¦dzie pewnym niepustym zbiorem, którego elementy nazywa¢ b¦dziemy zdaniami prostymi lub zmiennymi zdaniowymi. symbole ∨, ∧, →, ¬ zwane alternatyw¡, koniunkcj¡, implikacj¡ i negacj¡, b¦dziemy nazywa¢ spójnikami

zdaniotwórczymi. Zbiór formuª (zda« zªo»onych) F (zbudowanych ze zda« prostych P) deniujemy jako j¦zyk rekurencyjny nad alfabetem

X = P ∪ {(, ), ¬, ∧, ∨, →}

wyznaczony przez

1 j¦zyk bazowy P,

2 i konteksty: (t₁∨ t₂), (t₁∧ t₂), (t₁ → t₂), ¬(t).

(12)

Inaczej: rozwa»my funkcj¦ F_Z :2^X^? 7→2^X^? okre±lon¡ wzorem:

F_Z(J) = J ∪ {(p ∨ q); p, q ∈ J} ∪ {(p ∧ q); p, q ∈ J}∪

{(p → q); p, q ∈ J} ∪ {¬(p); p ∈ J}.

Wtedy F = S_n∈NF_Zⁿ(P), gdzie F_Z⁰(J) = J, F_Zⁿ⁺¹=F_Z(F_Zⁿ(J)).

Denicja rekurencyjna F poci¡ga te», »e zachodzi nast¦puj¡ce Twierdzenie

Zbiór F ⊆ X^? jest najmniejszym j¦zykiem speªniaj¡cym:

1 P ⊆ F ;

2 je±li p, q ∈ F , to ¬(p), (p ∨ q), (p ∧ q), (p → q) ∈ F .

Twierdzenie to wykorzystujemy cz¦sto przy dowodzeniu twierdze«

dotycz¡cych formuª rachunku zda« i deniowaniu funkcji na zbiorze F .

(13)

W dalszych rozwa»aniach zbiory P i F s¡ ustalone. My±l¡c o zastosowaniach informatycznych nale»y zastanowi¢ si¦ jakich struktur u»y¢ do zapami¦tania formuªy.

Przykªad Rozwa»my formuª¦ ((p → q) ∧ (r ∨ q)) i pytanie: czy zmienna r si¦ w niej pojawia? Aby na nie odpowiedzie¢ analiza sªowa jest wystarczaj¡ca. Ale na pytanie o maksymalne

zagnie»d»enie nawiasów jest ju» trudniej odpowiedzie¢. Je±li jednak zbudujemy struktur¦ drzewiast¡

∧ }}zzzzzzzz

C!!C CC CC CC

→

~~}}}}}}}}

D!!D DD DD

DD ∨

}}||||||||

??

?

p q r q

(14)

Drzewo to oddaje sposób zagnie»d»enia nawiasów i st¡d mo»na je wyznaczy¢ jednoznacznie.

Uwaga Zwykle nie b¦dziemy pisa¢ zewn¦trznego nawiasu, gdy» jest on zb¦dny.

Tak jak w przypadku wyra»e« arytmetycznych wprowadza si¦

priorytety operatorów, aby unikn¡¢ u»ycia zb¦dnych nawiasów.

Priorytety te od najwy»szgo s¡ nast¦puj¡ce: negacja, koniunkcja, alternatywa, implikacja, równowa»no±¢.

(15)

Przykªad

Zgodnie z tymi zasadami formuªa p → q ∨ r ∧ q to w istocie p → (q ∨ (r ∧ q)). Drzewo tej formuªy wygl¡da nast¦puj¡co:

→

~~}}}}}}}}

B B BB BB BB

p ∨

~~}}}}}}}}

??

q ∧

??

r q

(16)

Je±li chcemy unikn¡¢ nawiasów i zachowa¢ liniow¡ reprezentacj¦

formuªy w postaci sªowa, które wystarczy przeczyta¢ (od lewej do prawej lub od prawej do lewej), aby rozpozna¢ jego struktur¦, wystarczy zastosowa¢ notacj¦ polsk¡. Najpierw przechodzimy drzewo w gª¡b i otrzymujemy sªowo → p ∨ q ∧ rq, nast¦pnie czytaj¡c je od prawej do lewej i wykorzystuj¡c tylko dwie komórki pami¦ci mo»emy np. ªatwo obliczy¢ warto±¢ logiczn¡ formuªy dla ustalonego warto±ciowania zmiennych w niej wyst¦puj¡cych.

(17)

Symbolem 2 oznacza¢ b¦dziemy dwelementow¡ algebr¦ Boole'a o no±niku {0, 1} wyró»nionych elementach 0, 1 i dziaªaniach

opisanych w tabelach:

∧ 0 1 0 0 0 1 0 1

∨ 0 1 0 0 1 1 1 1

⇒ 0 1

0 1 1 1 0 1

¬ 0 1 1 0

(18)

Denicja

Ka»d¡ funkcj¦ v : P 7→ {0, 1} nazywamy warto±ciowaniem (logicznym) zda« prostych. Ka»d¡ tak¡ funkcj¦ mo»na rozszerzy¢

na zbiór F formuª deniuj¡c v : F 7→ {0, 1} wzorami:

v(z) = v(z) z ∈ P

v(¬z) = ¬v(z) z ∈ F

v(pq) = v(p)v(q) p, q ∈ F , ∈ {∨, ∧, ⇒}

Denicja

Formuª¦ z ∈ F nazywamy speªnialn¡, je±li istnieje warto±ciowanie v : P 7→ {0, 1} takie, »e v(z) = 1, mówimy wtedy, »e z jest speªniona przy warto±ciowaniu v. Formuª¦ z ∈ F nazywamy tautologi¡, je±li formuªa ¬z nie jest speªnialna.

(19)

Zadanie 1.

Wyka», »e formuªa z ∈ F jest tautologi¡ wtw, gdy jest speªnialna przy ka»dym warto±ciowaniu.

Zadanie 2.

Wyka», »e nast¦puj¡ce formuªy s¡ tautologiami; dla p, q ∈ F napis p ↔ q oznacza zdanie postaci p → q ∧ q → p

1 p ∨ ¬p;

2 ¬(¬p) ↔ p;

3 ¬(p ∨ q) ↔ (¬p ∧ ¬q);

4 (p → q) → ((q → r) → (p → r))

(20)

Ostatnia formuªa s nosi nazw¦ prawa sylogizmu.Je±li wykorzystamy w zadaniu 2. zadanie 1. to musimy rozpatrzy¢ osiem waro±ciowa«, gdy» w formule wyst¦puja trzy zmienne. Zwykle wtedy buduje si¦

tablic¦ logiczn¡, której wiersze s¡ wyznaczane przez

warto±ciowanie, a kolumny odpowiadaj¡ podformuªom, których waro±¢ logiczna jest potrzeba do obliczenia warto±ci caªej formuªy.

Mamy wi¦c

p q r p → q q → r p → r ((q → r) → (p → r)) s

0 0 0 1 1 1 1 1

0 0 1 1 1 1 1 1

0 1 0 1 0 1 1 1

1 0 0 0 1 0 0 1

0 1 1 1 1 1 1 1

1 0 1 0 1 1 1 1

1 1 0 1 0 0 1 1

1 1 1 1 1 1 1 1

(21)

Wida¢, »e taki algorytm zale»y wykªadniczo od ilo±ci zmiennych pojawiaj¡cych si¦ w formule. Mo»emy sie te» zastanawia¢, czy zgodnie z denicj¡ negacja s jest speªnialna. Tutaj mo»emy ªatwo wywnioskowa¢, »e v(s) = 0 tylko, gdy v(p → q) = 1 i

v((q → r) → (p → r)) = 0. A to zachodzi tylko, gdy

v(q → r) = 1 i v(p → r) = 0. St¡d v(p) = 1, v(r) = 0 i v(q) = 0.

Mamy wi¦c do rozpatrzenia tylko jedno warto±ciowanie! A przy tym warto±ciowaniu v mamy v(p → q) = 0, co przeczy pozostaªym zaªo»eniom. Reasumuj¡c negacja s nie jest speªnialna.

(22)

Denicja

Dwie formuªy A, B ∈ F s¡ logicznie równowa»ne, je±li dla ka»dego warto±ciowania v : P 7→ {0, 1} mamy v(A) = v(B). B¦dziemy stosowa¢ oznaczenie A ≡ B.

Intuicja jest jasna; semantycznie formuªy A i B s¡ nie do odró»nienia. Nietrudno udowodni¢

Twierdzenie

Dla formuª A, B mamy: A ≡ B wtedy i tylko wtedy, gdy formuªa A ↔ B jest tautologi¡.

Odt¡d do zbioru formuª b¦dziemy równie» zalicza¢ staªe 0, 1 odpowiadaj¡ce warto±ciom logicznym faªszu i prawdy.

(23)

Oto zestawienie wa»nych, cho¢ czasem banalnych formuª logicznie równowa»nych, które nale»y zapami¦ta¢:

A ∨ 0 ≡ A A ∧ 1 ≡ A

A → 0 ≡ ¬A A → 1 ≡ 1

A ≡ ¬¬A A ≡ A ∨ A

A ≡ A ∧ A A ∧ ¬A ≡ 0

A ∨ ¬A ≡ 1 A → A ≡ 1

A ∨ B ≡ B ∨ A A ∧ B ≡ B ∧ A

A ∨ (B ∨ C) ≡ (A ∨ B) ∨ C A ∧ (B ∧ C) ≡ (A ∧ B) ∧ C

A ∧ (A ∨ B) ≡ A A ∨ (A ∧ B) ≡ A

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

A → B ≡ ¬A ∨ B A → B ≡ ¬(A ∧ ¬B)

(24)

Podane równowa»no±ci b¦dziemy wykorzystywa¢ do upraszczania formuª. W danej formule b¦dziemy szuka¢ jej podformuªy i zast¦powa¢ j¡ logicznie równowa»n¡. oto przykªad:

p ∨ (¬p ∧ q) ≡ (p ∨ ¬p) ∧ (p ∨ q) ≡

1 ∧ (p ∨ q) ≡

(p ∨ q)

Zdenujmy dwa j¦zyki SAT i T odpowiednio formuª, które s¡

speªnialne i s¡ tautologiami. Mo»emy si¦ zastanawia¢ nad zªo»ono±ci¡ czasow¡ problemów:

formuªa nale»y do SAT (speªnialno±¢);

formuªa nale»y do T (prawdziwo±¢).

(25)

Bezpo±rednio z denicji wynika algorytm o zªo»ono±ci wykªadniczej.

Wiadomo (Twierdzenie Cooka), »e problem speªnialno±ci (a wi¦c i prawdziwo±ci) jest NP-zupeªny. Tak wi¦c ustalenie, czy istnieje algorytm o wielomianowej czasowej zªo»ono±ci obliczeniowej dla nale»enia do SAT pozwoli rozstrzygn¡¢, czy P = NP.

Przypomnijmy, »e problem równo±ci klas zªozono±ci obliczeniowej P i NP jest jednym z siedmiu problemów milenijnych!

(26)

Na drodze do znalezienia lepszego algorytmu dla problemu

speªnialno±ci (tautologii) pojawiªo si¦ te» podej±cie syntaktyczne:

budowano systemy formalne, w których ustalenie, czy z ∈ F jest tautologi¡ sprowadza si¦ do analizy skªadniowej z, czyli budowy, ksztaªtu z. Prykªadem takiego systemu jest system Hilberta. Zanim omówimy taki system zajmiemy si¦ metod¡ tablic semantycznych i rezolucj¡, które równie» wykorzystuj¡ analiz¦ skªadniow¡ formuªy do rozstrzygni¦cia, czy jest ona speªnialna.

(27)

W metodach tych rozwa»a si¦ zbiory formuª.

Denicja

Zbiór formuª U = {A₁, . . . ,A_n} jest (jednocze±nie) speªnialny, je±li istnieje warto±cowanie v, zwane modelem dla U, przy którym wszystkie formuªy zbioru s¡ speªnialne, czyli

v(A₁) = . . . =v(A_n) =1.

W nast¦pnym twierdzeniu zebrane s¡ wa»ne, acz proste wªasno±ci zbiorów speªnialnych.

(28)

Twierdzenie

1 Je±li U jest speªnialny i V ⊆ U, to V jest speªnialny.

2 Je±li U jest speªnialny i B jest tautologi¡, to U ∪ {B} jest speªnialny.

3 Je±li U nie jest speªnialny i U ⊆ V , to V nie jest speªnialny.

4 Je±li U nie jest speªnialny i A_i ∈U jest tautologi¡, to U \ {A_i} nie jest speªnialny.

(29)

Denicja

Je±li U jest zbiorem formuª, a A formuª¡, to A jest konsekwencj¡

logiczn¡ U (symbolicznie U |= A), je±li dla ka»dego modelu v dla U, v jest modelem dla A.

Przykªad Niech U = {p → q, q → r} i A = p → r. Z ostatniego zadania mamy od razu, »e U |= A.

Ostatni¡ denicj¦ rozszerzymy na przypadek, gdy U jest zbiorem pustym przyjmuj¡c, »e ka»de warto±ciowanie jest modelem dla zbioru pustego. B¦dziemy pisa¢ |= A, gdy ∅ |= A. Zauwa»my, »e

|=A wtw, gdy A jest tautologi¡!

(30)

Twierdzenie

1 U |= A wtw, gdy |= A₁∧ . . . ∧A_n→A.

2 Je±li U |= A i U ⊆ V , to V |= A.

3 Je±li U |= A i B jest tautologi¡, to U \ {B} |= A.

Denicja

Zbiór formuª T nazywamy teori¡, gdy jest domkni¦ty na konsekwencje logiczne: dla ka»dej formuªy A warunek T |= A poci¡ga A ∈ T .

Zauwa»my, »e z Twierdzenia 3.10 (punkt 2.) otrzymujemy od razu,

»e ka»da teoria T zawiera wszystkie tautologie!

(31)

Niech U b¦dzie zbiorem formuª,a

T (U) = {A ∈ F ; U |= A}

zbiorem wszystkich konsekwencji logicznych U. Nietrudno pokaza¢,

»e T (U) jest teori¡ generowan¡ przez U. Wtedy elementy U s¡

nazywane aksjomatami.