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


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?.


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


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


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


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)


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:


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


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.


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


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):


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)


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)


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


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


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 ,


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.


(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


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


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.


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


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.


(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.


(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)


(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


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).


(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


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.


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.


(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.


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


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).


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:


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


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


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.


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.


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).


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.


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


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


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


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.


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,


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


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


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}


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.


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


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).


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).


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


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


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


(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


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.


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


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


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


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


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

Logica propoziţională

Documents

Transcript of Logica propoziţională