44090454 Inteligenta Artificial A Inferenta in Logica Propozitionala Si Predicativa

transcript

Inteligenţă artificială

6. Metode de inferenţă în logica propoziţională şi predicativă Florin Leon

Universitatea Tehnică „Gh. Asachi” Iaşi Facultatea de Automatică şi Calculatoare

http://florinleon.byethost24.com/curs_ia.htm

Florin Leon, Inteligenta artificiala, http://florinleon.byethost24.com/curs_ia.htm

Metode de inferenţă în logica propoziţională şi predicativă

1. Logica propoziţională

1.1. Modus Ponens

1.2. Modus Tollens

1.3. Rezoluţia propoziţională

2. Logica predicatelor

2.1. Raţionamentul înainte

2.2. Raţionamentul înapoi

2.3. Rezoluţia predicativă

1.1. Modus Ponens

1.2. Modus Tollens

Logica şi limbajul natural

În limbajul natural, multe propoziţii sunt ambigue şi pentru ele există mai multe moduri de reprezentare

Reprezentările simple sunt preferabile, însă pot face imposibile unele tipuri de raţionament

Logica aduce formalizarea codării cunoştinţelor

Logica propoziţională

Formalismul logic permite derivarea de noi cunoştinţe din cunoştinţe deja existente, prin deducţie logico-matematică sau inferenţă

O propoziţie e adevărată dacă derivă din propoziţii cunoscute ca adevărate

Domeniu strâns legat de demonstrarea automată a teoremelor şi inteligenţa artificială

Formule bine formate

Propoziţie

Deducţie. Teoremă

Tautologie

Demonstrare semantică

Teorema de completitudine a calculului propoziţional

În calculul propoziţional mulţimea teoremelor coincide cu mulţimea tautologiilor

Noţiunea de teoremă este de natură sintactică, în

timp ce noţiunea de tautologie are o natură semantică

Teorema subliniază faptul că aceste noţiuni sunt echivalente

Orice tautologie poate fi dedusă pe cale sintactică

Orice propoziţie adevărată în orice caz este o teoremă şi poate fi folosită ulterior pentru inferenţe

1.1. Modus Ponens

1.2. Modus Tollens

Metode de inferenţă: MP, MT

Modus ponendo ponens (prescurtat Modus Ponens) Premise: P → Q şi P Concluzie: Q Lat. „ponere” = a pune, a afirma Modalitatea care afirmând [P] afirmă [Q] Afirmarea antecedentului

Modus tollendo tollens (prescurtat Modus Tollens) Premise: P → Q şi non Q

Concluzie: non P Lat. „tollere” = a lua, a nega Modalitatea care negând [Q] neagă [P] Negarea consecventului

1.1. Modus Ponens

1.2. Modus Tollens

Reguli de transformare a formulelor (I)

Reguli de transformare a formulelor (II)

Forma normal conjunctivă

engl. “Conjunctive Normal Form”

O conjuncţie de disjuncţii

un ŞI de SAU-uri

Transformarea în FNC

Transformarea Ţeitin (I)

G.S. Tseitin - On the complexity of derivation in propositional calculus, Studies in Constructive Mathematics and Mathematical Logic, part 2, pp. 115-125, 1968

Transformarea Ţeitin (II)

Evită expandarea exponenţială

Rezultatul este proporţional cu dimensiunea formulei originare

Noua formulă poate să nu fie echivalentă cu formula originară

De exemplu dacă xi = fals

Formula originară este (ne)satisfiabilă dacă şi numai dacă formula nouă este (ne)satisfiabilă

Proprietate necesară pentru procesul de rezoluţie

19 Florin Leon, Inteligenta artificiala, http://florinleon.byethost24.com/curs_ia.htm

Rezoluţia propoziţională (I)

Rezoluţia propoziţională (II)

Ideea de bază a acestei forme de raţionament este deducerea din două propoziţii, în care unul din termeni apare cu

valori de adevăr contrare, a unei concluzii din care este eliminat termenul respectiv

Se bazează pe reducere la absurd

Demonstrarea semantică

Termenii nu sunt echivalenţi, dar implicaţia este adevărată

Exemplul 1

Procesul de rezoluţie

Exemplul 2

Rezoluţia

1.1. Modus Ponens

1.2. Modus Tollens

Logica predicatelor

Formulele depind de variabile

Exemple

Reducerea la inferenţa propoziţională

Orice formulă predicativă de ordinul I poate fi propoziţionalizată

Mulţimea de termeni ar putea fi infinită

Father(Father(Father(John)))

Teorema lui Herbrand

Dacă o propoziţie este implicată de o bază de cunoştinţe de ordin I, demonstraţia implică o submulţime finită a bazei de cunoştinţe propoziţionalizate

Ordinul termenilor creşte iterativ în adâncime

Mai întâi simbolurile constante: Richard, John

Apoi la adâncimea 1: Father(Richard), Father(John)

Ş.a.m.d. până când demonstraţia reuşeşte

Forma normal conjunctivă

Exemplu: transformarea în FNC

Substituţia

Unificarea

Unificarea returnează o mulţime de substituţii

Pot exista mai multe unificări posibile

Pentru orice pereche unificabilă de expresii există cel mai general unificator (unic)

1.1. Modus Ponens

1.2. Modus Tollens

Raţionamentul înainte

Clauză Horn definită

Disjuncţie în FNC cu un singur termen pozitiv

Formula este echivalentă cu o implicaţie

Procedură de căutare

Descoperirea unei căi în spaţiul problemei care conduce de la starea iniţială la starea scop

Când căutarea porneşte din starea iniţială către starea scop, avem de-a face cu un raţionament înainte

Raţionamentul înainte

Dacă procesul de căutare este modelat printr-un sistem de producţie, rezolvarea problemei apare drept construirea unui arbore al operaţiilor posibile

Rădăcina arborelui este starea iniţială

Nivelul următor al arborelui se completează prin determinarea tuturor regulilor a căror parte stângă se potriveşte nodului rădăcină

Noile noduri se creează prin intermediul părţii drepte a regulilor considerate

Procedura se repetă pentru fiecare nod, până când se generează o configuraţie identică stării scop

Exemplul 1

Problema cănilor cu apă

Avem la dispoziţie 2 căni de capacităţi diferite A şi B

Scopul este ca în cana A să rămână o cantitate specificată de apă prin aplicarea a 6 operaţii posibile:

umple cana A (↑A)

umple cana B (↑B)

toarnă apa din cana A în cana B (A→B)

toarnă apa din cana B în cana A (B→A)

varsă cana A (↓A)

varsă cana B (↓B)

Exemplul 1

În figură se prezintă arborele rezultat prin aplicarea celor 6 operaţii unei probleme concrete: cana A are capacitatea de 4l, cana B are capacitatea de 3l iar în final în cana A

trebuie să se obţină un rest de 2l

Exemplul 1

Datorită complexităţii sale, numai primul nivel a fost completat, în rest urmărindu-se drumul către soluţia optimă (calea cea mai scurtă către scop)

Se remarcă faptul că nu există o soluţie optimă unică, ea putând fi atinsă pe două căi diferite

Exemplul 2

“The law says that it is a crime for an American to sell weapons to hostile nations. The country Nono, an enemy of America, has some missiles, and all of its missiles were sold to it by Colonel West, who is American.”

Trebuie demonstrat (scop): Col. West is a criminal

Exemplul 2

... it is a crime for an American to sell weapons to hostile nations: 1. American(x) Weapon(y) Sells(x,y,z) Hostile(z) Criminal(x)

Nono … has some missiles: x Owns(Nono,x) Missile(x): 2. Owns(Nono,M1) and Missile(M1)

… all of its missiles were sold to it by Colonel West 3. Missile(x) Owns(Nono,x) Sells(West,x,Nono)

Missiles are weapons: 4. Missile(x) Weapon(x)

An enemy of America counts as “hostile”: 5. Enemy(x,America) Hostile(x)

West, who is American … 6. American(West)

The country Nono, an enemy of America … 7. Enemy(Nono,America)

M1: funcţie Skolem, tratată ca un simbol

Exemplul 2

6 2 2 7

Exemplul 2

Probleme (I)

Potriviri redundante de reguli

Raţionament înainte incremental

Fiecare fapt nou dedus în iteraţia t trebuie derivat din cel puţin un fapt nou dedus în iteraţia t-1

Algoritmul Rete (Clips)

Probleme (II)

Fapte irelevante

Mulţime magică: folosirea informaţiilor din scop

Exemplu: scopul este Criminal(West)

Regula care are drept concluzie acest predicat: American(x) Weapon(y) Sells(x,y,z) Hostile(z) Criminal(x)

este rescrisă: Magic(x) American(x) Weapon(y) Sells(x,y,z) Hostile(z) Criminal(x)

iar faptul Magic(West) este adăugat în baza de cunoştinţe

Acum în BC pot exista milioane de americani, dar inferenţa se poate face numai cu West

1.1. Modus Ponens

1.2. Modus Tollens

Raţionamentul înapoi

Spaţiul problemei poate fi explorat şi în direcţie inversă faţă de cea urmată în cazul anterior

Când căutarea porneşte din starea scop către starea iniţială, avem de-a face cu un raţionament înapoi

Aici rădăcina arborelui este starea scop

Nivelul următor al arborelui se completează prin determinarea tuturor regulilor a căror parte dreaptă se potriveşte nodului rădăcină

Noile noduri se creează prin intermediul părţii stângi a regulilor considerate

Procedura se repetă pentru fiecare nod, până când se generează o configuraţie identică stării iniţiale

Exemplul 1

Pentru problema cănilor cu apă, trebuie să facem unele precizări suplimentare pentru a o rezolva prin raţionament înapoi

Când problema este rezolvată prin raţionament înainte, în starea scop în cana B se poate găsi orice cantitate de apă

Când problema este rezolvată prin raţionament înapoi, starea scop trebuie fixată pentru că de aici va începe raţionamentul

Exemplul 1

Să presupunem că dorim restul de 2l în cana A şi 0l în cana B

Nu toate cele 6 operaţii se vor putea aplica pentru orice nod

Vor exista constrângeri, de exemplu, dacă la un anumit moment în cana A sunt 0l, este

imposibilă aplicarea primei operaţii (umple A)

Ar însemna ca după umplerea cănii, în ea să nu existe apă, ceea ce este absurd

Exemplul 2

Comparaţie

Raţionamentul înainte Este dirijat de date (engl. “data driven”)

Recunoaşterea obiectelor, decizii de rutină

Poate determina încercarea multor acţiuni irelevante pentru atingerea scopului

Raţionamentul înapoi Este dirijat de scop (engl. “goal driven”)

Unde sunt cheile de la maşină, cum pot găsi un serviciu bun Prolog

Determină rezolvări cu o complexitate mult mai mică decât raţionamentul înainte, dar are mai multe constrângeri

1.1. Modus Ponens

1.2. Modus Tollens

Rezoluţia predicativă

Exemplul 1

Se poate constata că a treia ipoteză nu este necesară pentru demonstrarea concluziei

Dacă pe al treilea nivel al arborelui am fi utilizat-o, nu am fi ajuns la o contradicţie logică, ci am fi demonstrat că Geta nu este tatăl lui Tudor

În general, dacă există mai multe posibilităţi de substituţie şi unele încercări nu dau rezultate, este nevoie de o căutare de tip backtracking pentru găsirea soluţiei

Exemplul 2

Exemplul 3

Exemplul 3: FNC

Exemplul 3: Rezoluţia

Exemplul 4

Exemplul 4: FNC (I)

Exemplul 4: FNC (II)

Exemplul 4: FNC (III)

Exemplul 4: Rezoluţia

Demonstrarea teoremelor în logica de ordinul întâi

Turing, Church: problema demonstrării teoremelor în logica de ordinul întâi este semidecidabilă Se poate afla dacă o propoziţie se poate

demonstra

Nu se poate afla dacă o propoziţie nu se poate demonstra Algoritmul de rezoluţie poate rula la infinit

Problemă echivalentă cu determinarea opririi unei maşini Turing

Utilizări practice

Demonstratoarele automate de teoreme sunt folosite cu succes pentru:

Automatizarea demonstraţiilor

Algebra Robbins

Prima demonstraţie formală riguroasă pentru teorema incompletitudinii a lui Gödel

Verificarea şi sinteza componentelor software şi hardware

Algoritmul de criptare RSA

Algoritmul de string-matching Boyer-Moore

Verificare CPU

Proiectarea circuitelor

Remote Agent (NASA Deep Space 1)

84 Florin Leon, Inteligenta artificiala, http://florinleon.byethost24.com/curs_ia.htm

Concluzii

Procesul de rezoluţie este o modalitate convenabilă de a deduce noi adevăruri din premise multiple

Un alt avantaj al său este posibilitatea aplicării legilor logice, care au fost studiate intens

Metoda beneficiază de o formalizare strictă, care asigură consistenţa deducţiilor, nelăsând prea mult loc interpretărilor subiective

Există şi unele limitări; dacă există o demonstraţie, metoda rezoluţiei garantează găsirea ei, însă dacă nu există o astfel de demonstraţie, algoritmul poate intra într-o buclă infinită

În general, este imposibil de stabilit dacă şi când se va întâmpla acest lucru

44090454 Inteligenta Artificial A Inferenta in Logica Propozitionala Si Predicativa

Documents