Logica propoziţională
-
Upload
alexandru-tudose -
Category
Documents
-
view
66 -
download
5
description
Transcript of Logica propoziţională
-
Capitolul 2
Logica propoziional
(Calculul propoziional)
Manualele de Logic i Algebr ([BIE], [DID]) pot fi privite ca
o introducere (firav) n logica formal. i n alte manuale de
matematic (i nu numai), sunt prezente frecvent noiuni ca afirmaie,
axiom, teorem, raionament, demonstraie, etc. Aceste noiuni sunt
ns descrise sau concepute/receptate/folosite la modul informal: o
afirmaie este orice propoziie (fraz) care poate cpta o unic valoare
de adevr (a adevrat, f fals); o axiom este o afirmaie care se
accept a fi adevrat fr a se cere o demonstraie a ei; o teorem este
o afirmaie (presupus a fi adevrat) care se obine (din axiome sau
teoreme deja acceptate) printr-o demonstraie (formal), numit i
raionament; o demonstraie (formal) este transpunerea ntr-o form
(mai) exact a unui raionament; un raionament este o succesiune
(finit) de aplicri ale unor inferene (reguli de deducie); o regul de
deducie (inferen) are forma: premize/concluzii (att premizele ct i
concluziile sunt afirmaii, ideea fiind aceea c regulile sunt astfel
construite nct dac premizele sunt adevrate atunci i concluziile sunt
adevrate; se mai spune c inferenele sunt n acest caz valide sau
corecte), etc. De altfel, acesta este modul principal prin care se obin
(constructiv) n tiinele exacte noiuni noi (utiliznd definiiile) i
afirmaii (adevrate) noi (utiliznd raionamentele). Din punctul de
vedere al logicii filozofice, o noiune este complet caracterizat de
-
44 Cristian Masalagiu
coninut (element din structura noiunii alctuit din mulimea
proprietilor obiectelor care formeaz sfera noiunii) sau sfer
(element din structura noiunii alctuit din mulimea obiectelor ale
cror proprieti formeaz coninutul noiunii). O definiie ar avea
astfel rolul de a delimita precis sfera (coninutul) noiunii. Definirea
unei noiuni noi nseamn delimitarea unei noi sfere (sau a unui nou
coninut), ceea ce se poate face de exemplu (exist i alte tipuri
generale de definiii) prin precizarea unei sfere vechi (care
caracterizeaz complet o noiune anterior definit, numit gen proxim)
i a unei mulimi de proprieti suplimentare (care nu fac parte din
coninutul vechii noiuni, dar care mpreun cu acesta vor alctui
noul coninut), numit diferen specific: un paralelogram este un
patrulater convex care are dou laturi paralele i egale; un romb este
un paralelogram cu toate laturile egale; un ptrat este un romb avnd
un unghi de 90, . a. m. d. n acest mod, mergnd invers, procesul de
definire a unor noiuni ar deveni infinit dac nu am accepta existena
unor noiuni primare (pentru o mai bun nelegere se poate recurge i
la reprezentri grafice cum ar fi diagramele Venn-Euler [IP]).
Noiunile primare nu mai sunt definite prin schema gen proxim i
diferen specific ci sunt doar descrise cu ajutorul unor elemente
considerate a fi suficiente pentru delimitarea exact a sferei curente de
sfera altor noiuni (asemenea definiii sunt cunoscute i sub numele de
definiii operaionale): o mulime este o colecie de obiecte distincte
dou cte dou; un punct este ceea ce se obine prin apsarea unui vrf
de creion pe o foaie de hrtie, etc. Un proces similar are loc i n cazul
conceptelor de axiom (n rolul noiunilor primare), teorem (n
-
Fundamentele logice ale Informaticii 45
rolul noiunilor noi), regul de inferen (n rolul diferenei
specifice), acceptarea axiomelor ca fiind advrate fr demonstraie
avnd desigur scopul de a evita raionamentele infinite. Aa cum n
momentul definirii unei noiuni (noi) trebuie s fim ateni ca sfera
acesteia s fie nevid i (n general) distinct de sferele unor noiuni
deja existente (chiar definite operaional), n cazul raionamentelor este
de dorit ca axiomele s reprezinte cu certitudine afirmaii
adevrate, iar inferenele s fie valide (inferenele trebuie s fie valide
pentru a avea raionamente corecte, adic formate numai din afirmaii
adevrate). Din pcate, datorit lipsei unei sintaxe clare pentru
conceptul de afirmaie (lipsei definiiilor formale n general), precum i
datorit amalgamrii consideraiilor de natur sintactic i semantic,
eafodajul anterior este destul de ubred putnd conduce la apariia
unor paradoxuri de gndire sau la acceptarea unor adevruri hilare.
Prima parte a capitolului este destinat unei scurte treceri n revist a
unor asemenea anomalii i introducerii primelor elemente de logic
(informatic) formal.
1. Logica, parte a filozofiei
Ambiguitile permise de limbajul natural, acceptarea utilizrii unor
noiuni primare sau a unor axiome avnd coninut ambiguu n
raionamente complexe, tratarea simultan a unor probleme de natur
sintactic mpreun cu altele care implic semantica, au creat de-a
lungul timpului numeroase confuzii i interpretri greite, bruind
comunicarea inter-uman. Un prim tip de asemenea confuzii, cunoscute
-
46 Cristian Masalagiu
sub numele de paradoxuri logice, sunt deja clasificate, mprite pe
categorii. Nu este simplu s dm o definiie unanim acceptat (de altfel,
B. Russell a mprit paradoxurile n apte categorii, avnd definiii
practic diferite). Pentru unii, un paradox este o afirmaie care pare s
se autocontrazic, sau poate conduce la o situaie care contrazice
bunul sim. Mai general, este orice afirmaie surprinztoare,
alambicat, contrar intuiiei, sau, o argumentaie aparent solid,
corect, dar care conduce la o contradicie. Pentru alii, este o
propoziie care i afirm propria falsitate, sau, un argument care
conduce la o concluzie contradictorie dei ncepe cu nite premize
acceptabile i se folosete o deducie valid. Oricum, se accept faptul
c un paradox nu nseamn acelai lucru cu o contradicie. Astfel,
afirmaia Aceast cma este albastr i aceast cma nu este
albastr este o contradicie, dar un paradox va apare atunci cnd o
persoan face o anumit presupunere i apoi, urmnd o argumentaie
logic, ajunge la contrariul presupunerii iniiale. Nu spun niciodat
adevrul este considerat un paradox (al mincinosului), deoarece dac
presupunem c propoziia este adevrat atunci rezult imediat c ea
este fals si reciproc. Mai sus este vorba despre o clas mai simpl de
paradoxuri (numite i semantice). Practic, ele ar putea fi rezolvate
daca sunt eliminate complet din logica clasic, deoarece pot fi
considerate ca afirmaii crora nu li poate ataa o unic valoare de
adevr (contradiciilor nu li se poate practic ataa nici una!). Un
paradox mai complicat este paradoxul lui B. Russell, legat de teoria
mulimilor : Dac R este mulimea tuturor mulimilor care nu se
conin pe ele nsele, atunci R se conine pe sine nsi ca element?.
-
Fundamentele logice ale Informaticii 47
Imediat se obine c dac rspunsul este DA, atunci R nu se conine
pe ea nsi i dac rspunsul este NU, atunci R se conine.
Contradicia provine aici din acceptarea axiomei nelegerii: Dac P
este o proprietate (relaie, predicat), atunci M = {x | P(x)} este o
mulime (paradoxul precedent se obine lund P(x): x nu este
element al lui x). Matematic vorbind, paradoxul dispare dac se
renun la axioma nelegerii (mai exact, M de mai sus nu este o
mulime, ci o clas). Un alt paradox, cunoscut nc din antichitate, este
paradoxul lui Ahile i broasca estoas, atribuit lui Zenon: Ahile i o
broasc estoas se iau la ntrecere ntr-o alergare de vitez, Ahile
aflndu-se iniial ntr-un punct A i broasca n faa sa, la o distan a,
ntr-un punct B, dar ncepnd s se deplaseze amndoi n acelai
moment i n aceeai direcie. Afirmaie: Ahile nu va ajunge din urm
broasca (chiar dac broasca ar avea...viteza 0). Putem demonstra
afirmaia raionnd astfel: fie C mijlocul distanei dintre A i B; pentru
a ajunge n B, Ahile trebuie s ajung nti n C; fie acum D mijlocul
distanei dintre A i C, etc. Cum mulimea numerelor reale este dens,
mereu mijlocul unui segment de lungime diferit de zero va genera alte
dou segmente de lungime nenul, astfel nct Ahile nu va ajunge
niciodat broasca. Acest tip de paradox se numete i aporie,
contradicia provenind, n cazul nostru, din utilizarea unui raionament
corect intr-un mediu necorespunztor (drumurile, n legtur cu
deplasarea unor fiine, nu pot fi considerate drept reprezentri ale axei
reale). Dei nu sunt ele nsele absurditi, silogismele reprezint o
alt surs generoas de confuzii. Inferenele, adic paii elementari
(considerai a fi indivizibili) ai unui raionament, reprezint forme
-
48 Cristian Masalagiu
logice complexe. Aceste raionamente elementare se mpart n
deductive i inductive, iar cele mai simple inferene sunt cele imediate,
cu propoziii categorice (fiind formate din dou asemenea propoziii: o
premiz, i o concluzie). Silogismul este tipul fundamental de inferen
deductiv mediat alctuit din exact trei propoziii categorice: dou
premize, dintre care una major i alta minor, precum i o concluzie.
Silogismele se pot de altfel mpri n ipotetice, categorice, disjunctive,
etc. (nu insistm asupra altor detalii). Un exemplu de silogism
(categoric, corect) este:
Premiza major: Toate elementele transuranice sunt
radioactive.
Premiza minor: Plutoniul este element transuranic.
Concluzia: Plutoniul este radioactiv.
Pentru a folosi ns doar silogisme corecte (valide), este necesar un
studiu mai aprofundat al acestora. n caz contrar, putem ajunge, ca i n
cazul paradoxurilor, s acceptm nite aberaii drept propoziii
adevrate. De exemplu:
Greeala n silogismul anterior const n aceea c nu se ine cont de o
lege a silogismelor, care stipuleaz c ntr-un silogism valid exist trei
i numai trei termeni lingvistici distinci. Din pcate ns, n limba
Alb este adjectiv
Zpada este alb
Zpada este adjectiv
-
Fundamentele logice ale Informaticii 49
romn (dar nu numai) un acelai cuvnt (sau grup de cuvinte) poate
materializa mai mult dect o singur noiune. Astfel, dei n exemplul
nostru s-ar prea c avem exact trei termeni distinci (alb, adjectiv,
zpada), n realitate avem patru: n premiza major cuvntul alb
materializeaz un element al limbajului (o parte de vorbire), iar n
premiza minor el red o nsuire (care este caracteristic i zpezii).
Neconcordanele pot fi eliminate dac legile de genul amintit ar putea fi
prinse n forma sintactic exact a silogismului. Profitm de prilej
pentru a aminti i cteva idei legate de inferenele (raionamentele)
deductive cu propoziii compuse. Dei acestea nu sunt automat
generatoare de ambiguiti/aberaii, folosirea incorect a implicaiei
logice n cadrul lor poate produce neplceri. Mai nti, s observm c
putem considera c am definit structural ntreaga (sau mcar o parte
important a sa) mulime de afirmaii pe care le manipulm n limbaj
natural, n modul sugerat de logica clasic: pornim de la anumite
afirmaii (Baza - propoziii elementare) i apoi (Pas constructiv)
formm propoziii noi (fraze, propoziii compuse), din propoziii vechi
cu ajutorul unor operatori (conectori), cum ar fi sau, i, negaia,
implicaia (dac ... atunci ...), echivalena (dac ... atunci ... i
reciproc). Notnd cu A i B dou propoziii oarecare (elementare sau
compuse), putem forma propoziiile compuse (de acum nainte, va
nota egal prin definiie/notaie/convenie): C A sau B (simbolic:
A B); D A i B (simbolic: A B); E non A (simbolic: A);
F dac A atunci B (simbolic: A B; A se numete uneori ipotez
sau antecedent iar B concluzie sau consecvent); G dac A atunci B
-
50 Cristian Masalagiu
i reciproc (sau, A dac i numai dac B, sau A atunci i numai
atunci cnd B; simbolic: A B). Cum A i B pot lua fiecare doar
valorile a - adevrat sau f fals (desigur...nu simultan), la fel se va
ntmpla i cu propoziiile compuse. Astfel, C va fi a atunci i numai
atunci cnd mcar una dintre A i B este a, D va fi a atunci i numai
atunci cnd att A ct i B sunt a, E va fi a atunci i numai atunci cnd
A va fi f, F va fi f atunci i numai atunci cnd A este a i B este f. n
sfrit, G va fi a atunci i numai atunci cnd A i B sunt simultan a sau
simultan f. Ca o consecin, o implicaie va fi adevrat dac ipoteza
este fals, indiferent de valoarea de adevr a concluziei. Acum ne
putem referi n mod explicit i la inferene cu propoziii compuse (se
presupune c silogismele utilizeaz doar propoziii simple), cele
coninnd implicaia fiind des utilizate. Cele mai simple inferene de
acest tip sunt cele care conin dou premize i o concluzie, dintre ele
distingndu-se cele ipotetico-categorice (prima premiz este o
implicaie iar cea de-a doua const fie din antecedentul sau negaia
antecedentului, fie din consecventul sau negaia consecventului
implicaiei respective, conform [BIE]). Schemele valide care se folosesc
n raionamente sunt astfel de forma:
B
A
BA
modus ponendo-ponens (pe scurt, modus ponens)
sau
A
B
BA
modus tollendo-tollens (pe scurt, modus tollens)
-
Fundamentele logice ale Informaticii 51
Validitatea (reamintim: dac ipotezele sunt adevrate, atunci i
concluzia trebuie s fie adevarat) schemelor modus ponens (modul
afirmativ) i modus tollens (modul negativ) rezult imediat din definiia
implicaiei. Oprindu-ne la modus ponens, am putea spune c acesta
poate fi reformulat n: din A (adevrat) i A B (adevrat)
deducem (c) B (adevrat). Pe scurt, vom nota acest lucru prin
A B. Urmtorul exemplu este edificator pentru greelile care se pot
face fie din necunoaterea definiiei reale a implicaiei, fie din
confundarea lui A B (formul n limbajul de baz) cu A B
(formul n metalimbaj, care sugereaz deducerea lui B, pornind de la
A i folosind un raionament).
Exemplu. S considerm funcia f : R R, dat prin:
2
x, dac x 0f (x)=
x +1, dac x>0
S se arate c f este injectiv.
Conform uneia dintre definiiile cunoscute, trebuie s artm c pentru
fiecare x1, x2 R, avem: dac f (x1) = f (x2) atunci x1 = x2. Anticipnd
notatiile din Capitolul 3 i presupunnd cunoscut (cel puin la nivel
informal) semnificaia cuanficatorilor, putem scrie acest lucru sub
forma condensat (x1, x2 R)(f(x1) = f(x2) x1 = x2). Exist
urmtoarele posibiliti:
-
52 Cristian Masalagiu
a) x1, x2 0. Atunci f (x1) = x1 i f (x2) = x2. Prin urmare f(x1) = f(x2)
chiar coincide cu x1 = x2 i deci implicaia f(x1) = f(x2) x1 = x2 este
adevrat.
b) x1, x2 > 0. Atunci f (x1) = x12 + 1 i f (x2) = x2
2 + 1. Prin urmare,
f(x1) = f(x2) nseamn x12 + 1 = x2
2 + 1, ceea ce se ntmpl atunci i
numai atunci cnd (x1 - x2 )(x1
+ x2) = 0. Deoarece variabilele sunt
pozitive, ultima egalitate este echivalent cu x1 - x2 = 0, deci cu x1
= x2.
Am artat de fapt c avem f(x1) = f(x2) dac i numai dac x1 = x2 ceea
ce se poate scrie simbolic (n metalimbaj!) f(x1) = f(x2) x1 = x2. n
consecin, la fel ca la punctul precedent, implicaia cerut
f(x1) = f(x2) x1 = x2 este la rndul ei adevrat (este adevrat chiar
echivalena f(x1) = f(x2) x1 = x2), deoarece este clar c dac
antecedentul f(x1) = f(x2) este adevrat, atunci i consecventul x1 = x2
este adevrat (de fapt, i reciproc).
c) x1 0, x2 > 0. n acest caz f(x1) = x1 i f(x2) = x22 + 1. Atunci
f(x1) = f(x2) nseamn x1 = x22 + 1 i implicaia pe care trebuie s o
artm devine x1 = x22 + 1 x1 = x2, i aceasta pentru fiecare x1 0 i
x2 > 0. Nu mai putem proceda la fel ca n situaiile anterioare, deoarece
din x1 = x22 + 1 nu se poate deduce x1 = x2. Totui, implicaia n cauz
din limbajul de baz este adevrat, deoarece antecedentul ei este
fals. ntr-adevr, oricare ar fi x1 0 i x2 > 0, n egalitatea x1 = x22 + 1,
membrul stng este nepozitiv iar membrul drept este pozitiv, ceea ce
face ca relaia s devin imposibil n contextul dat.
n finalul paragrafului, pentru a introduce i o not optimist,
prezentm una dintre cele mai mari demonstraii cunoscute n
-
Fundamentele logice ale Informaticii 53
literatura tiinific a afirmaiei Oamenii de tiin nu vor ctiga
niciodat la fel de muli bani ca directorii executivi ai unor companii
de succes. n acest scop vom porni de la postulatele (axiomele)
Cunoaterea nseamn putere i Timpul nseamn bani, pe care le vom
folosi sub forma prescurtat: cunoatere = putere i respectiv
timp = bani. Ca inferene, le vom utiliza pe cele mai simple (imediate,
cu afirmaii categorice), la care adugm altele la fel de simple,
cunoscute din matematica elementar. Plecm astfel de la axioma
suplimentar:
muncputere
timp
Folosind axiomele iniiale i proprietile relaiei de egalitate, printr-o
inferen simpl deducem:
munccunoatere
bani
Aplicnd acum o proprietate a proporiilor, gsim:
munc= bani
cunoatere
Cititorul poate trage singur concluzia care se impune pentru situaia n
care cunoatere se apropie de (tinde la) valoarea zero.
Ca o concluzie, situaiile neplcute descrise anterior trebuie
evitate sau eliminate. Acest lucru se poate face doar prin translatarea
prilor de limbaj ntr-un mecanism formal bine pus la punct, pe care-l
vom descrie ncepnd cu seciunea/paragraful urmtoare/urmtor.
Enunul unora dintre exerciiile care urmeaz este reluat n 2.10.
-
54 Cristian Masalagiu
Exerciiul 2.1. O teorem, n sensul matematicii de liceu, are i ea
ipoteze i concluzii. Scriei simbolic forma general a unei teoreme
(directe), utiliznd propoziii elementare (variabile propoziionale) i
conectori logici. Scriei apoi teorema reciproc, contrara teoremei
directe i contrara reciprocei. Exist vreo legtur ntre acestea, n
ceea ce privete valoarea lor de adevr? Dai un exemplu de teorem
de caracterizare (A dac i numai dac B). Putei specifica altfel
rezultatul exprimat de teorem, astfel nct s fie separat - puse n
eviden condiia necesar i condiia suficient?
Exerciiul 2.2. S considerm definiia limitei unui ir dat de
numere reale, avnd ca valoare un numr real dat, definiie exprimat
cu ajutorul vecintilor care sunt intervale simetrice fa de punctul
considerat. S se exprime simbolic (n sensul matematicii de liceu,
folosind i cuantificatorii) aceast definiie i s se nege formula astfel
gsit.
Exerciiul 2.3. Exprimai simbolic, ca o formul n sensul
exerciiilor anterioare propoziia Dac mi-e sete, beau ap. Negai
formula i apoi rescriei rezultatul n limbaj natural. Dac ai fi negat
direct propoziia iniial, ai fi obinut acelai lucru?
n restul capitolului, cteva dintre concepte/rezultate/exemple
sunt din [MAS1] (trebuie s precizm c o parte dintre acestea provin,
la origine, din [SCH]).
2. Sintaxa logicii propoziionale
-
Fundamentele logice ale Informaticii 55
Vom trece direct la prezentarea sintaxei formale a logicii
propoziionale (calculului propoziional). Logica propoziional, aa
cum am sugerat deja, va fi numele unei mulimi de formule
(propoziionale), notat LPL sau, prescurtat, LP i definit structural n
cele ce urmeaz.
Definiia 2. 1. Fie o mulime numrabil de variabile propoziionale
(formule elementare, formule atomice pozitive, atomi pozitivi),
A = {A1, A2, }. Fie, de asemenea, C = {, , } mulimea
conectorilor/conectivelor logici/logice non (negaia), sau (disjuncia),
respectiv i (conjuncia) i P = { ( , ) } mulimea parantezelor
(rotunde). Formulele (elementele lui LP) vor fi cuvinte (expresii bine
formate) peste alfabetul L = A U C U P:
Baza (formulele elementare sunt formule). A LP .
Pas constructiv (obinere formule noi din formule vechi).
(i) Dac F LP atunci ( F) LP.
(ii) Dac F1, F2 LP atunci ( F1 F2 ) LP.
(iii) Dac F1, F2 LP atunci ( F1 F2 ) LP.
(iv) Dac F LP atunci (F) LP.
(v) Nimic altceva nu este formul.
Putem privi o formul F ca fiind reprezentat de un arbore binar
(arborele ataat lui F, notat Arb(F)), n modul urmtor (procedm
structural, conform definiiei lui LP):
-
56 Cristian Masalagiu
Definiia 2.2.
Baza. F = A A. Atunci arborele ataat lui F (sau, arborele care
reprezint F), este:
Pas constructiv.
(i) Fie F = ( F1) i s presupunem c se cunoate arborele ataat lui F1,
Arb(F1). Atunci, arborele ataat lui F va fi (ceva similar se obine
pentru (iv), adic pentru cazul F = (F1)):
(iii) Fie F = (F1 F2) i s presupunem c se cunosc att arborele ataat
lui F1 ct i arborele ataat lui F2 , adic Arb(F1) respectiv Arb(F2).
Atunci arborele ataat lui F va fi (pentru F = (F1 F2) se obine ceva
similar):
A
( )
))
Arb(F1)
-
Fundamentele logice ale Informaticii 57
Dei au un rol pur sintactic, neschimbnd cu nimic semantica
formulelor n care apar, parantezele rotunde au fost din anumite
motive tehnice privite mai sus ca un operator pre&post-fixat. Dac
introducem o ordine stnga-dreapta pe mulimea succesorilor imediai
ai fiecarui nod (implicit, pentru o formul este valabil ordinea de
scriere a literelor n cuvntul respectiv, exceptnd paranteza nchis
), care are acelai numr de ordine cu paranteza deschis (
corespunztoare), atunci se observ c fiecrei formule i corespunde
un arbore ataat unic i fiecrui arbore ordonat G (cu nodurile
etichetate cu elemente din L) i corespunde o unic formul din LP
(pentru care G este arborele ataat). Definim structural i mulimea
subformulelor oricrei formule date F (notat subf(F)). Admitem
implicit faptul c F subf(F) dac i numai dac F este subcuvnt al
lui F i F LP (cu alte cuvinte, F1 i F2, n cele ce urmeaz, sunt tot
formule).
( )
)
Arb(F1) Arb(F1)
-
58 Cristian Masalagiu
Definiia 2.3.
Baza. F = A A. Atunci subf(F) = {A}.
Pas constructiv.
(i) F = ( F1). Atunci subf(F) = subf(F1) U { ( F1) }.
(ii) F = (F1 F2). Atunci subf(F) = subf(F1) U subf(F2) U { (F1 F2) }.
(iii) Analog cu (ii) pentru cazul F = (F1 F2) (nlocuind peste tot,
simultan, cu ).
(iv) F = (F1). Atunci subf(F) = subf(F1) U { (F1) }
Observaie. Nu se admit alte posibiliti pentru scrierea unei formule,
dect cele fixate prin Definiia 2.1. Exist de altfel un algoritm care
rezolv problema de decizie: Dat orice cuvnt w L* (adic orice
secven finit de caractere din L) s se decid dac w LP. Conform
[JUC] de exemplu, notaia L* (algebric, L* este monoidul liber generat
de L) se explic prin aceea c mulimea cuvintelor (secvenelor finite
de simboluri) aparinnd unui alfabet cel mult numrabil formeaz un
monoid fa de operaia de concatenare (de juxtapunere a
literelor/cuvintelor). Elementul neutru, este cuvntul fr nici o liter
(cuvntul vid) i este notat cu e. Algoritmul menionat se termin
pentru fiecare intrare w L*, cu rspunsul (ieirea) DA dac w LP
i NU dac w LP. O problem de decizie are doar alternativa de
rspuns DA/NU i aici este un caz particular al problemei de
apartenen pentru un limbaj de tip 2. Revenind, A1 A2, nu este
formul pentru c nu are parantezele necesare (nu putem vorbi de
-
Fundamentele logice ale Informaticii 59
subf(A1 A2) pentru c A1 A2 nu este formul). Dar, la fel ca i n
cazul cunoscut al expresiilor aritmetice care conin variabile, constante
i operatorii (avnd i sensul de opus), +, i /, putem
accepta convenia de a prescurta scrierea unor expresii (formule,
cuvinte) prin eliminarea unor paranteze (sau chiar pe toate). Acest lucru
se poate face prin atribuirea de prioriti operatorilor, apoi bazndu-ne
pe faptul c aritatea lor (numrul de argumente) este cunoscut,
precum i pe unele proprieti cum ar fi comutativitatea, asociativitatea
sau distributivitatea. Prioritile standard sunt: 0 pentru , 1 pentru
, 2 pentru . Tot o convenie este i aceea de a folosi i alte nume
pentru formulele atomice, nafara celor admise deja prin faptul c sunt
simboluri desemnate a face parte din A. n general vom utiliza pentru
acestea litere mari de la nceputul alfabetului latin (A, B, C, ..., cu sau
fr indici). Invers, putem aduga n orice formul bine format
cupluri de paranteze corespondente (la fel cum le-am i eliminat),
pentru a mbunti receptarea corect a sintaxei i fr a schimba
semnificaia formulei n cauz. Acest lucru este permis de altfel prin
(iv), Definiia 2.1.
Exerciiul 2.4. Fie formula F = (( A) (B C)). Construii
arborele ataat (verificnd n acest mod i faptul c ntr-adevr
F LP). Eliminai parantezele i stabilii o prioritate a operatorilor
care intervin, astfel nct semnificaia intuitiv a noii secvene de
caractere s nu difere de semnificaia iniial (pentru a construi pe F,
se consider nti afirmaiile elementare A, B, C; se consider apoi
-
60 Cristian Masalagiu
negaia lui A, notat, s spunem, A i conjuncia lui B cu C, notat D;
n sfrit, se consider disjuncia lui A cu D).
Vom face i alte cteva prescurtri sintactice, justificate de altfel
i de anumite considerente semantice care vor fi prezentate ulterior:
(( F) G) se va nota cu (F G).
Pentru ((( F) G) (( G) F)) folosim (F G) sau
((F G) (G F)).
1
n
i Fi este o prescurtare pentru F1 F2 ... Fn.
1
n
i Fi este prescurtarea lui F1 F2 ... Fn .
Simbolurile i (numite dup cum tim implicaie, respectiv
echivalen) pot fi considerate ca i cum ar fi fost introduse de la bun
nceput n mulimea de conectori C (dac am fi procedat astfel de la
bun nceput, s-ar fi complicat att unele lucruri de natur sintactic cum
ar fi definiiile constructive, prioritile, etc., ct i definiia semanticii
LP, care urmeaz). Vom numi literal o variabil propoziional sau
negaia sa. A A se va numi i literal pozitiv iar orice element de
forma A,
A A va fi un literal negativ (vom nota A = {A1, A2, }). Dac
L este un literal, atunci complementarul su, L , va nota literalul A,
dac L = A A i respectiv literalul A dac L = A. Sperm ca
aceast notaie sintactic s nu fie confundat cu operaia semantic ,
-
Fundamentele logice ale Informaticii 61
prezent n definiia algebrelor booleene, rezultatele privind sintaxa
fiind, n general, separate de cele privind semantica. Se numete clauz
orice disjuncie (finit) de literali. Se numete clauz Horn o clauz
care are cel mult un literal pozitiv. O clauz pozitiv este o clauz care
conine doar literali pozitivi, iar o clauz negativ va conine doar
literali negativi. O clauz Horn pozitiv va conine exact un literal
pozitiv (dar, posibil, i literali negativi).
3. Semantica logicii propoziionale
Semantica (nelesul) unei formule propoziionale este, conform
principiilor logicii aristotelice, o valoare de adevr (a sau f), obinut n
mod determinist, care este independent de context, etc. Notnd de la
nceput pe a cu 1 i pe f cu 0, astfel nct s putem lucra cu algebra
boolean B = < B, , +, >, noiunea principal este cea de asignare
(interpretare, structur).
Definiia 2.4. Orice funcie S, S : A B se numete asignare.
Teorema 2.1 (de extensie). Pentru fiecare asignare S exist o unic
extensie a acesteia, S : LP B (numit tot structur sau
interpretare), care satisface:
(i) S(A) = S(A), pentru fiecare A A.
(ii) S(( F)) = (F)'S , pentru fiecare F LP.
(iii) S((F1 F2) ) = S(F1) S(F2), pentru fiecare F1, F2 LP.
-
62 Cristian Masalagiu
(iv) S((F1 F2) ) = S(F1) + S(F2), pentru fiecare F1, F2 LP.
Demonstraie. Fie S : A B. Definim funcia S : LP B, structural,
prin:
Baza. S(A) = S (A), pentru fiecare A A.
Pas constructiv.
(a) Dac F = ( F1), atunci S(F) = 1'(F )S .
(b) Dac F = (F1 F2), atunci S(F) = S(F1) S(F2).
(c) Dac F = (F1 F2), atunci S(F) = S(F1) + S(F2).
Este evident c S este o extensie a lui S, proprietatea (i) fiind
satisfcut imediat conform pasului Baza de mai sus. De asemenea,
definiiile (a) (c) din Pasul constructiv asigur satisfacerea punctelor
(ii) (iv) din enun, deoarece orice formul din LP, dac nu este
elementar, are una dintre cele trei forme considerate (cazul F = (F1)
este mult prea simplu pentru a fi tratat separat). Mai rmne s artm
c S este funcie total (adic, ataeaz fiecrui element din domeniu
un element i numai unul din codomeniu) i c ea este unica funcie
care satisface (i) (iv). Acest lucru se face prin inducie structural,
trebuind s artm c pentru fiecare F LP, este adevrat P(F), unde
P(F) este: Oricare ar fi asignarea S, valoarea S(F) exist (ca element
al lui B) i este unic, adic S este funcie, i oricare alt funcie S
care satisface (i) (iv), satisface S(F)= S(F).
Baza. Fie F = A A i orice asignare S. Cum S este funcie (total)
prin definiie i avem S(A) = S(A), tot prin definiie (S este extensia
-
Fundamentele logice ale Informaticii 63
lui S), este imediat faptul c S(A) exist i este unic n sensul precizat
(orice alt posibil S trebuie s fie tot o extensie a lui S).
Pas inductiv. Vom arta doar cazul F = ( F1), celelalte dou
(F = (F1 F2) i F = (F1 F2) ) fiind similare. Presupunem prin urmare
P(F1) ca fiind adevrat i demonstrm c P(F) este adevrat. Fie orice
asignare S. Faptul c S(F) exist (ca element al lui B) i este unic (n
sensul precizat), rezult din nou imediat, din ipoteza inductiv (S(F1)
exist i este unic), din definiia negaiei n B (tim c S(F) = 1(F )'S )
i a faptului c orice alt S trebuie s satisfac punctul (ii) din teorem.
De acum nainte nu vom face nici o diferen, nici mcar
notaional, ntre asignare i structur (intrerpretare). Se observ c
dat orice formul F LP i orice structur S, este suficient s
cunoatem valorile lui S n variabilele propoziionale care apar n F
(pentru fiecare F LP, vom nota cu prop(F) mulimea atomilor
pozitivi care apar n F, sau peste care este construit F). Vom numi
asignare (structur) complet pentru F, orice funcie parial S care
este definit exact (sau, mcar) pe prop(F) A i cu valori n B.
Aceasta, n cazul n care F este cunoscut, poate fi identificat cu o
funcie total pe A. Putem conchide chiar c n LP valoarea de adevr
a unei formule se deduce n mod unic din valoarea de adevr a
subformulelor (se mai spune c logica propoziional are proprietatea
-
64 Cristian Masalagiu
de extensionalitate). Vom mai pune S(F) S((F)) pentru fiecare
F LP.
Exerciiul 2.5. Definii structural prop(F), pentru fiecare F LP.
Fr alte precizri, vom lucra n continuare doar cu structuri
complete pentru mulimile de formule (o structur este complet pentru
o mulime de formule dac este complet pentru fiecare element din
acea mulime) care ne intereseaz la momentul dat.
Definiia 2.5. O formul F LP se numete satisfiabil dac exist
mcar o structur S (complet) pentru care formula este adevrat
(S(F) = 1). Se mai spune n acest caz c S este model pentru F
(simbolic, se mai scrie S F). O formul este valid (tautologie) dac
orice structur este model pentru ea. O formul este nesatisfiabil
(contradicie) dac este fals n orice structur (S(F) = 0, pentru fiecare
S, sau S F, pentru fiecare S).
Teorema 2.2. O formul F LP este valid dac i numai dac ( F)
este contradicie.
Demonstraie. F LP este valid dac i numai dac pentru fiecare
structur S avem S(F) = 1, adic (conform ii), Teorema 2.1) dac i
numai dac S(( F) ) = 1 = 0 (definiia negaiei), ceea ce nseamn c
( F) este o contradicie.
-
Fundamentele logice ale Informaticii 65
Clasa tuturor formulelor propoziionale LP, este astfel
partiionat n (mulimile indicate mai jos sunt ntr-adevr nevide i
disjuncte):
Tautologii
F
Formule satisfiabile dar nevalide
F ( F)
Contradicii
( F)
Tabelul 2.1
n tabelul anterior linia punctat poate fi considerat drept o
oglind n care se reflect adevrul.
Definiia 2.6. Dou formule F1, F2 LP se numesc tare echivalente
dac pentru fiecare structur S ele au aceeai valoare de adevr, adic
S(F1) = S(F2) (simbolic, vom scrie F1 F2). F1 i F2 se numesc slab
echivalente dac F1 satisfiabil implic F2 satisfiabil i reciproc (vom
scrie F1 s F2, ceea ce nseamn c dac exist S1 astfel nct
S1(F1) = 1, atunci exist S2 astfel nct S2 (F2) = 1 i reciproc). O
formul F LP este consecin semantic dintr-o mulime de formule
G LP, dac pentru fiecare structur corect S (aceasta nseamn aici
faptul c S este definit cel puin pentru toate variabilele propoziionale
care apar fie n F fie n elementele lui G), dac S satisface G (adic
-
66 Cristian Masalagiu
avem S(G) = 1 pentru fiecare G G) atunci S satisface F (simbolic,
vom scrie G F).
Observaie. Relaiile i s sunt relaii de echivalen (binare) pe LP,
n sens matematic (adic sunt reflexive, simetrice i tranzitive) i prin
urmare LP poate fi partiionat n clase de ehivalen corespunztoare,
obinndu-se mulimile ct LP/, respectiv LP/s. Mai mult, privind
, , ca nite operatori (de fapt, ar trebui s-i considerm mpreun
cu parantezele pe care le introduc, vezi i Exerciiul 2.4), atunci relaia
este compatibil (la stnga i la dreapta) cu acetia ([IP]), astfel
nct considernd 4-uplul LP = , se poate arta c acesta
formeaz o algebr boolean (homomorf cu B = < B, , +, >, dup
cum sugereaz Teorema de extensie).
Teorema 2.3. Fie G LP i G = { G1, G2, , Gn } LP. Urmtoarele
afirmaii sunt echivalente:
(i) G este consecin semantic din G.
(ii) ( 1
n
i Gi ) G este tautologie.
(iii) (1
n
i Gi ) G este contradicie.
Demonstraie.
-
Fundamentele logice ale Informaticii 67
(i) implic (ii). Presupunem prin reducere la absurd c
F = (1
n
i Gi) G nu este tautologie, dei G este consecin semantic
din G. Rezult c exist o structur S pentru care F este fals, adic S(
1
n
i Gi) = 1 i S(G) = 0. Prin urmare, pentru fiecare i [n] avem S(Gi)
= 1 i ca urmare S(G) = 0. n concluzie, exist o structur S astfel nct
S(G) = 1 i S(G) = 0. Acest lucru este absurd pentru c G este
consecin semantic din G.
(ii) implic (iii). Procedm din nou prin reducere la absurd, adic
presupunem c dei (1
n
i Gi) G este tautologie, (
1
n
i Gi) G nu
este contradicie. Aceast nseamn c F1 = (1
n
i Gi) G este
tautologie, dar F2 = (1
n
i Gi) G este satisfiabil. Prin urmare, exist
o structur S astfel nct S(F2) = 1 (i, desigur, S(F1) = 1). Din S(F2) = 1
rezult S((1
n
i Gi )) S( G) = 1, adic S((
1
n
i Gi )) = 1 i S(G) = 1.
n consecin, S( (1
n
i Gi )) = 0 i S(G) = 0. Pentru c
S(F1) = S((1
n
i Gi )) + S(G), avem S(F1) = 0, ceea ce este absurd
deoarece F1 este tautologie.
-
68 Cristian Masalagiu
(iii) implic (i). Presupunem prin reducere la absurd c
F = (1
n
i Gi) G este contradicie, dar G nu este consecin semantic
din G. Atunci exist o structur S care satisface toate formulele din G
dar nu satisface G. Prin urmare, avem S((1
n
i Gi)) = 1 i S(G) = 0, adic
S((1
n
i Gi)) = 1 i S(G) = 1. Cum S((
1
n
i Gi) G) =S((
1
n
i Gi))S(G),
rezult c exist S astfel nct S((1
n
i Gi) G) = 1, deci F nu este
contradicie (absurd).
n teorema anterioar am renunat la anumite paranteze,
respectnd prioritile/conveniile fcute. Vom face i pe viitor acest
lucru, fr a-l mai meniona explicit.
Teorema 2.4. Sunt adevrate urmtoarele echivalene (tari, pentru
oricare F, G, H LP):
(a) F F F (a) F F F (idempoten)
(b) F G G F (b) F G = G F (comutativitate)
(c) ( F G ) H
F ( G H )
(c) (F G) H F (G H)
(asociativitate)
(d) F ( G H )
(F G) (F H)
(d) F ( G H ) (F G) (F H)
(distributivitate)
-
Fundamentele logice ale Informaticii 69
(e) F ( F G ) F (e) F ( F G ) F (absorbie)
(f) F F (legea dublei negaii)
(g) ( F G )
F G
(g) ( F G ) F G (legile lui
deMorgan)
(h) F G F (h) F G G (legile validitii,
adevrate doar dac F este tautologie)
(i) F G F (i) F G G (legile contradiciei,
adevrate doar dac F este contradicie)
Demonstraie. Vom arta doar una dintre echivalene i anume (i). Fie
F LP orice contradicie i G LP. Fie orice structur S. Atunci
S(F G) = S(F)S(G) = 0, conform Tabelului 1.1 (punctul 9)) i
faptului c F este contradicie. Aceeai valoare o are i membrul drept
din (i).
Se poate arta, de exemplu, prin inducie matematic, faptul c
asociativitatea, distributivitatea i legile lui deMorgan se extind pentru
orice numr finit de formule.
Teorema 2.5 (de substituie). Fie H LP, oarecare. Fie orice
F, G LP astfel nct F este o subformul a lui H i G este tare
echivalent cu F. Fie H formula obinut din H prin nlocuirea (unei
apariii fixate a) lui F cu G. Atunci H H.
Demonstraie. Intuitiv, teorema spune c nlocuind ntr-o formul o
subformul cu o formul echivalent, obinem o formul echivalent cu
-
70 Cristian Masalagiu
cea iniial. Vom proceda prin inducie structural, avnd de artat
teorema din metalimbaj (H LP) P(H), unde
P(H): (F, G, H LP)(((F subf(H)) i
(H se obine din H nlocuind o apariie fixat a lui F cu G) i
(F G)) H H).
Baza. H = A A. S artm c P(A) este adevrat. Fie F, G,
H LP, astfel nct F subf(H), H se obine din H nlocuind
apariia aleas a lui F cu G, iar F G. Trebuie s artm c H H.
Dar, din F subf(H) i subf(H) = {A}, rezult c F = A ( care coincide
cu H). Prin urmare, H = G. Avem acum F = H, G = H i F G, de
unde urmeaz imediat c H H.
Pas inductiv. Trebuie tratate separat situaiile care urmeaz.
(i) H = ( H1). Presupunem c P(H1) este adevrat i demonstrm c
P(H) este adevrat. Fie F subf(H) = subf(H1) U {( H1)}. Dac
F = ( H1 ) ( = H), suntem ntr-o situaie similar cu cea din Baza,
deoarece raionamentul se face din nou asupra ntregii formule H. Fie o
apariie fixat a lui F subf(H1) subf(H) i considerm orice G LP
astfel nct G F. nlocuind pe F cu G n H, nseamn n acelai timp a
nlocui pe F cu G n H1. Notnd cu H respectiv H1 formulele obinute,
putem aplica ipoteza inductiv (P(H1) este adevrat) i obinem c
H1 H1. Revenind, tim c H = ( H1), H = ( H1) i H1 H1.
Rezult imediat c H H (vezi i Observaia care precede imediat
Teorema 2.3 i V.2.8 din Anex).
-
Fundamentele logice ale Informaticii 71
(ii) H = (H1 H2). Presupunem c P(H1) i P(H2) sunt adevrate i
demonstrm c P(H) este adevrat. Fie orice F subf((H1 H2)) =
subf(H1) U subf(H2) U{(H1 H2)}. Dac F = ( H1 H2 ) ( = H) suntem
din nou ntr-un caz similar cu cel din Baza. S considerm c
F subf(H1) (apariia deja fixat), cazul F subf(H2) tratndu-se
similar. Fie orice G LP astfel nct G F. A nlocui pe F cu G n H
nseamn, n acelai timp, a nlocui pe F cu G n H1 (H2 rmnnd
neschimbat). Vom nota cu H respectiv H1, formulele obinute dup
aceste nlocuiri. Aplicnd ipoteza inductiv (P(H1) este adevrat),
rezult imediat c H1 H1. Revenind, tim c H = (H1 H2),
H = (H1 H2) i H1 H1. Obinem imediat c H H (putem folosi
direct faptul deja amintit, c este compatibil cu operaiile, respectiv
cu conjuncia).
(iii) H = (H1 H2). Se demonstreaz analog cu cazul precedent.
Pentru a nu exista confuzii ntre limbajul de baz (LP) i
metalimbajul n care exprimm afirmaiile despre elementele lui LP, n
cele de mai sus (precum i n continuare) am notat implicaia cu iar
conjuncia prin i. Deocamdat am pstrat notaia clasic pentru
cuantificatorul universal (), deoarece el nu apare explicit n LP.
Rezultatele obinute ne permit practic s tratm formulele din
LP ntr-un mod similar cu funciile booleene, dac ne intereseaz
probleme de natur semantic. Astfel, vom nota cu 0 orice contradicie
i cu 1 orice tautologie i vom accepta principiul dualitii (rolul lui
-
72 Cristian Masalagiu
i + lundu-l respectiv , dup cum se poate deduce chiar din
Teorema 2.4). De asemenea, vom folosi tabelele de adevr pentru a
gsi n mod direct semantica (valoarea de adevr a) unei formule ntr-o
structur dat.
Nu apare astfel surprinztoare tematica paragrafului urmtor,
privind existena formelor normale.
4. Forme normale n LP
Spre deosebire de cazul funciilor booleene, vom studia pentru
nceput formele normale conjunctive i formele normale disjunctive
simultan.
Definiia 2.7. O formul F LP se afl n form normal
conjunctiv (FNC, pe scurt) dac este o conjuncie de disjuncii de
literali, adic o conjuncie de clauze. Simbolic:
inm
i,ji=1 j 1
F ( L )
(notm in
i i,jj=1
C L , i [m] ).
Similar, F LP este n form normal disjunctiv (FND, pe scurt),
dac este o disjuncie de conjuncii de literali.
n cele de mai sus Li,j A U A .
Exemplu. F = (A (B C)) este n FNC iar G = ((A B) (A C))
este n FND, dac A, B, C A.
-
Fundamentele logice ale Informaticii 73
Teorema 2.6. Pentru fiecare formul F LP exist cel puin dou
formule F1, F2 LP, F1 aflat n FNC i F2 aflat n FND, astfel nct
F F1 i F F2 (se mai spune c F1 i F2 sunt o FNC, respectiv o FND,
pentru F).
Demonstraie. Pentru a demonstra afirmaia necesar, (F)P(F) n
metalimbaj, unde
P(F): exist F1 LP, aflat n FNC i exist F2 LP, aflat n
FND, astfel nct F F1 i F F2,
procedm prin inducie structural.
Baza. F = A A. Aceast formul este att n FNC ct i n FND, deci
putem lua F1 = A i F2 = A.
Pas inductiv. Trebuie tratate cazurile corespunztoare definiiei
constructive a lui LP.
(i) F = ( G). Presupunem c P(G) este adevrat i demonstrm c
P(F) este adevrat. Din ipoteza inductiv rezult c exist formulele
G1, aflat n FNC i G2, aflat n FND, astfel nct G G1 i G G2.
Atunci, de exemplu, G G1 i, aplicnd legile lui deMorgan, gsim:
i in nm m
i,j i,ji=1 j 1 i=1 j 1
( ( L )) ( ( ( L )))
.
n ultima formul putem aplica unde este cazul legea dublei negaii
i apoi putem nlocui elementele de forma Li,j cu ji,L , obinnd astfel o
FND pentru F. Analog, dac pornim cu G2, care este o FND pentru G,
vom obine o FNC pentru F.
-
74 Cristian Masalagiu
(ii) F = (G H). Presupunem c afirmaiile P(G) i P(H) sunt
adevrate i artm c P(F) este adevrat. Din faptul c P(G) este
adevrat rezult c exist G1, aflat n FNC i satisfcnd G G1,
astfel nct:
G1 =
11 nm
i,ji=1 j 1
( ( L ))i
Cu totul similar, pentru c P(H) este adevrat, nseamn c exist H1,
aflat n FNC i satisfcnd H H1:
H1 =
22 nm
i,ji=1 j 1
( ( L ))i
Atunci, G H G1 H1 i este evident c ultima formul este tot o
conjuncie de disjuncii, adic este o FNC, notat F1, pentru F. Pentru a
obine o FND, F2, pentru F, pornim de la o FND, G2, pentru G i o
FND, H2, pentru H. Atunci F = G H G2 H2, de unde obinem
imediat o FND pentru F, notat F2, dac se aplic mai nti
distributivitatea generalizat a conjunciei fa de disjuncie i apoi, n
interiorul subformulelor, a disjunciei fa de conjuncie.
(iii) F = (G H). Procedm analog ca n cazul anterior.
Teorema precedent sugereaz existena unui algoritm recursiv
pentru obinerea simultan a unei FNC i a unei FND, pentru orice
formul propoziional. Putem folosi ns i tabelele de adevr i
modalitile de gsire a formelor normale conjunctive/disjunctive
(perfecte) descrise n Capitolul 1.
-
Fundamentele logice ale Informaticii 75
Exemplu. Gsii o formul F LP construit peste mulimea de
variabile propoziionale {A, B, C} i care s satisfac condiia: n
tabelul de adevr standard care o descrie, o schimbare i numai una
n secvena produce schimbarea valorii
corespunztoare de adevr S(F). Dac ncepem secvena S(F) cu 0,
atunci F este descris de tabelul:
A B C F
S(A) S(B) S(C) S(F)
0 0 0 0
0 0 1 1 *
0 1 0 1 *
0 1 1 0
1 0 0 0
1 0 1 1 *
1 1 0 1 *
1 1 1 0
Se poate construi apoi direct din tabel mcar o formul (sau dou) care
i corespunde semantic, formul ce se afl n FND (i/sau FNC). De
fapt vom folosi algoritmul de construcie a FNDP (FNCP) pentru o
funcie boolean. Conform Capitolului 1, acesta poate fi exprimat
astfel: se fixeaz liniile avnd 1 n ultima coloan (cele marcate cu *
n tabel); pentru fiecare asemenea linie se construiete o conjuncie de
literali (apar toi, cu bar sau fr): dac valoarea unei variabile
(atom pozitiv) este 0 n tabel, atunci variabila se trece n conjucia
-
76 Cristian Masalagiu
respectiv negat, iar dac valoarea ei este 1, atunci ea apare
nenegat; formula final, aflat n FND(P), este disjuncia tuturor
acestor conjuncii. Prin urmare, putem pune F = (A B C)
(A B C) (A B C) (A B C). Gsii, analog, o
FNC(P)
Conform teoremei anterioare, precum i datorit comutativitii
i idempotenei disjunciei, comutativitii i idempotenei conjunciei
(repetarea unui element, fie el literal sau clauz, este nefolositoare din
punctul de vedere al (ne)satisfiabilitii unei formule), este justificat
scrierea ca mulimi a formulelor aflate n FNC. Astfel, dac F este n
FNC (Definiia 2.7), vom mai scrie F = {C1, C2, ... , Cm} (nu uitm
totui c virgula aici provine dintr-o conjuncie), unde, pentru fiecare
i [m], vom pune }L,...,L,L{Cini,i,2i,1i
. Mai mult, dac avem
F LP reprezentat ca mulime (de clauze) sau ca mulime de mulimi
(de literali) i ne intereseaz doar studiul (ne)satisfiabilitii ei, putem
elimina clauzele C care conin att L ct i L , deoarece L L 1,
1 C 1 i deci aceste clauze sunt tautologii (notate generic cu 1).
Tautologiile componente nu au nici o semnificaie pentru stabilirea
valorii semantice a unei formule F aflate n FNC (1 C C).
-
Fundamentele logice ale Informaticii 77
5. Decidabilitate n LP
LP, cadrul formal propus (realitatea este modelat prin
afirmaii, afirmaiile sunt reprezentate ca formule propoziionale),
ofer ca principal metod de a rezolva problemele, testarea adevrului
(satisfiabilitii) unor formule. Din punctul de vedere al unui
informatician, trebuie ca pentru clasa de formule admis s existe un
algoritm care, avnd la intrare orice F LP, se termin cu rspunsul
DA, dac F este satisfiabil (sau valid, sau contradicie) i NU n
rest (tiind desigur c putem decide dac un anumit ir de caractere este
formul sau nu). n aceast situaie se spune c problema
satisfiabilitii (pe scurt, SAT) pentru LP este rezolvabil
(decidabil). Mai mult, am vrea s gsim asemenea algoritmi pentru
care complexitatea timp este rezonabil.
Teorema 2.7 (decidabilitatea SAT). Satisfiabilitatea (validitatea,
nesatisfiabilitatea) formulelor calculului propoziional este decidabil n
timp exponenial.
Demonstraie. Practic, demonstraia (exceptnd complexitatea) a fost
deja fcut, chiar n mai multe moduri. Fie F LP avnd prop(F) =
{A1, A2 , , An} = An . Se formeaz, de exemplu n Pasul 1 al unui
posibil algoritm (notat tot SAT) pentru testarea satisfiabilitii
(validitii, nesatisfiabilitii), tabela de adevr corespunztoare lui F
(Teorema de extensie, Teorema de substituie i legtura dintre
algebrele booleene LP i B stau la baza corectitudinii acestei
construcii) care are forma:
-
78 Cristian Masalagiu
S(A1) S(A2) S(An) S(F)
0 0 0 v1
2n = m
0 0 1 v2
1 1 1 vm
Dac toi vi (i [m]) sunt egali cu 0 atunci F este contradicie, dac toi
vi sunt 1 atunci F este tautologie, iar n rest F este satisfiabil dar
nevalid. Pentru a depista acest lucru, trebuie parcurs, n Pasul 2, n
cazul cel mai defavorabil, ntregul tabel, linie cu linie i prin urmare
trebuie efectuate 2n comparaii (F este construit peste n formule
atomice). Dei mai sus nu avem o explicaie formal riguroas a
faptului c SAT are timp exponenial, se poate arta c problema este
chiar NP-complet (conform [AHO]; a se urmri i comentariile care
urmeaz imediat dup demonstraie).
Datorit Teoremei de extensie i Teoremei de substituie,
putem construi o tabel de adevr pentru o formul pornind nu de la
variabile, ci chiar de la anumite subformule mai complicate (pentru care
valorile posibile, finale, sunt tot 0 sau 1). Mai mult (se pot consulta
[KNU], [JUC], [LUC] i, n special, [CRO], [AHO], [COR], [BR]),
trebuie cutai algoritmi rapizi (eficieni, tratabili), adic avnd
complexitate (timp) mic. Astfel, dou dintre msurile (teoretice,
globale) de complexitate des ntrebuinate sunt complexitatea timp i
-
Fundamentele logice ale Informaticii 79
complexitatea spaiu. Ideea este aceea c un (orice) pas elementar
(instruciune) al unui algoritm se execut ntr-o unitate de timp (pentru
spaiu, fiecare dat elementar se memoreaz ntr-un registru sau
locaie de memorie, acesta/aceasta ocupnd o unitate de spaiu),
criteriul numindu-se al costurilor uniforme. Exist i criteriul costurilor
logaritmice (pe care ns nu-l vom utiliza aici), n care orice informaie
de lungime i, se prelucreaz (respectiv, se memoreaz) n numrul de
uniti de timp (uniti de spaiu) egal cu log(i) + 1 (dac i = 0, se
convine s lum log(i) = 0; n noteaz partea ntreag inferioar a
numrului n). Intuitiv, timpul luat de execuia unui algoritm Alg este dat
de numrul de instruciuni (pai/operaii elementare) efectuate (s-l
notm cu tAlg), iar spaiul (notat cu sAlg) este dat de numrul de locaii
(elementare) de memorie (intern, a calculatorului) ocupate n cursul
execuiei. Sigur c totul se raporteaz la lungimea fiecarei intrri
(adic, n cazul nostru, la lungimea unei formule F IN LP, aceasta
putnd fi de exemplu nF = card (prop(F))) i ne intereseaz de fapt
sup{tAlg
(F) | F IN i nF = n N}, margine superioar pe care o vom
nota cu tAlg
(n). Aceast abordare (n care se caut cazul cel mai
nefavorabil, dac este desigur posibil), ne permite s fim siguri c
pentru fiecare intrare de lungime n, timpul de execuie al lui Alg nu va
depi tAlg(n). Cum determinarea acelui supremum este de multe ori
destul de dificil, ne vom mulumi s studiem aa-numita comportare
asimptotic (sau ordinul de cretere) a (al) lui tAlg(n), adic ne vor
interesa doar anumite margini ale sale, cum ar fi marginea sa
superioar. Formal, pentru fiecare f : N N, notm
-
80 Cristian Masalagiu
O(f) = {g | g : N N, exist c R, c 0 i exist k N, astfel nct
pentru fiecare n k avem g(n) cf(n)} i vom spune c fiecare
g O(f), este de ordinul lui f, ceea ce se mai noteaz i cu g = O(f).
Astfel, vom spune c SAT are complexitatea (timp, asimptotic) O(2n),
sau, pe scurt, complexitate exponenial, deoarece c exist (mcar) un
algoritm Alg care rezolv problema (cel sugerat n demonstraia
Teoremei 2.7) i pentru care tAlg(n) = O(2n). Similar, vom vorbi de
algoritmi polinomiali (tAlg
(n) = O(p(n)), unde p(n) desemneaz un
polinom n n, de orice grad), sau de algoritmi liniari (p(n) de mai sus
este un polinom de gradul I), adic de probleme avnd complexitatea
(timp, dar se poate defini ceva asemntor pentru spaiu) de tipul
precedent. Sperana de a gsi algoritmi mai performani pentru
rezolvarea SAT, se poate baza pe ideea de a restrnge LP la anumite
subclase stricte, particulare de formule ale sale, suficient de largi ns
pentru a exprima convenabil pri importante ale realitii. n plus, n
condiiile utilizrii calculatorului, gsirea unor algoritmi de natur
sintactic pentru rezolvarea SAT (n locul celor semantici, cum este
i cel bazat pe folosirea tabelelor de adevr) este o prioritate (chiar dac
acetia nu sunt mai buni din punctul de vedere al teoriei generale a
complexitii).
6. Formule Horn
Reamintim c o clauz Horn este o disjuncie de literali care
conine cel mult un literal pozitiv.
-
Fundamentele logice ale Informaticii 81
Definiia 2.8. O formul Horn este o formul aflat n FNC, clauzele
componente fiind (toate) clauze Horn.
Uneori, vom numi tot formul Horn i o formul care este (tare)
echivalent cu o formul de forma considerat n Definiia 2.8. Se
poate arta ([MAS1]) c exist formule propoziionale care nu sunt tare
echivalente cu nici o formul Horn, apariia a mcar doi literali pozitivi
distinci ntr-o clauz fiind decisiv. Formele posibile pentru o formul
Horn sunt (variabilele propoziionale care apar sunt elemente ale lui A):
(i) C = A1 A2 Ak, k 1, k N i
(ii) C = A1 A2 Ak B, k N.
Observaie. nafar de reprezentarea ca mulimi, clauzele Horn pot fi
reprezentate sub i sub aa-numita form implicaional. Vom distinge
cazurile (reamintim c 0 i 1 denot orice contradicie respectiv orice
tautologie):
C = A A (nici un literal negativ, un literal pozitiv). Acest
lucru se mai poate scrie sub forma C 1 A, ceea ce se
justific prin aceea c 1 A 1 A 0 A A.
C = A1 A2 Ak (nici un literal pozitiv, mcar un
literal negativ). Vom scrie C A1 A2 A3 Ak 0
(folosim din nou definiia implicaiei i faptul c 0 A A).
C = A1 A2 Ak B (exact un literal pozitiv,
mcar un literal negativ). Atunci CA1 A2 A3 AkB,
direct din definiia implicaiei.
-
82 Cristian Masalagiu
C (nici un literal negativ, nici un literal pozitiv). Din motive
tehnice vom folosi i aceast clauz vid (n reprezentarea
clauzelor cu mulimi vom folosi pentru chiar ). Prin
convenie, este o clauz de orice tip (inclusiv o clauz Horn),
dar nesatisfiabil.
Teorema 2.8. Satisfiabilitatea formulelor Horn este decidabil n timp
liniar.
Demonstraie. S considerm algoritmul:
Algoritm Horn
Intrare: Orice formul Horn, F, reprezentat ca mulime de clauze,
clauzele componente fiind clauze Horn diferite de clauza vid i scrise
sub form implicaional .
Ieire: DA, n cazul n care formula F este satisfiabil (furnizndu-se
i o asignare S care este model pentru F) i NU n caz contrar (F nu
este satisfiabil).
-
Fundamentele logice ale Informaticii 83
Metod (de marcare):
Pasul 1. i := 0.
Pasul 2.
Ct_timp ((exist n F o clauz C de forma
A1 A2 A3 Ak B, cu A1, A2, A3, ... , Ak marcai i
B nemarcat sau de forma A1 A2 A3 Ak 0, cu A1,
A2, A3, ... , Ak marcai) i (i = 0))
execut
Pasul 3. Alege un asemenea C ca mai sus.
Pasul 4. Dac ( C = A1 A2 A3 Ak B )
atunci
Pasul 5. Marcheaz B peste tot n F.
altfel
Pasul 6. i := 1.
Sf_Dac
Sf_Ct_timp
Pasul 7. Dac ( i = 0 )
atunci
Pasul 8. Scrie DA.
Pasul 9. Scrie S, cu S(A) = 1 dac i numai
dac A apare n F i este marcat.
altfel
Pasul 10. Scrie NU.
Sf_Dac.
-
84 Cristian Masalagiu
Artm mai nti c algoritmul se termin pentru fiecare intrare. S
precizm c aciunea de marcare o privim n sens grafic normal,
marcajul care poate fi ataat unei variabile proziionale alegndu-se
fr criterii speciale (s presupunem c el este *, mpreun eventual cu
anumii indici prin care s se identifice n care dintre execuiile
corpului buclei s-a fcut marcarea). Iniial, toate variabilele se
presupun a fi nemarcate. Dac F conine clauze de forma 1 B (care
se consider a fi de fapt de forma A1 A2 A3 Ak B, cu A1,
A2, A3, ... , Ak marcai i B nemarcat), se procedeaz conform
algoritmului, adic se marcheaz toate apariiile lui B n F i se trece la
pasul urmtor. Mai departe, la fiecare execuie a corpului buclei (Paii
3. i 4.), fie se marcheaz o variabil propoziional nou (nemarcat
nc), fie se iese din execuia buclei. Pentru c numrul de variabile
peste care este construit formula F este finit, terminarea algoritmului
este evident. Dac nu exist deloc clauze de tipul 1 B, algoritmul se
termin fr nici o execuie a corpului buclei, cu rspunsul DA
(formula este satisfiabil) i cu asignarea S, n care S(A) = 0 pentru
fiecare A (care apare n F).
Artm n continuare c algoritmul este corect. Aceasta nseamn c
ieirea algoritmului satisface ceea ce am dorit, adic rspunsul DA/S
corespunde faptului c formula F furnizat la intrare este satisfiabil (i
S F) iar rspunsul NU corespunde faptului c F este nesatisfiabil.
Vom separa cazurile:
Cazul a). La terminarea execuiei se obine DA i F nu conine
clauze C de tipul 1 B. Dup cum am observat, acest lucru nseamn
-
Fundamentele logice ale Informaticii 85
c bucla s-a terminat fr s i se execute vreodat corpul avnd n plus
i = 0 i S(A) = 0 pentru fiecare A (care apare n F). Atunci exist n F
(la finalul execuiei) doar clauze de tipul C1=A1 A2 A3 AkB,
sau C2 = A1 A2 A3 Ak 0 (k 1) , care n-au nici o
variabil marcat. Avem atunci, pe scurt, S(C1) = S(00 ... 0 0)= 1,
respectiv S(C2) = 1, de unde gsim S(F) = 1.
Cazul b). La terminare se obine DA iar F conine i clauze
C = 1 B. Atunci bucla se termin dup un anumit numr de execuii
ale corpului su, valoarea lui i este 0 i F conine n final clauze C
avnd marcate anumite variabile. Dac C = 1 B (adic
C = B), unde B este marcat (S(B) = 1), avem imediat S(C) = 1. Dac
C = A1 A2 A3 Ak B (k 1) este posibil ca, fie toate
variabilele din antecedent sunt marcate (dar atunci B este i el marcat i
atunci, din nou, S(C) = 1 pentru c semantica lui C este de tipul 1 1),
fie exist mcar una dintre variabilele Ai de mai sus care este
nemarcat, dar atunci vom avea iari S(C) = 1, pentru c semantica sa
este de tipul 0 1 sau 0 0. n sfrit, dac
C = A1 A2 A3 Ak 0 (k 1), unde mcar un Ai este
nemarcat, semantica lui C este de forma 0 0 i obinem din nou
S(C) = 1). Concluzia este c S(C) = 1 pentru fiecare C care apare n F,
adic S(F) = 1.
Cazul c). Algoritmul se termin cu i = 1 i rspunsul NU. Acest lucru
nseamn c exist n F o clauz C = A1 A2 A3 Ak 0 cu
toi Ai, i [k] marcai (obligatoriu, n F exist i clauze de forma
-
86 Cristian Masalagiu
1 B, B marcat), de unde rezult c semantica lui C n asignarea
furnizat de algoritm este de forma 1 0 i prin urmare S(C) = 0, de
unde S(F) = 0. Acest lucru nu nseamn ns c F este nesatisfiabil.
Pentru a trage aceast concluzie trebuie s artm c pentru nici o alt
asignare, ea nu poate fi model pentru F. S presupunem (RA) c exist
o asignare S (diferit de S, furnizat de algoritm) astfel nct
S(F) = 1. S observm, pentru nceput, c toate variabilele care au fost
marcate n algoritm (deci cele care au primit valoarea de adevr 1 n S),
trebuie s primeasc valoarea 1 n oricare S cu S(F) = 1. Altfel spus,
asignarea S conine cel mai mic numr posibil de valori 1 (atribuite
evident variabilelor marcate) astfel nct formula s aib anse s fie
satisfiabil. ntr-adevr, pentru fiecare S cu S(F) = 1, trebuie s avem
S(C) = 1 pentru fiecare clauz C din F. S ne ocupm puin de
momentul n care se marcheaz o variabil B, ordonnd clauzele din F
de forma C = A1 A2 A3 Ak B (k 1) dup numrul de
variabile din antecedent (chiar n algoritm, selecia unei clauze pentru
marcare se poate face dup un asemenea criteriu):
Clauze C de tipul 1 B B (nici o variabil n antecedent, B
nemarcat). De la acestea ncepe procesul de marcare. Din faptul
c S(C) trebuie s fie egal cu 1, este clar c trebuie pus
S(B) = 1 (B se i marcheaz, deci S(B) = 1).
Clauze C de forma A B A B (o variabil n
antecedent; A este marcat, B nemarcat). A nu putea fi marcat
dect dac a aprut deja ca un consecvent ntr-o clauz de
-
Fundamentele logice ale Informaticii 87
tipul anterior, sau n una de acelai tip cu aceasta i care are
antecedentul marcat. Prin urmare, n orice S cu S(C) = 1,
trebuie oricum s avem S(A) = 1, deci S( A) = 0 i atunci
S(B) = 1 (concecina este c B se marcheaz, deci i S(B) = 1).
Continum raionamentul cu C = A1 A2 B (dou variabile
n antecedent; ambele variabile marcate; B este, nc,
nemarcat), ajungnd din nou la concluzia c pentru fiecare S,
pentru a avea S(C) = 1, trebuie s avem S(B) = 1, precum i
S(B) = 1.
Revenind, am artat ntr-adevr c pentru fiecare S astfel nct
S(F) = 1, trebuie s avem S(A) = 1 pentru fiecare A marcat de ctre
algoritm, adic pentru fiecare A care satisface i S(A) = 1 (procesul
descris mai sus se continu pentru oricte variabile prezente n
antecedent, iar numrul acestora este finit). Prin urmare, avem i
S(C) = 0, de unde rezult c S(F) = 0, ceea ce este absurd.
S artm n final c algoritmul Horn are timp de execuie liniar.
Faptul c t(n) O(f(n)), unde f(n) = an + b (a, b N*), rezult
imediat din faptul c la fiecare execuie a corpului buclei se marcheaz
o nou variabil. Desigur c pentru a obine n mod real acest lucru
algoritmul trebuie detaliat, n sensul c, de exemplu, n Paii de tip 3
(de alegere a unei clauze corespunztoare C), selecia variabilei de
marcat trebuie fcut prin parcurgerea de un numr fix de ori
(independent de numrul de execuii) a listei variabilelor peste care este
construit F.
-
88 Cristian Masalagiu
Exemplu. S aplicm algoritmul de marcare urmtoarei formule Horn:
F = ( A D ) ( C A D ) ( A B ) D E.
Scriem nti F ca o mulime de implicaii, obinnd
F = {D A, C A D, A B 0, 1 D, E 0}. nainte de
prima execuie a corpului buclei, avem i = 0 i toate variabilele sunt
nemarcate.
Prima execuie. Alegem clauza 1D (de fapt, nu exist alt
posibilitate). Toate apariiile lui D se marcheaz cu *1:
1*D A, C A 1*D , A B 0, 1 1*D , E 0.
A doua execuie. Alegem D A (din nou, nu exist dect o
unic posibilitate) i A se marcheaz peste tot, cu *2:
1*D 2*A , C 2*A 1*D , 2*A B 0, 1 1*D , E 0.
A treia execuie nu mai are loc, deoarece nu mai exist clauze
de tipul cerut. Cum valoarea lui i nu s-a modificat (a rmas 0),
rspunsul algoritmului este DA.
Prin urmare, F este satisfiabil i o structur S, model pentru F, este
definit prin S(A) = 1, S(B) = 0, S(C) = 0, S(D) = 1, S(E) = 0.
Am gsit prin urmare o subclas convenabil (acest lucru este
cumva subiectiv) de formule propoziionale, si anume clasa formulelor
Horn, pentru care testarea satisfiabilitii se poate face ntr-un timp
rezonabil. Dei rezultatele teoretice generale ne spun c nu pot exista
metode sintactice mai bune dact metoda semantic sugerat de
Algoritmul SAT (dac ne referim la ntrega mulime LP), existena,
-
Fundamentele logice ale Informaticii 89
dovedit de acum, a unor algoritmi care s nu fac apel explicit la
semantic, pare deja a fi un ctig.
7. Rezoluie n LP
Fr a restrnge generalitatea, putem presupune c lucrm cu
formule din LP aflate n FNC, reprezentate sub form de mulimi
(finite) de clauze, iar clauzele ca mulimi (finite) de literali.
Definiia 2.9 (rezolvent). Fie clauzele C1, C2 , R. Spunem c R este
rezolventul lui C1, C2 (sau c C1, C2 se rezolv n R, sau c R se
obine prin rezoluie ntr-un pas din C1, C2), pe scurt,
R = ResL(C1, C2), dac i numai dac exist un literal L C1 astfel
nct L C2 i R = (C1 \ {L}) U (C2 \ { L }).
Vom putea reprezenta acest lucru i grafic, prin arborele de rezoluie:
Vom renuna la scrierea explicit a lui L sau/i L n momentul n care
nu exist cofuzii.
Observaie. Rezolventul a dou clauze este tot o clauz. Mai mult,
rezolventul a dou clauze Horn este tot o clauz Horn. Clauza vid ()
C1 C2
R
L
L
-
90 Cristian Masalagiu
poate fi obinut prin rezoluie din dou clauze de forma C1 = {A} i
C2 = {A}. n definiia anterioar putem considera c C1 i C2 sunt
diferite ntre ele. Dac ele ar coincide, atunci C1 = C2 =... LL 1,
adic acele clauze sunt tautologii, detectabile sintactic (n acest caz nu
ne mai intereseaz alte metode formale de studiere a satisfiabilitii lor).
Exemplu.
Fie formula F = {{A, E, B}, { A, B, C}, {A, D}, { A, D, E}}. S
gsim civa dintre rezolvenii care se pot obine (succesiv) pornind de
cele cele patru clauze care compun F, notate respectiv C1, C2, C3, C4:
Acetia au fost gsii apelnd de fiecare dat la C1. i C2 poate fi sursa
unui ntreg lan de asemenea rezolveni:
C1 C2 C1 C2 C1 C4
A A B B A A
{A, B, A,D}
E E
{E, B, B, C} {A, E, A, C} {E,B,D,E}
C1 C4
-
Fundamentele logice ale Informaticii 91
Muli dintre aceti rezolveni primari nu sunt interesani, fiind
tautologii (datorit faptului c acele clauze alese spre rezolvare conin
mai mult de un literal de tipul L/ L ). Procesul poate ns continua cu
gsirea de noi rezolveni folosindu-i i pe cei obinui din clauzele
iniiale (cum este cazul i mai sus) .a.m.d.
n acest moment putem s ne punem cel puin dou ntrebri:
Exist cazuri n care procesul anterior (de aflare succesiv de
rezolveni noi) nu se termin?
n caz de rspuns negativ i presupunnd c exist o legtur
ntre acest proces sintactic (de obinere de rezolveni) i
satisfiabilitate, se pot obine algoritmi (sintactici, eventual
performani) de testare a satisfiabilitii unor formule?
Rspunsul l vom da n cele ce urmeaz.
C2 C3
A A
{B, C, D} C1
B B
{C, D, A, E}
-
92 Cristian Masalagiu
Teorema 2.9 (lema rezoluiei). Fie oricare formul F LP (aflat n
FNC i reprezentat ca mulime de clauze) i R un rezolvent pentru C1,
C2 F. Atunci F este tare echivalent cu F U{R}.
Demonstraie.
. Dac S satisface F U{R} atunci desigur c S satisface F, conform
definiiei (o structur satisface o mulime de formule dac satisface
fiecare element din mulime).
. S presupunem c S F , adic S C, pentru fiecare C F. Fie
C1,C2 F i R un rezolvent al lor, R = (C1 \ {L}) U (C2 \ { L }), unde
L C1, L C2 .
Cazul 1. S(L) = 1. Atunci S L. Dar tim c S C2 . Rezult c
S C2 \ { L }, de unde S(R) = 1.
Cazul 2. S(L) = 0. Analog, artndu-se c S C1 \ {L}.
n teorema anterioar am fi putut considera, n loc de F, o mulime
oarecare de clauze, chiar infinit.
Definiia 2.10. Fie F o mulime oarecare de clauze din LP i C o
clauz. Spunem c lista C1, C2 , , Cm este o demonstraie prin
rezoluie (n mai muli pai) a lui C pornind cu F dac sunt
satisfcute condiiile:
(i) Pentru fiecare i [m], fie Ci F, fie Ci este obinut prin rezoluie
ntr-un pas din Cj, Ck, cu j, k < i.
(ii) C = Cm.
-
Fundamentele logice ale Informaticii 93
n condiiile definiiei, se mai spune c C este demonstrabil
prin rezoluie (pornind cu F, sau, n ipotezele date de F). Mai mult,
pentru a spune acest lucru, este suficient ca F s fie inserat (prezent)
ntr-o demonstraie i nu s fie neaprat ultimul element al acesteia.
Intuitiv, o demonstraie prin rezoluie n mai muli pai nseamn o
succesiune finit de rezoluii ntr-un pas, care poate fi reprezentat i
grafic, printr-un arbore (a se vedea exemplul care urmeaz), sau chiar
ca un graf oarecare (dac nu folosim noduri diferite pentru apariiile
distincte ale unei aceleiai clauze). n particular, dac C este clauza
vid, atunci demonstraia respectiv se numete i respingere.
Numrul de pai dintr-o demonstraie este dat de numrul de clauze
obinute prin rezoluie ntr-un pas (din clauze anterioare). Acesta poate
fi considerat ca fiind o msur a mrimii (lungimii) demonstraiei. O
alt msur pentru o demonstraie reprezentat ca text poate fi chiar
lungimea listei (numrul total de clauze, sau chiar numrul total de
clauze distincte). Dac reprezentm o demonstraie ca un arbore, putem
folosi i msuri specifice, cum ar fi adncimea arborelui, numrul de
nivele ([IVA]), etc. Convenim s eliminm din orice demonstraie
rezolvenii care conin att L ct i L, aceste clauze fiind tautologii i
deci neinteresante din punctul de vedere al studiului satisfiabilitii
unei formule aflate n FNC.
Exemplu. Fie F = {{A, B, C}, {A}, {A, B, C}, {A, B}}. O
respingere poate fi descris prin arborele:
{A, B, C} {A, B, C}
C C
{A, B} {A, B}
B B
{A} {A}
A A
-
94 Cristian Masalagiu
Definiia 2.11 (mulimea rezolvenilor unei mulimi de clauze). Fie F
o mulime de clauze din LP (nu neaprat finit). Notm succesiv:
Res(F) = F U{R | exist C1, C2 F astfel nct R = Res(C1, C2)}.
Res(n+1)(F) = Res(Res(n)(F)), n N. Prin Res(0)(F) vom nelege F i
atunci vom putea pune i Res(1)(F) = Res(F).
Res*(F) = (n)ResnN
(F).
Res(n)
(F) se va numi mulimea rezolvenilor lui F obinui n cel mult
n pai, iar Res*(F) mulimea (tuturor) rezolvenilor lui F.
Observaie. Direct din definiie rezult c:
F = Res(0)
(F) Res(1)(F) ... Res(n)(F) ... Res*(F).
-
Fundamentele logice ale Informaticii 95
Putem da atunci i o definiie structural a lui Res*(F). Vom nota astfel
cu Resc mulimea definit prin:
Baza. F Resc.
Pas constructiv: Dac C1, C2 Resc i C = Res(C1, C2), atunci
C Resc.
Rmne s artm c cele dou definiii introduc aceeai mulime.
Teorema 2.10. Pentru fiecare F LP, avem Res*(F) = Resc.
Demonstraie. Artm egalitatea prin dubl incluziune.
. Demonstrm prin inducie matematic adevrul afirmaiei din
metalimbaj (n)P(n), unde P(n): Res(n)(F) Resc.
Baza. n = 0. Trebuie artat c F = Res(0)(F) Resc, ceea ce este
imediat din definiia lui Resc.
Pas inductiv. Presupunem c Res(n)(F) Resc i artm c
Res(n+1)
(F) Resc, ceea ce este din nou imediat din definiia lui Resc i
Definiia 2.11. n sfrit, avem Res*(F) Resc, direct din Definiia
2.11 i observaia care urmeaz acesteia.
. Procedm prin inducie structural, mai exact artm c afirmaia
din metalimbaj (C Resc)(C Res*(F)) este adevrat.
Baza. C F. Adevrat, deoarece F = Res(0)(F) Res*(F).
-
96 Cristian Masalagiu
Pas inductiv. Fie C = Res(C1, C2), C1, C2 Resc i resupunem c C1,
C2 Res*(F). S artm c C Res*(F). Acest fapt urmeaz imediat,
conform Definiiei 2.11.
De acum nainte vom folosi ambele notaii pentru mulimea
rezolvenilor unei mulimi de clauze. i n Teorema 10 se putea
considera c F reprezint o mulime oarecare de clauze.
Teorema 2.11. Fie F o mulime de clauze din LP (nu neaprat finit).
O clauz C LP se poate demonstra prin rezoluie pornind cu clauzele
lui F dac i numai dac exist k N, asfel nct C Res(k)(F).
Demonstraie. Fie F i C fixate ca n enun.
. S presupunem c exist o demonstraie prin rezoluie a lui C
pornind cu F, C1, C2, ... , Cm = C. Este ndeplinit condiia (i) din
Definiia 2.10 i atunci nseamn c pentru fiecare i [m], avem
Ci Resc, care coincide cu Res*(F), conform Teoremei 2.10. Prin
urmare, conform definiiei lui Res*(F) exist k N, asfel nct
C Res(k)(F).
. S presupunem c exist k N, asfel nct C Res(k)(F) (pe k l
considerm a fi cel mai mic numr natural care satisface condiia).
Conform Definiiei 2.11, avem Res(j)(F) = Res(Res(j-1)(F)) =
Res(j-1)
(F) U {R | exist C1, C2 Res(j-1)
(F) astfel nct
R = Res(C1, C2)}, pentru fiecare j [k]. Putem conveni chiar ca n a
-
Fundamentele logice ale Informaticii 97
doua mulime din reuniunea de mai sus s nu punem dect rezolvenii
noi, care nu apar n Res(j-1)
(F). Atunci C apare efectiv n Res(k)
(F) dar
nu i n Res(k-1)(F). Dac k = 0, am terminat (C F i lista format doar
din C constituie o demonstraie prin rezoluie a lui C). n caz contrar,
mai nti construim algoritmic un graf neorientat n felul urmtor: la
Pasul 1 punem ca noduri elementele din Res(k)(F), care nu sunt i n
Res(k-1)
(F); la Pasul 2 punem nodurile din Res(k-1)
(F) care nu sunt n
Res(k-2)(F), precum i muchiile corespunztoare care unesc nodurile
puse deja n graf, conform rezoluiilor ntr-un pas din care ele provin,
. a. m. d. n cel mult k + 1 pai, vom plasa n graf i elementele
(folosite) ale lui F, precum i toate muchiile corespunztoare
rezoluiilor ntr-un pas cu ajutorul crora se construiete Res(k)(F).
Considerm acum subgraful generat de nodul C i toate nodurile aflate
pe lanuri de la C la frunze ([IVA]). Acesta este un arbore cu rdcina
C, care reprezint o demonstraie a lui C pornind cu o submulime a lui
F, deci i cu F (desigur c demonstraia se obine prin listarea
corespunztoare a nodurilor, ultimul element din list fiind C). Dac
subgraful considerat nu este arbore, acest lucru se datoreaz faptului c
mcar o clauz C este utilizat n mai muli pai de rezoluie. Graful
poate fi uor transformat n arbore prin multiplicarea nodurilor de tipul
C i a arcelor aferente.
Dup cum probabil s-a putut observa, n cele de mai sus am
folosit n majoritatea cazurilor termenul mulimea de clauze F i nu
formula F (aflat n FNC). Dei pe noi ne intereseaz doar formulele
(care pot fi privite ca mulimi finite de clauze n cazul n care ne
-
98 Cristian Masalagiu
intereseaz doar satisfiabilitatea lor), aproape toate rezultatele sunt
valabile i pentru mulimi infinite (numrabile) de formule (clauze).
Teorema urmtoare stabilete o legtur important, privind
satisfiabilitatea, ntre mulimile infinite i cele finite de formule
oarecare din LP.
Teorema 2.12 (de compactitate pentru LP). Fie M o mulime infinit
(numrabil) de formule din LP. M este satisfiabil dac i numai dac
fiecare submulime finit a sa este satisfiabil.
Demonstraie.
. Dac exist structura S astfel nct S M, adic S(F) = 1 pentru
fiecare F M, atunci evident c acelai lucru se ntmpl pentru fiecare
submulime (finit) M M.
. Pentru fiecare n N, vom nota Mn {F M | subf(F)
A = prop(F) An}, adic mulimea formulelor din M care sunt
construite peste (cel mult) mulimea de variabile propoziionale
An = {A1, A2, , An}. Cum mulimea funciilor booleene de n
variabile (FB(n)
) are cardinalul 22n
, n Mn exist cel mult 22
n formule cu
tabele de adevr distincte. Mai mult, direct din definiii avem
M1 M2 Mn ... M i M =1
nn
M
. Revenind, s
presupunem c fiecare submulime finit a lui M este satisfiabil i s
artm c M este satisfiabil. Fie K M orice submulime finit
-
Fundamentele logice ale Informaticii 99
(satisfiabil) a lui M. Atunci exist n, natural, astfel nct K Mn . Fie
Mn = {F1, F2, , nk
F }, kn n22 , mulimea elementelor lui Mn care
au tabele de adevr distincte. Pentru fiecare formul G din K alegem o
formul i numai una, Fi, din Mn, astfel nct G Fi. Fie "
nM mulimea
tuturor acestor formule, pentru care este satisfcut condiia: K este
satisfiabil dac i numai dac Mn este satisfiabil. Fie atunci Sn un
model pentru "nM . Avem i Sn Mn pentru c pentru fiecare
F Mn \ "
nM , exist G "
nM astfel nct Sn(G) = Sn(F). Din ipoteza
noastr (fiecare submulime finit a lui M este satisfiabil) rezult
aadar c exist un ir de structuri care satisfac:
S1 M1, S2 M2, , Sn Mn ,
Renumerotnd dac este cazul variabilele iniiale, putem presupune c
fiecare dintre mulimile de mai sus este nevid i c modele sunt
construite succesiv, dup cum este descris n ceea ce urmeaz. S1
exist i este indiferent modul su de obinere. Apoi, pentru fiecare
i {1, 2, ...}, construim Si+1 pornind de la Si (i modificnd eventual i
pe Si-1, , S1), n felul urmtor: Si+1 pleac cu valorile de adevr
pentru A1, A2, ... , Ai stabilite de ctre Si i fixeaz o valoare pentru
Ai+1, n mod aleator. Dac nu avem Si+1 Mi+1, atunci revenim, alegnd
o structur Si+1 care s satisfac Mi+1 (tim c exist), prin schimbarea,
eventual, i a structurilor anterioare S1, S2, ... , Si (acestea vor fi simple
restricii ale lui Si+1, lucrul fiind evident posibil deoarece Mi Mi+1).
Ca urmare, putem defini structura S : A {0,1}, dat prin
-
100 Cristian Masalagiu
S(Ai) = Si(Ai), pentru fiecare i N*. Faptul c S este funcie i model
pentru M este imediat.
Teorema 2.13. Fie F LP, aflat n FNC i reprezentat ca mulime
(finit) de clauze. Atunci Res*(F) este finit.
Demonstraie. Artm mai nti c exist un k N astfel nct
Res(k)
(F) = Res(k+1)
(F). Fie | prop(F)| = n. Numrul total (m, s spunem)
al clauzelor peste (cel mult) n variabile atomice date este finit (de fapt,
m = 3n). Orice rezoluie ntr-un pas terge cte un literal. Prin
urmare, indiferent cte dintre cele m posibile clauze sunt prezente
iniial n F i orici pai de rezoluie am efectua, cardinalul oricrui
Res(i)
(F) nu poate depi m. Datorit acestui fapt i existenei
incluziunii Res(i)
(F) Res(i+1)(F) (pentru fiecare i N), afirmaia
noastr se deduce imediat. Mai mult, notnd cu j pe cel mai mic k cu
proprietatea de mai sus, avem Res(j)
(F) = Res(j+l)
(F), pentru fiecare l
N (lucru care rezult printr-o simpl inducie matematic i folosind
Definiia 2.11). De aici conchidem imediat c Res(j)(F) = Res*(F), de
unde card(Res*(F)) m.
Reamintind c vom elimina din orice mulime de forma Res*(F),
pe msur ce se obin, toate clauzele care conin o subformul de tipul
A A, enunm cea mai important teorem din acest capitol.
-
Fundamentele logice ale Informaticii 101
Teorema 2.14 (teorema rezoluiei pentru calculul propoziional).
Fie F o mulime oarecare de clauze din calculul propoziional. Atunci F
este nesatisfiabil dac i numai dac Res*(F).
Demonstraie. Conform Teoremei de compactitate, tim c F este
nesatisfiabil dac i numai dac exist o submulime finit a sa care
este nesatisfiabil. Din acest motiv, n cele de mai jos vom presupune
c F este o mulime finit de clauze, sau, alternativ, o formul
propoziional aflat n FNC. Fr a restrnge generalitatea, putem
presupune deci c F este o formul oarecare din LP (Teorema 2.6).
(corectitudine). S presupunem c Res*(F) i s artm c F
este nesatisfiabil. Conform Definiiei 2.11 i aplicrii repetate (de un
numr finit de ori) a Lemei rezoluiei, avem F Res(1)(F) Res(2)(F)
Res(n)(F) . Dac Res*(F) atunci exist k N, astfel nct
Res(k)(F), adic Res(k)(F) este nesatisfiabil ( este nesatisfiabil
prin convenie). Cum F Res(k)(F), rezult c F este nesatisfiabil.
(completitudine). S presupunem c F este nesatisfiabil i s
artm c Res*(F). Fie n = card(prop(F)). Procedm prin inducie
asupra lui n, adic demonstrm astfel adevrul metateoremei (n N)
( | prop(F)| = n i F este nesatisfiabil Res*(F)).
Baza. n = 0. Aceasta nseamn c F = {} = Res*(F) i concluzia este
evident.
Pas inductiv. Presupunem afirmaia adevrat pentru formule
construite peste n variabile propoziionale i o demonstrm pentru
-
102 Cristian Masalagiu
formule construite peste n+1 formule atomice. Fie F LP, construit
peste An+1 = {A1, A2, , An, An+1}. Pornind de la aceast formul vom
construi alte dou formule, notate n +1A
0F i respectivn 1A
1F , n modul
urmtor:
n +1A
0F se formeaz din F prin eliminarea sintactic a oricrei
apariii a literalului pozitiv An+1 din orice clauz i apoi
eliminarea n totalitate a tuturor clauzelor care conin o apariie
negativ a literalului An+1.
n 1A
1F se obine prin dualizare, adic din F se scot din toate
clauzele apariiile negative ale lui An+1 i se elimin apoi toate
clauzele care conin apariii pozitive ale aceleiai variabile.
Afirmaie. Dac F este nesatisfiabil, atunci att n +1A
0F ct i n 1A
1F
sunt nesatisfiabile. S presupunem c F este nesatisfiabil i nu are
clauze care sunt tautologii. Fie n +1A
0F i fie S orice structur corect
(definit pentru toate variabilele propoziionale care intervin n
formulele considerate). Considernd clauzele C ale lui n +1A
0F , avem
urmtoarele posibiliti :
C este o clauz din F, nemodificat. Evident c valoarea lui S
pentru aceast clauz nu se modific i astfel nu modific
valoarea de adevr a lui n +1A
0F fa de cea a lui F (dac lum n
considerare doar aceast clauz).
C provine dintr-o clauz din F, care coninea n plus o apariie
a lui An+1. Dac S(An+1) = 0, atunci S(C U {An+1}) = S(C), din
-
Fundamentele logice ale Informaticii 103
nou valoarea de adevr a lui n +1A
0F nemodificndu-se fa de cea
a lui F (relativ la C). Dac S(An+1) = 1, avem S(C U {An+1}) = 1.
Cum F este nesatisfiabil, nseamn c exist o alt clauz C,
C U {An+1} C F cu S(C) = 0. Este evident c C nu poate
conine pe An+1 deoarece S(An+1) = 1 i nici pe An+1 (n acest
caz C nu ar mai fi aprut n n +1A
0F ). Prin urmare, C apare i n
n +1A
0F , de unde urmeaz imediat c S(n +1A
0F ) = 0.
Mai exist posibilitatea ca nesatisfiabilitatea lui F s fi provenit din
faptul c S(C) = 0 pentru o clauz C F care conine neaprat An+1,
restul clauzelor lui F, ca i cele ale lui n +1A
0F , fiind adevrate n S. Acest
lucru nseamn c n aceast structur avem S(An+1) = 1. S considerm
structura S care coincide cu S, exceptnd valoarea lui An+1, care este
pus pe 0. Conform celor de mai sus, avem imediat S(F) =1, ceea ce
este absurd, F fiind nesatisfiabil. Rezult c n +1A
0F este nesatisfiabil.
Se procedeaz similar pentru n 1A
1F . (q. e. d.)
n acest moment tim c formulele n +1A
0F i n 1A
1F sunt nesatisfiabile i,
mai mult, sunt construite peste cel mult n variabile. Aplicnd ipoteza
inductiv pentru aceste formule rezult c Res*( n +1A
0F ) i
Res*( n 1A
1F ). Conform Teoremelor 2.11 i 2.13, exist o respingere
(D0) C1, C2, , Cl = , pornind cu elementele lui n +1A
0F , precum i o
-
104 Cristian Masalagiu
respingere (D1) B1, B2, Bt = , pornind cu clauzele lui n 1A
1F .
Adugm acum la fiecare clauz din (D0) pe An+1, peste tot de unde
acesta a fost scos (inclusiv la clauzele rezultate n urma aplicrii
rezoluiei ntr-un pas), obinnd o demonstraie prin rezoluie notat
(D0) i, analog, adugm la fiecare element din (D1) pe An+1 acolo
unde este necesar, obinnd o alt demonstraie prin rezoluie, notat
(D1) (odat An+1 respectiv An+1 introduse, ele nu vor mai fi terse).
Sunt posibile urmtoarele situaii:
Ultima clauz a lui (D0) este Cl = {An+1} i ultima clauz a lui
(D1) rmne Bt = Bt = (sau invers, Cl = Cl = i Bt = Bt =
{An+1}). Atunci concatenm cele dou liste care reprezint
demonstraiile (D0) i (D1), rezultnd evident o respingere
pornind cu clauzele lui F.
Ultima clauz lui (D0) este Cl = {An+1}i ultima clauz a lui
(D1) este Bt = {An+1}. Atunci concatenm din nou cele dou
liste i apoi mai facem un pas de rezoluie obinnd clauza final
C = Res(Cl, Bt) = . Din nou avem o respingere pornind cu
clauzele lui F.
n ambele situaii, conform Teoremei 2.11, rezult c Res*(F).
n urma acestui rezultat, putem concluziona c exist algoritmi
sintactici pentru a testa nesatisfiabilitatea formulelor din logica
propoziional, ei rmnnd (din pcate, dar nesurprinztor)
exponeniali ca timp de execuie. Lucrrile [MAS4] i [MAS5] pot fi
consultate pentru alte detalii legate de complexitatea rezoluiei. S
-
Fundamentele logice ale Informaticii 105
remarcm i faptul c testarea satisfiabilitii nu implic nimic special
(n acest caz, condiia de verificat va fi Res*(F)), ca de altfel nici
testarea validitii