Bài giảng Trí tuệ nhân tạo - Chứng minh trong logic mệnh đề

Nội dung text: Bài giảng Trí tuệ nhân tạo - Chứng minh trong logic mệnh đề

1. TRÍ TU NHÂN TO Chng minh trong Logic Mnh đ
2. Ni dung trình bày 2
   Hp gii mnh đ
   Thut tốn hp gii
   Thut tốn Davis Putman
   Suy din tin
   Suy din lùi
   ðánh giá suy din tin và suy din lùi
3. Hp gii Mnh đ 3
   Hp gii mnh đ là lut ca suy din
   Ch s dng mt mình hp gii mnh đ (khơng cn s dng các lut khác) cĩ th xây dng mt chương trình chng minh lý thuyt đúng và đ cho tt c Logic Mnh đ
   Ch hot đng vi biu din dng hi chun (Conjunctive Normal Form)
4. Dng Hi Chun CNF 4
   Cơng thc Dng hi Chun (CNF) cĩ dng: (A ∨ B ∨ ¬C) ∧ (B ∨D) ∧ (¬ A) ∧ (B ∨C) • (A ∨ B ∨ ¬C) là mt clause • A, B, ¬C là các literal, mà mi cái là mt bin hay ph đnh ca mt bin • Mi clause phi đưc tho và cĩ th đưc tho theo nhiu cách • Mi câu trong logic mnh đ đu cĩ th vit dưi dng CNF
5. Bin đi thành CNF 5
   Loi b các du mũi tên ( ⇐, ⇔, ⇒) bng đnh nghĩa
   ðưa du ph đnh vào dùng lut De Morgan ¬(A ∨ B) ≡ ¬A ∧ ¬ B ¬(A ∧ B) ≡ ¬A ∨ ¬ B
   Phân phi or vào and A ∨ (B ∧ C) ≡ (A ∨ B) ∧ (A ∨ C)
   Mi câu đu cĩ th đưc bin đi thành CNF, nhưng kích thưc cĩ th tăng lên theo lu tha.
6. Ví d Bin đi CNF 6 (A ∨ B) ⇒ (C ⇒ D) 1. Loi b du mũi tên ¬(A ∨ B) ∨ (¬C ∨ D) 2. ðưa ph đnh vào (¬ A ∧ ¬ B) ∨ (¬C ∨ D) 3. Phân phi (¬ A ∨ ¬C ∨ D) ∧ (¬ B ∨ ¬C ∨ D)
7. Hp gii mnh đ 7
   Lut hp gii: α ∨ ¬β β ∨ γ α ∨ γ
   Hp gii Robison – chng minh phn chng: Mun chng minh KB ⇒ α là đúng, ta chng minh điu ngưc li KB ∧ ¬α là sai
   Hp gii là đúng và đ cho logic mnh đ
8. Thut tốn Hp gii (Robinson) 8 1. Bin đi tt c các câu thành dng CNF 2. Ly ph đnh kt lun, đưa vào KB 3. Lp 1. Nu trong KB cĩ cha hai mnh đ ph đnh nhau (p và ¬p) thì tr v true 2. Nu cĩ hai mnh đ cha các literal ph đnh nhau thì áp dng hp gii. 3. Lp cho đn khi khơng th áp dng tip lut hp gii. 4. Tr v false
9. Ví d Hp gii Mnh đ 9 Chng minh R Bưc Cơngthc Suydn 1 P ∨ Q 1 P ∨ Q Cho trưc 2 P ⇒ R 2 ¬P ∨ R Cho trưc 3 Q ⇒ R 3 ¬Q ∨ R Cho trưc
10. Ví d Hp gii Mnh đ 10 Chng minh R Bưc Cơngthc Suydn 1 P ∨ Q 1 P ∨ Q Cho trưc 2 P ⇒ R 2 ¬P ∨ R Cho trưc 3 Q ⇒ R 3 ¬Q ∨ R Cho trưc 4 ¬R Ph đnh kt lun
11. Ví d Hp gii Mnh đ 11 Chng minh R Bưc Cơngthc Suydn 1 P ∨ Q 1 P ∨ Q Cho trưc 2 P ⇒ R 2 ¬P ∨ R Cho trưc 3 Q ⇒ R 3 ¬Q ∨ R Cho trưc 4 ¬R Ph đnh kt lun 5 Q ∨ R 1, 2 6 ¬P 2, 4 7 ¬Q 3, 4 8 R 5, 7 9 · 4, 8
12. Th tc Davis Putman 12
    Bin đi tt c các câu thành dng CNF
    Ly ph đnh kt lun, đưa vào KB
    Lp
    Nu trong KB cĩ cha hai mnh đ mâu thun (ví d: P và ¬P) thì tr v true
    S dng mt bin mnh đ đ hp gii:  Ly tt c các câu cha bin mnh đ đưc chn.  Áp dng lut hp gii lên mi cp câu cha khng đnh và ph đnh ca bin mnh đ.  Vit các câu kt qu mi và xố các câu đã s dng.
    Lp cho đn khi khơng cịn bin mnh đ nào cĩ th hp gii đưc.
    Tr v false
13. Suy din Tin và Lùi 13
    Logic dng Horn (hn ch): KB = ni lin ca các mnh đ Horn Mnh đ Horn =  bin mnh đ, hay  (ni ri các bin) ⇒ bin Ví d: C ∧ (B ⇒ A) ∧ (C ∧ D ⇒ D)
    Tam đon lun (cho dng Horn): đ đi vi KB Horn α⇒β , α β
    Cĩ th đưc s dng vi suy din tin và suy din lùi
    Các thut tốn này rt t nhiên và chy vi thi gian tuyn tính
14. Suy din tin 14
    Ý tưng: kích hot tt c các lut mà tin đ ca nĩ tho trong KB,
    b sung kt lun vào KB, lp cho đn khi tìm thy kt lun
15. Ví d Suy din Tin 15
16. Ví d Suy din Tin 16
17. Ví d Suy din Tin 17
18. Ví d Suy din Tin 18
19. Ví d Suy din Tin 19
20. Ví d Suy din Tin 20
21. Ví d Suy din Tin 21
22. Ví d Suy din Tin 22
23. Suy din Lùi (Back Chaining) 23 Ý tưng: quay lùi t câu hi q: đ chng minh q bng BC, kim tra xem q đã bit chưa, hay chng minh bng cách suy din lùi tt c tin đ ca mt lut nào đĩ rút ra q Tránh loop: kim tra xem mt mc tiêu ph đã nm trong ngăn xp mc tiêu hay chưa Tránh lp li cơng vic: kim tra xem mt mc tiêu ph mi 1. đã đưc chng minh đúng, hay 2. đã tht bi
24. Ví d Suy din Lùi 24
25. Ví d Suy din Lùi 25 Q? P ⇒ Q P?
26. Ví d Suy din Lùi 26 Q? P ⇒ Q P? L ∧ M ⇒ P L?
27. Ví d Suy din Lùi 27 Q? P ⇒ Q P? L ∧ M ⇒ P L? A ∧ B ⇒ L A? 
28. Ví d Suy din Lùi 28 Q? P ⇒ Q P? L ∧ M ⇒ P L? A ∧ B ⇒ L A?  B? 
29. Ví d Suy din Lùi 29 Q? P ⇒ Q P? L ∧ M ⇒ P L?  A?  B? 
30. Ví d Suy din Lùi 30 Q? P ⇒ Q P? L ∧ M ⇒ P L?  A?  B?  M? L ∧ B ⇒ M L? B?
31. Ví d Suy din Lùi 31 Q? P ⇒ Q P? L ∧ M ⇒ P L?  A?  B?  M?  L?  B? 
32. Ví d Suy din Lùi 32 Q? P ⇒ Q P?  L?  A?  B?  M?  L?  B? 
33. Ví d Suy din Lùi 33 Q?  P?  L?  A?  B?  M?  L?  B? 
34. Suy din Tin (FC) và Lùi (BC) 34
    FC là hưng d liu , x lý t đng, khơng ý thc,
    vd, nhn dng mu, quyt đnh l trình
    Cĩ th làm nhiu vic khơng liên quan đn đích
    BC là hưng đích , thích hp vi gii quyt vn đ,
    ð phc tp ca BC cĩ th ít hơn nhiu so vi tuyn tính theo kích thưc ca KB
35. ðiu cn nm 35
    Hiu đưc ý tưng, cơ s ca phép hp gii và vic chng minh dùng thut tốn hp gii
    Nm đưc các dng suy din áp dng đưc trên logic mnh đ
    Làm đưc các bài tp liên quan đn logic mnh đ
36. Thc mc 36