t6p16pe
Partea a II-a a textului de fata este dedicata metodelor de reprezentare a cunostintelor. Acest capitol si urmatoarele trei prezinta cele mai importante modele de reprezentare a cunostintelor utilizate in programele de inteligenta artificiala. In finalul Capitolului 6 se vor pune in evidenta modalitati de combinare a modelelor discutate, combinarea paradigmelor de reprezentare fiind tendinta actuala in sistemele bazate pe cunostinte.
Unul dintre primele si cele mai importante modele de reprezentare a cunostintelor in inteligenta artificiala este logica simbolica. Logica simbolica a fost dezvoltata de logicieni ca o metoda formala de rationament, in principal in domeniul matematicii, cel mai raspindit model logic fiind logica cu predicate de ordinul I.
Logica cu predicate de ordinul I a fost folosita pentru prima data ca metoda de reprezentare a cunostintelor in inteligenta artificiala in programul de demonstrare a teoremelor al lui Gilmore si in programul "The Logic Theorist" al lui Newell, Shaw si Simon a1963i. Programul lui Gilmore pentru demonstrarea teoremelor in logica cu predicate de ordinul I s-a bazat pe rezultatele teoretice importante ale lui Herbrand aChang,Lee,1973i care au stabilit conditiile in care o multime de formule (clauze) este inconsistenta. In 1965 Robinson, plecind de la rezultatele lui Herbrand, a propus o metoda mult mai eficienta de stabilire a inconsistentei unei formule: rezolutia. Aceasta metoda si diversele ei rafinari ulterioare au devenit abordarea preferentiala a celor mai multe demonstratoare de teoreme dezvoltate pina in prezent.
Utilizarea logicii simbolice ca model de reprezentare a cunostintelor in inteligenta artificiala este importanta deoarece ofera o abordare formala a rationamentului, cu fundamente teoretice riguroase. Formalismul logic permite derivarea unor cunostinte noi, plecind de la cele existente, pe baza deductiei si a demonstrarii teoremelor. Acest lucru faciliteaza automatizarea proceselor de rationament si executia inferentelor corecte si logic valide. Pe de alta parte, logica simbolica este suficient de expresiva si flexibila pentru a permite reprezentarea cu acuratete a cunostintelor problemei de rezolvat.

Rezolvarea problemelor in cadrul formalismului logic se bazeaza in special pe demonstrarea teoremelor. Exista doua abordari importante in demonstrarea teoremelor: metodele sintactice si metodele semantice.
Metodele sintactice de demonstrare a teoremelor, cum ar fi de exemplu cele propuse de Herbrand, Gilmore si Robinson, se bazeaza pe procedee mecanice de aplicare a regulilor de inferenta si sint independente de domeniul de interpretare al formulei. Aceste metode pot fi usor automatizate si constituie baza tuturor programelor de demonstrare a teoremelor.
Metodele semantice de demonstrare a teoremelor se bazeaza pe utilizarea sistematica a valorilor de adevar ale formulelor si depind de domeniul de interpretare fixat. Deoarece domeniul de interpretare al unei formule este de multe ori infinit, aceste metode sint greu algoritmizabile. O discutie a metodelor semantice de demonstrare poate fi gasita in Malita a1987i si Popa a1992i. O prezentare detaliata a principiilor teoretice si a metodelor sintactice de demonstrare a teoremelor poate fi gasita in Chang si Lee a1973i si Gabbay s.a. a1993i.
Reprezentarea cunostintelor in logica se bazeaza in esenta pe urmatoarele doua componente:
* Crearea structurilor formale care reprezinta fapte de baza, inferente si alte tipuri de cunostinte, numite structuri presupuse.
* Aplicarea regulilor de inferenta ale sistemului logic pentru a compara, combina si obtine din aceste structuri presupuse (date) noi structuri, numite structuri deduse.
De exemplu, enuntul "Toti studentii de la calculatoare stiu sa programeze" poate fi exprimat in logica cu predicate de ordinul I astfel:

Daca se stie in plus ca Radu este student la calculatoare, deci se poate concluziona pe baza celor doua structuri presupuse noua structura

3.1 Logica propozitionala
Logica propozitionala este un caz particular al logicii cu predicate de ordinul I. Elementele de baza ale logicii propozitionale sint propozitiile, numite si atomi sau propozitii simple. Urmatoarele enunturi sint propozitii:
Masina este alba P
Oamenii traiesc pe luna Q
Notatiile din dreapta reprezinta simbolic propozitiile enuntate. O propozitie poate fi adevarata sau falsa, deci poate avea doua valori de adevar. De exemplu, propozitia P este adevarata si propozitia Q este falsa. Atita timp cit se admit doar doua valori de adevar pentru o propozitie, adevarat si fals, logica se numeste logica clasica sau logica bivalenta. Acceptarea unui numar mai mare de valori conduce la logici polivalente (neclasice). Prezentarea care urmeaza se situeaza numai in cadrul logicii bivalente.
3.1.1 Sintaxa logicii propozitionale
Propozitiile simple sau atomii sint compozabile. Ele se pot combina, dind nastere la noi propozitii care sint, la rindul lor, adevarate sau false. Propozitiile combinate se formeaza din atomi folosind conectorii logici. Conectorii logici indica operatiile de asociere sau combinare care sint cele mai frecvente in vorbire sau rationament. De exemplu, din doua propozitii simple
Mihaela este frumoasa P1
Mihaela este buna P2 se poate forma propozitia compusa
Mihaela este frumoasa si Mihaela este buna notata cu . In continuare se vor folosi urmatoarele simboluri pentru conectorii logici:
I negatie
* conjunctie
* disjunctie
* implicatie simpla
* implicatie dubla
In consecinta, alfabetul logicii propozitionale este format din simbolurile care desemneaza atomii, conectorii logici si alte simboluri cum ar fi parantezele. In plus exista doua simboluri speciale pentru desemnarea valorilor logice de adevarat si fals, notate prin conventie cu a, respectiv f.
Limbajul logicii propozitionale se construieste pornind de la definitia alfabetului si definind regulile corecte de formare a cuvintelor limbajului cu simboluri din alfabet. Un cuvint in acest limbaj se numeste formula bine formata.
Definitie. O formula bine formata in calculul propozitional se defineste recursiv astfel:
(1) Un atom este o formula bine formata
(2) Daca P este formula bine formata, atunci *P este formula bine formata.
(3) Daca P si Q sint formule bine formate atunci P*Q, P*Q, P*Q si P*Q sint formule bine formate.
(4) multimea formulelor bine formate este generata prin aplicarea repetata a regulilor (1)*(3) de un numar finit de ori.
O formula bine formata se scrie riguros utilizind paranteze. De obicei se omit aceste paranteze ori de cite ori absenta lor nu da nastere la confuzii, tinind cont de precedenta conectorilor logici. Precedenta conectorilor logici, in ordine descrescatoare, este: I, *, *, *, *.
Exemple:
1. nu este o formula bine formata.
2. este o formula bine formata si poate fi scrisa .
3. este o formula bine formata si poate fi de asemenea scrisa .
3.1.2 Semantica logicii propozitionale
Semantica sau intelesul unei propozitii este valoarea de adevarat sau fals a acesteia, i.e. atribuirea unei valori de adevar acelei propozitii pe baza unei functii de evaluare a propozitiei.
Definitie. Se numeste interpretare a unei formule bine formate atribuirea de valori de adevar fiecarui atom din formula. Altfel spus, o interpretare specifica functiile de evaluare ale tuturor atomilor componenti ai formulei.
Exemplu. Fie formula si o interpretare I1 care asigneaza valorile de adevar a lui P si f lui Q. In aceasta interpretare formula este adevarata. O interpretare diferita I2 asigneaza valorile de adevar a lui P si a lui Q, formula fiind falsa in aceasta interpretare. Evident, exista patru interpretari distincte pentru aceasta propozitie.
Functia de evaluare a unei formule asociaza formulei o unica valoare de adevar, pe baza valorilor de adevar ale atomilor componenti ai formulei, utilizind regulile de evaluare ale conectorilor logici, reguli specificate de obicei prin tabele de adevar. Deoarece se refera la semantica formulei, aceste reguli se mai numesc si reguli semantice. In continuare se va nota valoarea de adevar a unei formule P cu Pv. Odata ce s-a stabilit o interpretare unei formule, valoarea ei de adevar poate fi determinata. Aceasta se poate face prin aplicarea repetata a regulilor semantice asupra unor portiuni din ce in ce mai mari ale formulei, pina cind se determina o singura valoare de adevar pentru formula. Regulile semantice sint prezentate in Figura 3.1.

Figura 3.1 Regulile semantice ale formulelor bine formate in calculul propozitional
Se observa ca Figura 3.1 reprezinta concis regulile de evaluare ale conectorilor logici. De exemplu, semnificatia tabelelor de adevar ale conectorilor logici * si * este surprinsa de regulile 3, 4, 8 si 9 din Figura 3.1. In aceste conditii se poate gasi semnificatia unei propozitii fiind data o interpretare I pentru acea propozitie.
Exemplu. Fie formula si interpretarea I: P adevarat, Q fals si R fals. Atunci: prin aplicarea regulii 2 IQ adevarat prin aplicarea regulii 3 adevarat prin aplicarea regulii 6 fals prin aplicarea regulii 5 fals
Deci valoarea de adevar PV a formulei in interpretarea I este fals.
3.1.3 Proprietatile propozitiilor
Pe baza functiei de evaluare si a domeniului de interpretare se pot specifica urmatoarele proprietati ale formulelor bine formate:
* O formula bine formata este valida sau tautologie daca formula are valoarea adevarat in orice interpretare.
* O formula bine formata este inconsistenta (contradictie, nerealizabila) daca formula are valoarea fals in orice interpretare.
* O formula bine formata este realizabila sau consistenta daca exista cel putin o interpretare in care formula are valoarea adevarat.
* Doua formule sint echivalente daca au aceeasi valoare de adevar in orice interpretare.
Figura 3.2 prezinta intuitiv aceste proprietati ale formulelor bine formate.

Figura 3.2 Realizabilitatea formulelor bine formate
Realizarea rationamentului intr-un sistem logic implica existenta unui mecanism de obtinere a noi formule pe baza formulelor existente, deci de extindere consistenta a cunostintelor universului problemei.
Definitie. O formula F este o consecinta logica a unei formule P daca F are valoarea adevarat in toate interpretarile in care P are valoarea adevarat. Definitia se poate extinde si in cazul a n formule. O formula F este consecinta logica a unei multimi de formule daca formula F este adevarata in toate interpretarile in care sint adevarate.
Consecinta logica se noteaza .
Exemple:
1. P este o formula realizabila dar nu este valida deoarece o interpretare care atribuie fals lui P atribuie fals si formulei P.
2. este o formula valida deoarece pentru orice interpretare, formula este adevarata.
3. este o contradictie deoarece pentru orice interpretare, formula este falsa.
4. P si I(IP) sint formule echivalente deoarece fiecare are aceeasi valoa¬re de adevar pentru orice interpretare.
5. P este o consecinta logica a formulei deoarece pentru orice interpretare in care este adevarata, P este totdeauna adevarata.
Notiunea de consecinta logica ofera o modalitate de a realiza inferenta valide in logica propozitionala. Urmatoarele doua teoreme stabilesc criteriile in functie de care o formula este o consecinta logica a unui set de formule.
Teorema. Formula F este consecinta logica a unei multimi de formule daca formula este valida.
Demonstratie.
(*) Daca F este o consecinta logica a multimii de formule , atunci pentru orice interpretare I in care sint adevarate, deci formula este adevarata, F este de asemenea adevarata prin definitie. Deci este adevarata pentru astfel de interpretari. Pentru interpretarile in care este falsa, este adevarata conform regulii 7 din Figura 3.1. Rezulta de aici ca este adevarata in orice interpretare, deci este formula valida.
(*) Daca este valida, atunci pentru orice interpretare I pentru care este adevarata, deci in care si sint adevarate, F este adevarata, deci F este o consecinta logica a multimii de formule .
Teorema. Formula F este consecinta logica a unei multimi de formule daca formula este inconsistenta.
Demonstratie.
Demonstratia acestei teoreme se face pe baza primei teoreme. Conform acesteia, F este o consecinta logica a multimii de formule daca si numai daca este valida, i.e. daca si numai daca este inconsistenta. , deci teorema este demonstrata.
Aceste doua teoreme prezinta o importanta deosebita in rationamentul logic, deoarece problema stabilirii consecintelor logice se reduce la problema demonstrarii validitatii sau a inconsistentei unei formule bine formate. Aceasta idee este importanta si reprezinta esenta tuturor metodelor de demonstrare automata a teoremelor in logica simbolica, asa cum se va vedea in Sectiunea 3.3.
O posibilitate de a determina echivalenta a doua formule este utilizarea tabelelor de adevar. Se observa ca demonstratia celei de a doua teoreme s-a facut utilizind echivalenta formulelor logice. De exemplu, pentru a arata ca este o formula echivalenta cu , se poate construi urmatoarea tabela de adevar.

In tabelul urmator sint prezentate citeva legi importante de echivalenta in logica propozitionala.

3.1.4 Discutie despre conectori
Definitie. O multime de conectori logici se numeste multime adecvata daca orice formula logica poate fi exprimata folosind numai conectorii acestei multimi.
Multimea este o multime adecvata de conectori. Deasemenea, perechile , si sint si ele multimi adecvate de conectori. Nici o alta pereche de conectori din multimea nu este o multime adecvata de conectori; de exemplu nu este o multime adecvata.
Se pune problema minimalitatii unei multimi de conectori, respectiv se pune intrebarea "Exista multimi adecvate formate dintr-un singur conector?". Exista doi conectori, care, fiecare in parte, formeaza o multime adecvata de conectori.
Conectorul lui Nicod, numit si Nor si notat cu *, permite definirea urmatoarelor formule de echivalenta: si , ceea ce face ca sa fie o multime adecvata. Conectorul are tabela de adevar:

Conectorul lui Sheffer, numit incompatibilitate, si notat cu *, este definit prin urmatoarea formula: , ceea ce inseamna ca este adevarat cind cel putin un atom este fals. Sint adevarate formulele: si , ceea ce face ca sa fie o multime adecvata. Conectorul are tabela de adevar:

Semnificatia anumitor conectori a fost mult discutata in logica. De exemplu, disjunctia introduce ambiguitatea. Exista doua tipuri de disjunctie, disjunctia simpla si disjunctia exclusiva, notata de obicei cu *. Urmatoarele formule definesc disjunctia exclusiva:


Replicatia, notata , este folosita pentru a elimina argumentatiile care nu sint de acord cu semnificatia implicatiei logice conform careia falsul implica orice si adevarul este implicat de orice. Tabela de adevar a replicatiei este prezentata mai jos, comparativ cu cea a implicatiei.

3.1.5 Reguli de inferenta in logica propozitionala
Regulile de inferenta in logica propozitionala ofera o modalitate de a realiza demonstratii logice sau deductii. Fiind data o multime de formule , problema este de a demonstra adevarul unei formule F, numita concluzie sau teorema, pe baza formulelor din P, numite axiome si utilizind regulile de inferenta.
Metodele sintactice de demonstrare a teoremelor, care nu se bazeaza pe atribuirea de valori de adevar atomilor din formula, utilizeaza reguli de inferenta sintactice. Aceste reguli de inferenta, logic valide, permit obtinerea de noi formule din multimea de formule initiale numai pe baza unor operatii sintactice. Cele mai importante reguli de inferenta (deductie) in logica propozitionala sint:
(1) Modus Ponens
(2) Substitutia. Daca P este o formula valida, formula P' obtinuta din P prin substitutia consistenta a atomilor din P este de asemenea valida.
Exista doua tipuri de substitutie: substitutia uniforma, in care o variabila se inlocuieste peste tot cu aceeasi formula (echivalenta cu ea sau nu) si substitutia prin echivalenta, in care se poate inlocui fiecare aparitie a unei variabile cu o alta formula, dar aceste formule trebuie sa fie echivalente cu variabila substituita.
Exemplu. Formula este valida; atunci formula este de asemenea valida prin aplicare regulii de substitutie uniforma.
(3) Regula inlantuirii
(4) Regula conjunctiei
(5) Regula transpozitiei
Observatie. Aceste reguli de inferenta pastreaza caracterul de tautologie al formulelor obtinute prin aplicarea lor, daca formulele de plecare sint tautologii.
3.2 Logica cu predicate de ordinul I
Modelul de reprezentare a cunostintelor in programele de inteligenta artificiala trebuie sa posede un grad mare de flexibilitate pentru a putea reprezenta adecvat domeniul discursului. Logica propozitionala nu are aceasta proprietate deoarece nu permite exprimarea proprietatilor obiectelor si a relatiilor existente intre obiecte, si nici generalizarea enunturilor la clase de obiecte cu caracteristici similare.
Logica cu predicate de ordinul I a fost dezvoltata tocmai pentru a da posibilitatea exprimarii rationamentelor despre obiecte complexe sau clase de obiecte si despre relatiile existente intre ele. Aceasta generalizare se face pe baza introducerii predicatelor in locul propozitiilor, a utilizarii functiilor, a variabilelor si a cuantificatorilor de variabile. Aceste concepte sint riguros definite in continuare.
3.2.1 Sintaxa logicii cu predicate de ordinul I
Alfabetul logicii cu predicate de ordinul I contine simboluri pentru reprezentarea constantelor, notate prin conventie cu litere mici de la inceputul alfabetului , variabilelor, notate prin conventie cu litere mici de la sfirsitul alfabetului , functiilor, notate cu , predicatelor, notate cu , a conectorilor si a cuantificatorilor logici. Conectorii logici folositi in logica cu predicate de ordinul I sint: si *, iar cuantificatorii sint cuantificatorul existential (*) si cuantificatorul universal (*).
In cazul logicii cu predicate de ordinul I, predicatele sint functii logice de mai multe argumente, argumentele predicatelor numindu-se termeni.
Definitie. Fie D un domeniu de valori. Un termen se defineste astfel:
(1) O constanta este un termen cu valoare fixa apartinind domeniului D.
(2) O variabila este un termen ce poate primi valori diferite din domeniul D.
(3) Daca f este o functie de n argumente si sint termeni, atunci este termen.
(4) Toti termenii sint generati prin aplicarea regulilor (1)*(3).
Definitie. Se numeste predicat de aritate n o functie P de n argumente cu valori adevarat sau fals, . Un predicat de aritate 0 este o propozitie, numita si predicat constant.
Definitie. Daca P este un predicat de aritate n si sint termeni, atunci se numeste atom sau formula atomica. Nici o alta expresie nu poate fi atom.
Definitie. Se numeste literal un atom sau un atom negat.
Definitie. O formula bine formata in logica cu predicate de ordinul I se defineste astfel:
(1) Un atom este o formula bine formata.
(2) Daca P este o formula bine formata atunci: sint formule bine formate.
(3) Daca P si Q sint formule bine formate atunci: sint formule bine formate.
(4) Orice formula bine formata este generata prin aplicarea de un numar finit de ori a regulilor (1)*(3).
O reprezentare intuitiva a modului de construire a cuvintelor, deci a formelor bine formate in limbajul logicii cu predicate de ordinul I, este prezentata in Figura 3.3. In continuare se vor omite parantezele din formule ori de cite ori aceasta nu creeaza ambiguitate. De asemenea, in anumite conditii, se va folosi *x si *y in loc de si .

Figura 3.3 Constructia formulelor bine formate in logica cu predicate de ordinul I
Exemple:
1. este o formula bine formata. , si sint literali, in acest caz literali pozitivi deci nenegati. x, y, z sint variabile.
2. este o formula bine formata. x, y si z sint variabile, f(x) functie, toate fiind considerate termeni. este un literal.
3. este o formula bine formata. si sint literali, primul pozitiv si cel de al doilea negativ.
4. nu este o formula bine formata deoarece cuantificatorii nu pot fi aplicati predicatelor. Acest lucru este posibil numai in logicile de ordin superior (logici de ordinul II).
5. nu este o formula bine formata deoarece negatia nu poate fi aplicata unei constante si, in general, nici unui termen.
6. nu este o formula bine formata deoarece argumentele predicatelor nu pot fi predicate.
Definitie. O formula bine formata este in forma normala conjunctiva, pe scurt FNC, daca formula are forma , unde este o formula formata dintr-o disjunctie de literali.
Definitie. O formula bine formata este in forma normala disjunctiva, pe scurt FND, daca formula are forma , unde este o formula formata dintr-o conjunctie de literali.
De exemplu, este o formula in forma normal conjunctiva, iar este o formula in forma normal disjunctiva.
3.2.2 Semantica logicii cu predicate de ordinul I
Similar logicii propozitiilor, semantica unei formule bine formate in logica cu predicate de ordinul I se poate stabili pe baza domeniului de interpretare al formulei. Domeniul de interpretare este multimea tuturor obiectelor din care se selecteaza constantele, variabilele si care stabileste domeniul de definitie si domeniul de valori ale functiilor din formule. Daca nu este exprimat explicit, domeniul de interpretare se deduce din context, putind fi si infinit. Odata stabilit domeniul de interpretare, se poate specifica interpretarea unei formule bine formate, deci se poate afla valoarea ei de adevar in acea interpretare.
Definitie. Interpretarea unei formule F in logica cu predicate de ordinul I consta in fixarea unui domeniu de valori nevid D si a unei asignari de valori pentru fiecare constanta, functie si predicat ce apar in F astfel:
(1) Fiecarei constante i se asociaza un element din D.
(2) Fiecarei functii f, de aritate n, i se asociaza o corespondenta , unde .
(3) Fiecarui predicat de aritate n, i se asociaza o corespondenta .
Exemplu. Fie urmatoarea formula bine formata cu domeniul de interpretare D=A1,2S si urmatoarea interpretare I:

Pentru a stabili valoarea de adevar a formulei se considera:
* fals
* adevarat
In consecinta, deoarece formula nu este adevarata pentru orice x din domeniul de interpretare D, expresia are valoarea de adevar fals.
Odata stabilite sintaxa si semantica logicii cu predicate de ordinul I, aceasta poate fi utilizata pentru a reprezenta cunostinte. In continuare se dau exemple de transformare a unor enunturi din limbaj natural in logica cu predicate de ordinul I.
Fie urmatoarele patru enunturi, dintre care primele trei sint axiome si cel de-al patrulea este teorema de demonstrat, sau concluzia.
(1) Oricine poate citi este literat.
(2) Delfinii nu sint literati.
(3) Anumiti delfini sint inteligenti.
(4) Exista inteligenti care nu pot citi.
Exprimind cele patru propozitii in logica cu predicate de ordinul I se obtine:
(A1)
(A2)
(A3)
(A4) unde cu Citeste(x) s-a notat asertiunea "x poate citi", cu Delfin(x) "x este delfin", cu Literat(x) "x este literat" si cu Inteligent(x) "x este inteligent". Domeniul de interpretare al acestor formule este considerat implicit multimea tuturor fiintelor.
Fie axiomele de baza ale numerelor naturale:
(1) Pentru fiecare numar natural exista un unic succesor imediat.
(2) Nu exista nici un numar natural pentru care 0 este succesorul imediat.
(3) Pentru orice numar natural diferit de zero, exista un unic predecesor imediat.
Utilizind functia s(x) pentru a desemna succesorul imediat al lui x, functia p(x) pentru predecesorul imediat al lui x si predicatul pentru a exprima asertiunea "x este egal cu y", se obtine urmatoarea exprimare a axiomelor numerelor naturale in logica cu predicate de ordinul I.
(A1)
(A2)
(A3)
Domeniul de interpretare al acestor formule este evident multimea numerelor naturale, iar functiile s(x) si p(x) sint definite in consecinta.
Intr-o formula variabilele pot fi variabile libere sau legate. O variabila este legata intr-o formula daca exista un cuantificator ce o refera. In caz contrar, variabila este libera. O formula care contine variabile libere nu poate fi evaluata. De exemplu, formula nu poate fi evaluata deoarece nu se cunoaste cuantificarea lui y si nici cea a lui z. Variabila x este legata, iar variabilele y si z sint libere.
3.2.3 Proprietatile formulelor bine formate
Proprietatile formulelor bine formate in logica cu predicate de ordinul I sint aceleasi ca si in logica propozitiilor: validitate, inconsistenta, realizabilitate, echivalenta formulelor, consecinta logica. Definitiile sint similare dar, de aceasta data, trebuie sa se considere interpretarile pentru toate domeniile de interpretare posibile ale formulelor. De exemplu, formula: din sectiunea anterioara nu este o tautologie, deci nu este valida, deoarece exista cel putin o interpretare pentru care ea este falsa. Formula este inconsistenta sau contradictie deoarece nu exista nici o interpretare pentru care aceasta formula sa fie adevarata. Formula este insa valida, deoarece ea este adevarata indiferent de interpretare.
Fie urmatoarele doua formule:
(A1) Bun(roco)
(A2)
Se poate arata ca formula , unde roco este o constanta, este o consecinta logica a formulelor (A1) si (A2). Sa presupunem ca atit (A1) cit si (A2) sint adevarate intr-o interpretare I. Atunci formula este adevarata deoarece (A2) specifica pentru "orice x" din domeniu. Dar se stie ca Bun(roco) este adevarata in interpretarea I pe baza lui (A1), deci rezulta ca este adevarata deoarece adevarat nu poate implica fals. S-a demonstrat ca pentru orice interpretare in care (A1) si (A2) sint formule adevarate si formula este adevarata, deci este o consecinta logica a formulelor (A1) si (A2).
Echivalenta formulelor poate fi stabilita utilizind legile de echivalenta din logica cu predicate de ordinul I prezentate in Figura 3.4. In figura s-au notat cu Q si cuantificatorii universal si existential.

Figura 3.4 Legi de echivalenta a formulelor in logica cu predicate de ordinul I

Figura 3.4 (continuare) Legi de echivalenta a formulelor in logica cu predicate de ordinul I
In toate exemplele mentionate mai sus s-au folosit metode semantice pentru stabilirea caracterului formulelor. In sectiunea urmatoare se vor discuta metode semantice pentru realizarea deductiilor si stabilirea caracterului unei multimi de formule. Dupa cum se observa din exemplele de mai sus, inspectarea tuturor interpretarilor unei formule peste toate domeniile posibile poate fi deosebit de dificila, daca nu imposibila in anumite cazuri, deci o astfel de abordare este greu de automatizat.
3.2.4 Reguli de inferenta in logica cu predicate de ordinul I
Regulile de inferenta sintactice din logica propozitionala prezentate in Sectiunea 3.1.5, Modus Ponens, substitutia, inlantuirea, conjunctia si transpozitia, pot fi generalizate in cazul logicii cu predicate de ordinul I. De exemplu, regula Modus Ponens are urmatoarea forma:
Modus Ponens
Se observa ca s-a facut substitutia lui a cu x, ceea ce a fost posibil deoarece P(x)*Q(x) este adevarata pentru orice interpretare.
Regula substitutiei poate avea forme mai sofisticate in cazul logicii cu predicate de ordinul I. Aceste forme vor fi discutate in sectiunea urmatoare. Tot in aceeasi sectiune se prezinta in detaliu si rezolutia, regula de inferenta sintactica importanta.
Regulile de inferenta prezentate sint reguli deductive, deci valide. Ele pastreaza caracterul de tautologie al formulei. In programele de inteligenta artificiala se folosesc insa si reguli de inferenta nedeductive, numite si invalide deoarece rezultatele obtinute pe baza acestor reguli nu sint intotdeauna adevarate. Aceste reguli pot fi insa utile in numeroase cazuri, asa cum se va vedea mai tirziu, desi nu garanteaza corectitudinea rezultatului obtinut. In continuare se prezinta citeva astfel de reguli de inferenta invalide, dar utilizate:
(1) Inferenta abductiva. Inferenta abductiva se bazeaza pe utilizarea cunostintelor cauzale pentru a explica sau a justifica o concluzie, posibil invalida. Inferenta abductiva are urmatoarea forma:

De exemplu, din formulele:
se poate infera desi s-ar putea ca Radu sa se legene datorita unui cutremur de pamint.
(2) Inferenta inductiva. Inferenta inductiva se bazeaza pe ideea ca o proprietate adevarata pentru o submultime de obiecte dintr-o clasa este adevarata pentru toate exemplele din acea clasa. Inferenta inductiva are forma:

De exemplu, dupa ce se constata ca cele mai multe lebede sint albe, se poate infera prin inductie ca toate lebedele sint albe, desi exista si lebede negre, cum ar fi unele dintre cele care cresc in Australia.
(3) Inferenta analogica. Inferenta analogica este o forma de inferenta bazata pe experienta si se bazeaza pe ideea conform careia situatii sau entitati care tind sa fie asemanatoare sub anumite aspecte sint asemanatoare in general. Inferenta analogica este de fapt o combinatie a celorlalte forme de inferenta: abductive, deductive si inductive. Inferenta analogica are forma:

Toate aceste trei forme de inferenta sint invalide, dar reprezinta modalitati de simulare a rationamentului de bun simt. Ele sint folosite in inteligenta artificiala, mai ales in cazul programelor de invatare automata, asa cum se va vedea in Capitolul 9.
3.2.5 Rezolvarea problemelor in cadrul formalismului logic
Pentru a putea investiga cum se rezolva problemele in logica cu predicate de ordinul I si puterea expresiva a acestui model de reprezentare a cunostintelor, se considera urmatorul exemplu. Fie multimea de enunturi:
(1) Marcus era om.
(2) Marcus era pompeian.
(3) Toti pompeenii erau romani.
(4) Cezar era dictator.
(5) Toti romanii fie erau devotati lui Cezar, fie il urau.
(6) Fiecare om este devotat cuiva.
(7) Oamenii incearca sa asasineze dictatorii fata de care nu sint devotati.
(8) Marcus a incercat sa-l asasineze pe Cezar.
Faptele descrise de aceste propozitii pot fi reprezentate sub forma de formule bine formate in calculul cu predicate de ordinul I astfel:
(1) Marcus era om se exprima sub forma:
(A1) Om(marcus)
Aceasta reprezentare surprinde elementul esential al propozitiei, si anume faptul ca Marcus era om, dar nu exprima informatia continuta in limbaj natural despre timpul trecut utilizat. Pentru exemplul considerat aceasta informatie este nerelevanta, dar in alte cazuri ea ar putea sa conteze, deci ar trebui extinsa reprezentarea in consecinta.
(2) Marcus era pompeian se exprima sub forma:
(A2) Pompeian(marcus)
(3) Toti pompeenii erau romani se exprima sub forma:
(A3)
Conform conventiei facute x este o variabila, in timp ce simbolul marcus utilizat in (A1) si (A2) este o constanta.
(4) Cezar era dictator se exprima sub forma:
(A4) Dictator(cezar)
Tot conform conventiei facute, simbolul cezar este considerat o constanta. In plus, se face presupunerea implicita ca exista un unic individ care se numeste Cezar in universul problemei de rezolvat.
(5) Toti romanii erau fie devotati lui Cezar fie il urau. Pentru a exprima aceasta propozitie, tinind cont de semantica ei, nu se poate folosi conectorul logic * care are semnificatia de "sau inclusiv", ci trebuie folosit un "sau exclusiv". In aceste conditii propozitia se exprima sub forma:
(A5)

(6) Fiecare om este devotat cuiva se exprima sub forma:
(A6)
Aici apare o noua problema de traducere a limbajului natural in forma logica, si anume ordinea cuantificatorilor. Utilizind formula logica de mai sus s-a presupus ca pentru orice persoana x, exista o persoana y fata de care x este devotata. Dar aceeasi fraza ar fi putut fi interpretata, eventual, si ca exista o persoana y fata de care toate celelalte persoane sint devotate, ceea ce s-ar fi exprimat in logica sub forma:

(7) Oamenii incearca sa asasineze dictatorii fata de care nu sint devotati poate fi exprimata sub forma:
(A7)
Evident ca si in acest caz ar fi putut sa existe o exprimare logica diferita. Cititorul poate incerca sa o gaseasca.
(8) Marcus a incercat sa-l asasineze pe Cezar se exprima sub forma:
(A8)
Presupunind ca faptele (1)*(8) sint adevarate, deci sint axiome, cum se poate stabili daca Marcus nu era devotat lui Cezar, deci cum se poate demonstra teorema (concluzia):
(c) ?
Aceasta demonstratie se poate face aplicind regulile de inferenta ale logicii cu predicate de ordinul I prezentate in sectiunea anterioara. Inspectind axiomele (A1)*(A8), se observa ca demonstratia s-ar putea face numai pe baza axiomelor (A1), (A4), (A7) si (A8). Dar apare urmatoarea problema: desi oricine stie ca daca Marcus este om el este in acelasi timp persoana, acest lucru nu este explicit indicat in enunt. Se observa de aici una din dificultatile fundamentale in rezolvarea problemelor de inteligenta artificiala si anume reprezentarea cunostintelor de bun simt. Pentru a putea rezolva problema, trebuie adaugat un nou enunt care sa statueze ca toti oamenii sint persoane.
(9) Toti oamenii sint persoane se exprima sub forma:
(A9)
In acest moment se poate demonstra concluzia (c) pe baza axiomelor (A1), (A4), (A7), (A8) si (A9). Aplicind regula substitutiei in axioma (A7) si substituind uniform variabila x cu constanta marcus si variabila y cu constanta cezar se obtine o noua axioma
(A10)

Aplicind regula Modus Ponens asupra axiomelor (A1) si (A9) se obtine:
(A11) Persoana(marcus) si aplicind din nou regula Modus Ponens asupra axiomelor (A11), (A4), (A8) si (A10) se obtine concluzia cautata:

Se observa ca aceasta demonstratie a fost facuta prin selectia intuitiva a axiomelor ce trebuie combinate si a diverselor reguli de inferenta ce trebuie utilizate. O asemenea abordare este evident nepractica intr-un program de demonstrare automata a teoremelor. Pentru a putea automatiza procesul de demonstrare este preferabil sa existe o singura regula de inferenta. Aceasta este rezolutia. In plus, trebuie stabilita o strategie de aplicare a regulii de inferenta pentru a ajunge cit mai repede la solutie, daca exista solutie. Aceste probleme vor fi abordate in sectiunea urmatoare.
Un alt aspect important ce trebuie considerat in momentul in care se discuta rezolvarea problemelor in cadrul formalismului logic este posibilitatea existentei unei solutii. Este orice teorema demonstrabila? In cazul logicii propozitionale exista intotdeauna proceduri efective care permit atit stabilirea faptului ca o formula este teorema, cit si a faptului ca nu este teorema. In consecinta problema demonstrarii teoremelor in logica propozitionala este decidabila. In cazul logicii cu predicate de ordinul I se garanteaza existenta unei proceduri care sa demonstreze ca o formula este teorema daca acea formula este intr-adevar teorema. Dar aceasta procedura nu este garantata sa se opreasca daca formula de demonstrat nu este teorema. In consecinta demonstrarea teoremelor in logica cu predicate de ordinul I nu este decidabila, ci este o problema semidecidabila.
In pofida acestui rezultat trist, formalismul logic este utilizat intens ca metoda de rezolvare a problemelor in inteligenta artificiala deoarece, in cele mai multe cazuri, produce rezultatele dorite. De asemenea trebuie tinut cont de faptul ca utilizarea unei strategii particulare sau a unei combinatii de strategii in demonstrarea teoremelor poate genera situatii in care o teorema nu se poate demonstra chiar daca acea formula este intr-adevar teorema. Acesta este cazul strategiilor incomplete. Si in aceasta situatie s-au facut compromisuri, in sensul ca s-au acceptat strategii incomplete de demonstrare a teoremelor datorita avantajului de eficienta pe care il aduc. O strategie completa va reusi intotdeauna sa demonstreze ca o formula este teorema daca formula este cu adevarat teorema, dar aceasta completitudine poate fi penalizata de necesitati crescute ale resurselor de timp si spatiu utilizate de programul care o implementeaza.
3.3 Demonstrarea teoremelor utilizind rezolutia
In 1965, Robinson propune principiul rezolutiei ca metoda eficienta de demonstrare a teoremelor, principiu care reprezinta baza tuturor demonstratoarelor automate de teoreme actuale. Rezolutia este o metoda de inferenta sintactica care, aplicata repetat unei multimi de formule in forma standard, determina daca multimea de formule este inconsistenta. Pentru a demonstra ca formula C este o consecinta logica a formulelor , se demonstreaza ca este o formula nerealizabila prin deducerea unei contradictii.
Principiul rezolutiei este o metoda de demonstrare prin respingere, care corespunde in general unei demonstrari prin reducere la absurd. De aceea, utilizarea principiului rezolutiei in demonstrarea teoremelor se mai numeste si metoda respingerii prin rezolutie sau respingere rezolutiva. Metoda rezolutiei se aplica insa unei forme standard a formulelor, numita forma clauzala, forma introdusa de Davis si Putnam.
3.3.1 Transformarea formulelor in forma clauzala
Definitie. Se numeste clauza o disjunctie de literali. Se numeste clauza de baza o clauza fara variabile. Se numeste clauza Horn o clauza care contine cel mult un literal pozitiv.
Definitie. Se numeste clauza vida o clauza fara nici un literal; clauza vida se noteaza, prin conventie, cu . Se numeste clauza unitara o clauza ce contine un singur literal.
O clauza Horn poate avea una din urmatoarele patru forme: o clauza unitara pozitiva ce consta intr-un singur literal pozitiv; o clauza negativa formata numai din literali negati; o clauza formata dintr-un literal pozitiv si cel putin un literal negativ (clauza Horn mixta) sau clauza vida. Se numeste clauza (Horn) distincta o clauza ce are exact un literal pozitiv, ea fiind fie o clauza unitara pozitiva, fie o clauza Horn mixta.
Exemple:
1. este o clauza. Intr-o clauza toate variabilele sint implicit cuantificate universal.
2. este o clauza Horn, in particular o clauza Horn distincta.
3. este o clauza de baza deoarece nu contine variabile.
Transformarea unei formule bine formate in forma clauzala se face pe baza regulilor prezentate in continuare.
Pasul 1. Se elimina toti conectorii logici de implicatie si echivalenta folosind legile de eliminare a implicatiei si a implicatiei duble prezentate in Figura 3.4.
Pasul 2. Se muta toate negatiile din formula astfel incit sa preceada atomii folosind legea negarii negatiei, legile lui De Morgan si legile de echivalenta a cuantificatorilor prezentate in Figura 3.4.
Exemplu. Formula se transforma in apoi in din care se obtine in final formula .
Pasul 3. Se redenumesc variabilele, daca este cazul, astfel incit toti cuantificatorii sa se refere la variabile diferite, i.e. se redenumesc variabilele astfel incit variabilele referite de un cuantificator sa nu aiba acelasi nume cu variabilele referite de alt cuantificator.
Exemplu. In formula se redenumeste cea de a doua variabila x referita de cuantificatorul existential (*x) si se obtine formula .
Pasul 4. Se elimina toti cuantificatorii existentiali din formula printr-un proces de substitutie numit skolemnizare. Acest proces necesita ca toate variabilele definite de un cuantificator existential sa fie inlocuite prin functii Skolemn, adica functii arbitrare care pot lua intotdeauna valoarea ceruta de cuantificatorul existential. Skolemnizarea se executa dupa urmatoarele reguli:
4.1. Daca primul (cel mai din stinga) cuantificator este un cuantificator existential, se inlocuiesc toate aparitiile variabilei pe care o cuantifica cu o constanta arbitrara care nu apare nicaieri in expresie si se elimina cuantificatorul. Acest proces se aplica pentru toti cuantificatorii existentiali care nu sint precedati de cuantificatori universali, folosind constante diferite in substitutie.
4.2. Pentru fiecare cuantificator existential care este precedat de unul sau mai multi cuantificatori universali, se inlocuiesc toate aparitiile variabilei cuantificate printr-o functie care nu mai apare in expresie si care are ca argumente toate variabilele cuantificate universal ce preced cuantificatorul existential. Cuantificatorul existential se elimina. Procesul se repeta pentru fiecare cuantificator existential folosind un simbol de functie diferit si alegind ca variabile ale functiei argumentele care corespund tuturor variabilelor cuantificate universal ce preced cuantificatorul existential.
Exemplu. Expresia se transforma prin substitutii de skolemnizare in . Inlocuirea variabilei y cu o functie arbitrara de argumente v si x se justifica pe baza faptului ca variabila y, urmind dupa variabilele v si x, poate fi dependenta functional de acestea iar in acest caz, functia arbitrara g poate reproduce aceasta dependenta.
Pasul 5. Se muta toti cuantificatorii unviersali la stinga expresiei si se transforma expresia in forma normal conjunctiva.
Pasul 6. Se elimina toti cuantificatorii universali deoarece ei sint retinuti implicit in forma clauzala si se elimina conjunctiile din forma normal conjunctiva. In acest fel se obtine o multime de formule numite clauze.
Observatie. Multimea de clauze obtinute prin procesul de mai sus nu este echiv¬alenta cu formula originala dar realizabilitatea formulei este pastrata. Multimea de clauze este realizabila respectiv inconsistenta, daca si numai daca formula originala este realizabila, respectiv inconsistenta.
Exemplu. Se considera urmatoarea formula

Pentru a transforma aceasta formula in forma clauzala se aplica procedeul descris anterior. Prin executia procedurii pas cu pas se obtine
Pasul 1. Se elimina conectorul de implicatie logica si se obtine

Pasul 2. Se aduc negatiile in fata atomilor si se obtine

Pasul 3. Acest pas nu este necesar deoarece toate variabilele cuantificate au nume distincte.
Pasul 4. Se aplica skolemnizarea si se elimina astfel cuantificatorii existentiali prin introducerea functiilor g(y), h(y) si l(y) si a constantei a. Se obtine

Pasul 5. Se transforma formula in forma normal conjunctiva si se obtine

Pasul 6. Se elimina cuantificatorul universal si conjunctia, obtinindu-se multimea de doua clauze


Aceasta multime de clauze reprezinta transformarea formulei initiale in forma clauzala.
3.3.2 Rezolutia in logica propozitionala
Pentru a explica principiul rezolutiei, in aceasta sectiune se prezinta rezolutia pentru cazul particular al demonstrarii teoremelor in logica propozitionala. Principiul rezolutiei in logica propozitionala este urmatorul. Pentru orice doua clauze C1 si C2, daca exista un literal L1 in C1 care este complementar cu un literal L2 in C2 atunci disjunctia intre C1 din care s-a eliminat L1 si C2 din care s-a eliminat L2 este rezolventul clauzelor C1 si C2. Se mai spune ca cele doua clauze, C1 si C2, rezolva.
Definitie. Fie clauzele:
(C1)
(C2) cu . Rezolventul clauzelor C¬1 si C¬2 este deci
(C)
Teorema. Fiind date doua clauze, C1 si C2, un rezolvent C al clauzelor C1 si C2 este o consecinta logica a clauzelor C1 si C2.
Pentru a demonstra ca o formula S este o teorema derivata dintr-un set de axiome A utilizind principiul rezolutiei, se aplica algoritmul prezentat in continuare. Ideea algoritmului este aceea de a porni de la o multime de clauze care se presupune a fi realizabila si a genera noi clauze care reprezinta restrictii asupra modului in care clauzele originale pot fi facute adevarate. Apare o contradictie in momentul in care o clauza devine atit de restrictionata incit nu mai poate fi facuta adevarata. Acest lucru este indicat de generarea clauzei vide.
Algoritm: Respingerea prin rezolutie in logica propozitionala.
1. Converteste setul de axiome A in forma clauzala si obtine multimea de clauze S0
2. Neaga teorema, transforma teorema negata in forma clauzala si adauga rezultatul la S0

3. repeta
3.1. Selecteaza o pereche de clauze C1 si C2 din S
3.2. Determina
3.3. daca atunci pina s-a obtinut clauza vida ( ) sau nu mai exista nici o pereche de clauze care rezolva
4. daca s-a obtinut clauza vida atunci teorema este adevarata (este demonstrata)
5. altfel teorema este falsa sfirsit.
Se considera urmatoarele enunturi:
(1) Am timp liber.
(2) Daca am timp liber si ma plimb atunci cunosc orasul.
(3) Daca este soare sau este cald atunci ma plimb.
(4) Este cald.
Se cere sa se demonstreze utilizind metoda respingerii prin rezolutie enuntul:
(5) Cunosc orasul.
Pentru aceasta se exprima primele patru enunturi si enuntul de demonstrat in logica propozitionala obtinindu-se urmatorul set de axiome
(A1) T
(A2)
(A3)
(A4) C si concluzia de demonstrat
(C) O
Se transforma axiomele in forma clauzala, se neaga teorema (C) si se adauga la multimea de clauze obtinute din axiome. In urma acestui proces se obtine urmatoarea multime de clauze:
(C1) T
(C2)
(C3)
(C3')
(C4) C
(C5) IO
Deducerea clauzei vide din setul de axiome, deci demonstrarea prin respingere a teoremei "Cunosc orasul", este prezentata in Figura 3.5.

Figura 3.5 Respingerea prin rezolutie in logica propozitionala
3.3.3 Unificarea expresiilor
In logica propozitionala este usor sa se identifice perechile de literali complementari, L si IL, din doua clauze pentru a aplica rezolutia. In logica cu predicate de ordinul I acest lucru este mai dificil deoarece in procesul de identificare trebuie tinut cont de argumentele predicatelor. De exemplu, literalii P(x) si P(a) pot unifica cu conditia ca sa se aplice o regula de substitutie in primul literal prin care variabila x sa fie inlocuita cu constanta a. Gasirea unei substitutii pentru variabilele din expresii sau subexpresii astfel incit expresiile, respectiv subexpresiile, sa devina identice, se numeste unificare si este un proces esential in demonstrarea teoremelor in general si, in particular, prin metoda rezolutiei.
Definitie. O substitutie este o multime de perechi , in care vi sint variabile distincte si ti sint termeni care nu contin vi. Termenii ti inlocuiesc variabilele in orice expresie in care se aplica substitutia. O substitutie se noteaza .
In continuare se vor folosi litere grecesti pentru reprezentarea substitutiilor. Rezultatul aplicarii unei substitutii * asupra unei expresii E este notat E* si este expresia obtinuta prin inlocuirea tuturor aparitiilor variabilei vi cu termenul ti in expresia E, pentru toate perechile din substitutia *. O expresie poate fi un termen, un literal, un atom sau o formula bine formata sau o multime de termeni, literali, atomi sau formule bine formate.
Exemple:
1. Se considera expresia si substitutiile , , , . Prin aplicarea, pe rind, a acestor substitutii expresiei E se obtine:




Se observa ca este o clauza de baza.
2. Fie expresia si aplicind substitutia se obtine expresia .
Definitie. Se numeste unificator al unei multimi de expresii , o substitutie * care face ca expresiile sa devina identice, adica . Multimea se numeste multime de expresii unificabila, daca exista un unificator pentru aceasta multime. Se mai spune ca multimea de expresii unifica.
Definitie. Un unificator * al unei multimi de expresii este cel mai general unificator, pe scurt mgu, daca si numai daca pentru orice alt unificator * al multimii exista o substitutie *' astfel incit . Altfel spus, orice unificator * al multimii este o instanta a lui * .
Observatie. Daca doua expresii unifica, atunci exista un unic cel mai general unificator.
Exemple:
1. Fie expresiile si . Cele doua expresii unifica aplicind substitutia , . Aplicind substitutia se obtine . Se observa ca este cel mai general unificator al celor doua expresii.
2. Fie expresiile si . Cel mai general unificator al celor doua expresii este unde y' si z' sint aparitiile variabilelor y si z in E2. Rezultatul unificarii este .
3. Fie expresiile si . Aceste doua expresii nu unifica deoarece o posibila incercare de substitutie de tipul este ilegala. Daca z este substituit cu x si cu , de fapt x este substituit cu ceea ce contrazice definitia substitutiei.
Observatie. Unificarea se poate aplica si literalilor dintr-o aceeasi clauza. Daca exista un cel mai general unificator astfel incit doi sau mai multi literali dintr-o clauza unifica, clauza care ramine prin eliminarea tuturor literalilor cu exceptia unuia din literalii unificati este numita factor al clauzei originale. De exemplu, fie clauza si cel mai general unificator . Atunci clauza este un factor al clauzei initiale C.
In continuare se prezinta algoritmul de unificare a literalilor sau a expresiilor in general in logica cu predicate de ordinul I.
Algoritm: Unificarea expresiilor

1. daca E1 si E2 sint constante atunci
1.1. daca atunci intoarce A S
1.2. intoarce INSUCCES
2. daca E1 este variabila sau E2 este variabila atunci
2.1. Schimba E1 cu E2 astfel incit E1 sa fie variabila
2.2. daca atunci intoarce A S
2.3. daca E1 apare in E2 atunci intoarce INSUCCES
2.4. intoarce
3. daca si sau si /* aceleasi simboluri predicative sau functionale cu aceeasi aritate */ atunci
3.1.
3.2.
3.3.
3.4.
3.5.
3.6. daca atunci intoarce INSUCCES
3.7
3.8
3.9
3.10. daca atunci intoarce INSUCCES
3.11. intoarce
4. intoarce INSUCCES sfirsit.
Observatii:
1. Algoritmul intoarce lista de substitutii care formeaza cel mai general unificator al celor doua expresii (literali) E1 si E2. Algoritmul este garantat sa produca cel mai general unificator, daca acesta exista.
2. In cazul in care cele doua expresii nu unifica, algoritmul intoarce valoarea speciala INSUCCES pentru a marca esecul unificarii.
3. Pasul 2.3 verifica daca o expresie care contine o anumita variabila nu este unificata cu acea variabila.
3.3.4 Rezolutia in logica cu predicate de ordinul I
Aplicarea principiului rezolutiei in logica cu predicate de ordinul I implica construirea rezolventului a doi literali complementari, care fie sint identici, fie au fost facuti identici prin aplicara substitutiei definita de cel mai general unificator al celor doi literali asupra clauzelor ce contin acesti doi literali.
Definitie. Fie clauzele:
(C1)
(C2) numite clauze parinte si * cel mai general unificator al literalilor Pi si Qj, cu . Atunci este un rezolvent binar al clauzelor C1 si C2.
Observatie. Rezolventul a doua clauze nu este unic. Aplicarea rezolutiei intre doua clauze care rezolva poate genera diversi rezolventi in cazul in care in cele doua clauze exista mai multi literali complementari care, prin unificare, pot fi facuti identici.
Exemple:
1. Fie clauzele si . Cel mai general unificator al celor doua clauze este si rezolventul celor doua clauze este , literalii complementari care au rezolvat fiind Literat(x) si ILiterat(y).
2. Fie clauzele si . Aceste doua clauze pot rezolva si pot produce diversi rezolventi. Daca se selecteaza atunci si si prin unificarea literalilor si . Aplicind o noua subtitutie pentru aceasta clauza, , se obtine .
Daca se selecteaza cel mai general unificator al literalilor si , atunci se obtine un alt rezolvent .
Daca se selecteaza ca cel mai general unificator al literalilor si atunci .
Demonstrarea teoremelor aplicind metoda respingerii prin rezolutie poate fi descrisa de algoritmul urmator. Enunturile care descriu problema trebuie exprimate in modelul logic si formeaza multimea de axiome A. Concluzia care trebuie obtinuta, deci rezolvarea problemei, este teorema de demonstrat.
Algoritm: Respingerea prin rezolutie in logica cu predicate de ordinul I
1. Converteste setul de axiome A in forma clauzala si obtine multimea de clauze S0
2. Neaga teorema de demonstrat, transforma teorema negata in forma clauzala si adauga rezultatul obtinut la S0

3. repeta
3.1. Selecteaza o pereche de clauze C1, C2
3.2. Fie literalii si
3.3. Aplica unificarea si calculeaza
3.4. daca atunci
3.4.1. Determina
3.4.2. daca atunci pina s-a obtinut clauza vida ( ) sau nu mai exista nici o pereche de clauze care rezolva sau o cantitate predefinita de efort a fost epuizata
4. daca s-a obtinut clauza vida atunci teorema este adevarata (este demonstrata)
5. altfel
5.1. daca nu mai exista nici o pereche de clauze care rezolva atunci teorema este falsa
5.2. altfel nu se poate spune nimic despre adevarul teoremei sfirsit.
Observatii:
* In cazul in care s-a obtinut clauza vida, metoda respingerii prin rezolutie garanteaza faptul ca teorema este adevarata, deci este demonstrabila pe baza setului de axiome A.
* Reciproc, daca teorema este adevarata, se poate obtine clauza vida dupa un numar finit de executii a pasului 3, cu conditia ca strategia de rezolutie sa fie completa.
* Conditia de oprire a ciclului, "o cantitate predefinita de efort a fost epuizata", absenta in cazul algoritmului respingerii prin rezolutie in calculul cu propozitii, a fost introdusa in acest caz deoarece metoda demonstrarii teoremelor prin respingere rezolutiva este semidecidabila in logica cu predicate de ordinul I. In cazul in care concluzia T de demonstrat este falsa, deci nu este teorema, este posibil sa se ajunga in situatia in care, daca avem noroc, "nu mai exista nici o pereche de clauze care rezolva". Atunci se poate concluziona ca teorema este falsa. Dar este de asemenea posibil ca pasul 3 sa se execute la infinit daca T nu este teorema. Din acest motiv se introduce o cantitate predefinita de efort (resurse de timp sau spatiu) la epuizarea careia algoritmul se opreste. In acest caz s-ar putea ca teorema sa fie adevarata, dar efortul predefinit impus sa fie prea mic, sau se poate ca T sa nu fie teorema. Rezulta deci ca nu se poate spune nimic despre adevarul teoremei.
Se prezinta in continuare doua exemple de demonstrare a teoremelor utilizind metoda respingerii prin rezolutie. Primul exemplu considera din nou problema delfinilor inteligenti, prezentata in Sectiunea 3.2.2, exprimata prin urmatoarele trei enunturi:
(1) Oricine poate citi este literat.
(2) Delfinii nu sint literati.
(2) Anumiti delfini sint inteligenti. si cere sa se demonstreze ca
(4) Exista inteligenti care nu pot citi.
Se exprima setul de propozitii in logica cu predicate si se obtin urmatoarele trei axiome si concuzia de demonstrat:
(A1)
(A2)
(A3)
(C)
Se transforma axiomele in forma clauzala si se obtine:
(C1)
(C2)
(C3) Delfin(a)
(C3') Inteligent(a)
Se neaga teorema, obtinindu-se si se transforma teorma negata in forma clauzala, rezultatul adaugindu-se la multimea de clauze de mai sus.
(C4)
Deducerea clauzei vide, deci demonstratia teoremei, este prezentata in Figura 3.6.

Figura 3.6 Respingerea prin rezolutie in logica cu predicate de ordinul I
Se observa ca o demonstratie prin respingere prin rezolutie poate fi reprezentata convenabil printr-un arbore de respingere sau arbore de deductie care are ca radacina clauza vida. In acest arbore trebuie marcate clauzele care rezolva si puse in evidenta substitutiile efectuate pentru unificarea literalilor complementari.
Se considera in continuare urmatoarea problema de transport.
(1) Daca orasul x este legat de orasul y prin drumul z si pot circula biciclete pe drumul z, atunci se poate merge de la x la y.
(2) Daca orasul x este legat de orasul y prin drumul z, atunci orasul y este legat de orasul x prin drumul z.
(3) Daca se poate merge de la x la y si de la y la z atunci se poate merge de la x la z.
(4) Orasul a este legat de orasul b prin drumul d1.
(5) Orasul b este legat de orasul c prin drumul d2.
(6) Orasul a este legat de orasul c prin drumul d3.
(7) Pot circula biciclete pe d1.
(8) Pot circula biciclete pe d2.
Se cere sa se demonstreze ca se poate merge de la orasul a la orasul c.
Exprimarea in logica cu predicate a problemei date conduce la urmatoarea multime de formule, din care primele opt sint axiomele problemei, ultima fiind concluzia de demonstrat.
(A1)
(A2)
(A3)
(A4)
(A5)
(A6)
(A7)
(A8)
(C)
Se transforma axiomele in forma clauzala, se neaga teorema si se transforma teorema negata in forma clauzala, obtinindu-se urmatoarea multime de clauze:
(C1)
(C2)
(C3)
(C4)
(C5)
(C6)
(C7)
(C8)
(C9)
Demonstratia teoremei este prezentata in Figura 3.7.

Figura 3.7 Demonstrarea teoremei Merg(a,c) utilizind rezolutia
Se observa din acest exemplu ca, in fiecare punct, exista numeroase perechi de clauze care pot rezolva. Este rolul strategiei de control de a elimina, partial sau total, aceasta ambiguitate.
3.3.5 Strategii rezolutive
Algoritmul respingerii prin rezolutie in logica cu predicate de ordinul I prezentat in sectiunea anterioara, ca si cel din calculul propozitional de altfel, contine o etapa nedeterminista, pasul 3.1. In acest pas al algoritmului nu se spune nimic despre modul in care trebuie selectate cele doua clauze care rezolva. Este rolul strategiei rezolutive de a transforma acest pas intr-un pas determinist. Deoarece rezolutia este o metoda de inferenta, modul de aplicare repetata a rezolutiei pentru a rezolva problema este stabilit de strategia de control utilizata. Strategia rezolutiva trebuie sa dea criteriile de selectie a perechilor de clauze care rezolva, in cazul in care exista mai multe astfel de clauze. Eventual, strategia de control poate sa stabileasca si care literali din cele doua clauze care rezolva sint selectati pentru a produce rezolventul.
Se reaminteste faptul ca o strategie rezolutiva este completa daca, prin aplicarea ei, se poate demonstra teorema (se produce clauza vida) ori de cite ori formula de demonstrat este teorema.
Cele mai importante strategii rezolutive sint prezentate in continuare.
* Strategia dezvoltarii pe latime sau pe nivel, numita si metoda saturarii nivelului, are la baza urmatoarea idee: se calculeaza toti rezolventii posibili de pe un nivel, acesti rezolventi se adauga la acest nivel pentru a forma nivelul urmator si se reia procesul pentru nivelul urmator. Aceasta strategie este o strategie completa dar prezinta dezavantajul unui consum mare de resurse spatiu si timp.
* Strategia multimii suport are la baza urmatoarea idee: se imparte multimea de clauze in doua submultimi de clauze S1 si S2, de preferinta astfel incit, pentru orice interpretare I, clauzele din S1 sint adevarate in I, iar clauzele din S2 sint false in I. Se aplica rezolutia numai intre perechi de rezolventi din multimi diferite, deci si . Aceasta strategie este completa si poate fi asimilata cu o cautare pe nivel in spatiul starilor.
* Strategia rezolutiei semantice combina strategia multimii suport cu rezolvarea in simultan a mai multor clauze. In acest fel se incearca eliminarea clauzelor inutile prin rezolvarea simultana a unui grup de clauze, ordonarea predicatelor si ordonarea clauzelor. Strategia rezolutiei semantice este o strategie completa.
* Strategia rezolutiei liniare are la baza urmatoarea idee: orice rezolvent Ci obtinut in rezolutie este utilizat ca unul din cei doi rezolventi pe baza carora se obtine urmatorul rezolvent . Aceasta strategie este completa si, in plus, simplu si eficient de implementat.
* Strategia rezolutiei de intrare liniara este un caz particular al strategiei rezolutiei liniare in care una din clauzele care rezolva apartine intotdeauna setului initial de axiome. Este o strategie foarte eficienta dar nu este completa. Aceasta strategie de control sta la baza functionarii mecanismului de demonstrare a teoremelor din limbajul Prolog, asa cum se va explica in detaliu in Capitolul 11.
* Strategia rezolutiei unitare, numita si strategia preferintei unitare, este un alt caz particular al strategiei rezolutiei liniare, in care una din clauzele ce rezolva este o clauza unitara, deci o clauza care contine un singur literal. Aceasta strategie nu este completa.
Cele doua exemple de demonstrare a teoremelor prezentate in sectiunea anterioara, i.e. problema delfinilor inteligenti si problema de transport, au folosit o strategie rezolutiva liniara, in particular rezolutia de intrare liniara. In acelasi timp se poate considera ca s-a aplicat si o strategie a multimii suport in care multimea de clauze s-a impartit in multimea S1 care contine toate clauzele provenite din setul initial de axiome si multimea S2 care contine clauzele provenite din negarea teoremei de demonstrat.
Aplicind strategia dezvoltarii pe latime in cazul problemei delfinilor inteligenti se vor obtine pentru primele doua nivele rezolventii (distincti) prezentati in Figura 3.8. Fiind o strategie de cautare pe nivel, strategia dezvoltarii pe latime, daca poate deduce clauza vida, va gasi automat si drumul cel mai scurt spre solutie. De multe ori, in demonstrarea teoremelor intereseaza mai putin drumul cel mai scurt spre clauza vida si mai mult numarul de rezolventi generati. Din aceasta cauza strategii care genereaza mai putini rezolventi, cum ar fi strategiile liniare, sint preferate.

Figura 3.8 Strategia dezvoltarii pe latime
Strategiile prezentate ofera criterii de selectie a clauzelor utilizate in producerea rezolventului, deci o modalitate sistematica de generare a rezolventilor, dar de multe ori, nu indica selectia unei perechi unice de clauze dintre clauzele ce pot rezolva la un moment dat. In plus, nu se spune nimic despre perechea de literali complementari care trebuie selectata in cazul in care doua clauze pot rezolva in mai multe feluri. Pentru rezolvarea acestor probleme si construirea unui program performant de demonstrare a teoremelor trebuie utilizate si criterii euristice aChang,Lee,1973i.
3.3.6 Obtinerea raspunsurilor utilizind respingerea prin rezolutii
Tehnica demonstrarii teoremelor poate fi utilizata si pentru a obtine raspunsuri la intrebari despre universul problemei descris de axiome aNilsson,1980i. Multe teoreme sint reprezentate prin formule care contin variabile cuantificate existential, de forma . In aceste cazuri este de dorit sa se poata raspunda la intrebari de tipul "Ce valoare are x daca formula este adevarata?" Pentru a putea raspunde la aceste intrebari este nevoie de o metoda de demonstratie constructiva. Aceasta metoda se obtine printr-o extindere a metodei respingerii rezolutiei.
Se considera urmatorul enunt: "Daca Grivei merge oriunde merge Mihai si Mihai este la scoala, unde este Grivei?". Pentru a rezolva aceasta problema, se exprima cunostintele in modelul logic
(A1)
(A2)
(C)
Forma clauzala echivalenta este:
(C1)
(C2)
(C3)
Demonstratia teoremei este banala, arborele de deductie fiind prezentat in Figura 3.9(a). Pentru a putea obtine insa si o instanta a variabilei y, instanta care va indica unde este Grivei, se adauga clauzei care a rezultat din negarea teoremei chiar negarea ei, astfel incit