Inteligen artificial6. Metode de inferen n logica propoziional i predicativFlorin LeonUniversitatea Tehnic Gh. Asachi Iai Facultatea de Automatic i Calculatoare http://florinleon.byethost24.com/curs_ia.htmFlorin Leon, Inteligenta artificiala, http://florinleon.byethost24.com/curs_ia.htm

Metode de inferen n logica propoziional i predicativ1. Logica propoziional 1.1. Modus Ponens 1.2. Modus Tollens 1.3. Rezoluia propoziional 2. Logica predicatelor 2.1. Raionamentul nainte 2.2. Raionamentul napoi 2.3. Rezoluia predicativ

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

2

Metode de inferen n logica propoziional i predicativ1. Logica propoziional 1.1. Modus Ponens 1.2. Modus Tollens 1.3. Rezoluia propoziional 2. Logica predicatelor 2.1. Raionamentul nainte 2.2. Raionamentul napoi 2.3. Rezoluia predicativ

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

3

Logica i limbajul natural

n limbajul natural, multe propoziii sunt ambigue i pentru ele exist mai multe moduri de reprezentare

Reprezentrile simple sunt preferabile, ns pot face imposibile unele tipuri de raionament

Logica aduce formalizarea codrii cunotinelor

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

4

Logica propoziional

Formalismul logic permite derivarea de noi cunotine din cunotine deja existente, prin deducie logico-matematic sau inferen O propoziie e adevrat dac deriv din propoziii cunoscute ca adevrate Domeniu strns legat de demonstrarea automat a teoremelor i inteligena artificial

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

5

Formule bine formate

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

6

Propoziie

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

7

Deducie. Teorem

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

8

Tautologie

Demonstrare semantic9

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

Teorema de completitudine a calculului propoziional

n calculul propoziional mulimea teoremelor coincide cu mulimea tautologiilor Noiunea de teorem este de natur sintactic, n timp ce noiunea de tautologie are o natur semantic Teorema subliniaz faptul c aceste noiuni sunt echivalente

Orice tautologie poate fi dedus pe cale sintactic Orice propoziie adevrat n orice caz este o teorem i poate fi folosit ulterior pentru inferene10

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

Metode de inferen n logica propoziional i predicativ1. Logica propoziional 1.1. Modus Ponens 1.2. Modus Tollens 1.3. Rezoluia propoziional2. Logica predicatelor 2.1. Raionamentul nainte 2.2. Raionamentul napoi 2.3. Rezoluia predicativ

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

11

Metode de inferen: MP, MT

Modus ponendo ponens (prescurtat Modus Ponens)

Modus tollendo tollens (prescurtat Modus Tollens)

Premise: P Q i P Concluzie: Q Lat. ponere = a pune, a afirma Modalitatea care afirmnd [P] afirm [Q] Afirmarea antecedentuluiPremise: P Q i non Q Concluzie: non P Lat. tollere = a lua, a nega Modalitatea care negnd [Q] neag [P] Negarea consecventului

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

12

Metode de inferen n logica propoziional i predicativ1. Logica propoziional 1.1. Modus Ponens 1.2. Modus Tollens 1.3. Rezoluia propoziional2. Logica predicatelor 2.1. Raionamentul nainte 2.2. Raionamentul napoi 2.3. Rezoluia predicativ

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

13

Reguli de transformare a formulelor (I)

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

14

Reguli de transformare a formulelor (II)

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

15

Forma normal conjunctiv

engl. Conjunctive Normal Form O conjuncie de disjuncii

un I de SAU-uri

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

16

Transformarea n FNC

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

17

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

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

18

Transformarea eitin (II)

Evit expandarea exponenial

Rezultatul este proporional 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 rezoluie

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

19

Rezoluia propoziional (I)

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

20

Rezoluia propoziional (II)

Ideea de baz a acestei forme de raionament este deducerea din dou propoziii, n care unul din termeni apare cu valori de adevr contrare, a unei concluzii din care este eliminat termenul respectiv

Se bazeaz pe reducere la absurdFlorin Leon, Inteligenta artificiala, http://florinleon.byethost24.com/curs_ia.htm

21

Demonstrarea semanticTermenii nu sunt echivaleni, dar implicaia este adevrat

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

22

Exemplul 1

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

23

FNC

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

24

Procesul de rezoluie

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

25

Exemplul 2

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

26

FNC

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

27

Rezoluia

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

28

Rezoluia

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

29

Rezoluia

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

30

Metode de inferen n logica propoziional i predicativ1. Logica propoziional 1.1. Modus Ponens 1.2. Modus Tollens 1.3. Rezoluia propoziional 2. Logica predicatelor 2.1. Raionamentul nainte 2.2. Raionamentul napoi 2.3. Rezoluia predicativ

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

31

Logica predicatelor

Formulele depind de variabile

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

32

Exemple

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

33

Reducerea la inferena propoziional

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

34

Reducerea la inferena propoziional

Orice formul predicativ de ordinul I poate fi propoziionalizat Mulimea de termeni ar putea fi infinit

Father(Father(Father(John)))Dac o propoziie este implicat de o baz de cunotine de ordin I, demonstraia implic o submulime finit a bazei de cunotine propoziionalizate Mai nti simbolurile constante: Richard, John Apoi la adncimea 1: Father(Richard), Father(John) .a.m.d. pn cnd demonstraia reuete

Teorema lui Herbrand

Ordinul termenilor crete iterativ n adncime

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

35

Forma normal conjunctiv

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

36

Exemplu: transformarea n FNC

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

37

Transformarea n FNC

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

38

Transformarea n FNC

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

39

Transformarea n FNC

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

40

Transformarea n FNC

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

41

Substituia

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

42

Unificarea

Unificarea returneaz o mulime de substituii Pot exista mai multe unificri posibile Pentru orice pereche unificabil de expresii exist cel mai general unificator (unic)Florin Leon, Inteligenta artificiala, http://florinleon.byethost24.com/curs_ia.htm

43

Metode de inferen n logica propoziional i predicativ1. Logica propoziional 1.1. Modus Ponens 1.2. Modus Tollens 1.3. Rezoluia propoziional 2. Logica predicatelor 2.1. Raionamentul nainte 2.2. Raionamentul napoi