Bài giảng Trí tuệ nhân tạo - Logic vị từ

Nội dung text: Bài giảng Trí tuệ nhân tạo - Logic vị từ

1. TRÍ TU NHÂN TO Logic v t
2. Ni dung trình bày 2
   Logic bc nht (First Order Logic)
   Cú pháp và ng nghĩa
   Các lưng t
   Hp gii vi logic v t
   Phép th
   Thut gii đng nht
3. Ti sao s dng logic bc nht? 3
   Logic mnh đ ch x lý trên các s kin , là các khng đnh cĩ giá tr hoc đúng hoc sai.
   Logic v t (logic bc nht) cho phép chúng ta nĩi v các đi tưng , tính cht ca chúng, quan h gia chúng, phát biu v tt c các đi tưng hay mt đi tưng nào đĩ mà khơng cn lit kê tưng minh.
4. Logic Bc nht 4
   Các câu khơng th biu din bng logic mnh đ nhưng cĩ th bng logic bc nht
   Socrates là ngưi nên socrates cht
   Khi sơn mt hp bng màu xanh, nĩ s tr thành hp xanh
   Mt ngưi đưc cho phép truy cp trang web nu h đưc cp quyn chính thc hay quen bit vi ai đưc phép truy cp
5. Cú pháp ca FOL 5
   Term (tham chiu đi tưng)
   Ký hiu hng: Lan, Tuan, DHKHTN,
   Bin: x, y, a,
   Ký hiu hàm áp dng cho mt hay nhiu term: f(x), tuoi(Lan), anhcua(Tuan)
   Câu (phát biu v đi tưng)
   Mt ký hiu v t (predicate) áp dng cho mt hay nhiu term : Thuoc(Lan, DHKHTN), Laanhem(Tuan, Lan), Labanbe(anh cua(Tuan), Lan),
   t1= t2
   Nu x là mt bin và φ là mt câu thì ∀x. φ và ∃x. φ là mt câu
   Các câu to t các câu khác vi tốn t ni câu: ¬ ∧∧∧ ∨∨∨ ←←← ↔ →→→
   Tên và s lưng đi s ca hàm hay v t đưc gi là functor và arity.
6. Ng nghĩa ca FOL 6
   Cĩ mt tp ngm đnh U các đi tưng mà mt câu FOL phát biu trên đĩ, U gi là tp vũ tr hay min phát biu.
   Term tham chiu đn đi tưng trong U:
   Hng tham chiu đn mt đi tưng c th.
   Bin tham chiu đn mt đi tưng nào đĩ (cn lưng t hĩa).
   Hàm tham chiu đn mt đi tưng thơng qua các đi tưng khác.
   Câu là phát biu trên các đi tưng:
   V t th hin tính cht hoc quan h gia các đi tưng.
   Lưng t giúp phát biu trên tồn b các đi tưng (lưng t vi mi) hay mt đi tưng nào đĩ (lưng t tn ti) mà khơng cn lit kê hay nêu ra tưng minh.
7. Lưng t vi mi 7
   ∀ Sinh viên CNTT thì thơng minh: ∀x Sinhviên(x,CNTT) → Thơngminh(x)
   ∀x P đúng trong mt min phát biu U nu và ch nu P đúng vi mi x thuc U.
   Nghĩa là, tương đương vi phép ni lin ca các đi tưng trong U Sinhviên(Lan,CNTT) → Thơngminh(Lan) ∧ Sinhviên(Minh,CNTT) → Thơngminh(Minh) ∧ Sinhviên(Tun,CNTT) → Thơngminh(Tun) ∧
8. Li thưng gp cn tránh 8
   Thơng thưng, → là phép ni thưng đi vi ∀
   Li thưng gp: dùng ∧ làm phép ni chính đi vi ∀: ∀x Sinhviên(x,CNTT) ∧ Thơngminh(x) nghĩa là “Mi ngưi đu là sinh viên CNTT và mi ngưi đu thơng minh”
9. Lưng t Tn ti 9
   ∃ Cĩ sinh viên CNTT thơng minh: ∃x Sinhviên(x,CNTT) ∧ Thơngminh(x)
   ∃x. P đúng trong mt min phát biu U nu và ch nu P đúng vi mt x nào đĩ thuc U.
   Nghĩa là, tương đương vi phép ni ri ca các đi tưng trong U Sinhviên(Lan,CNTT) ∧ Thơngminh(Lan) ∨ Sinhviên(Minh,CNTT) ∧ Thơngminh(Minh) ∨ Sinhviên(Tun,CNTT) ∧ Thơngminh(Tun) ∨
10. Li thưng gp khác cn tránh 10
    Thơng thưng, ∧ là phép ni chính vi ∃
    Li thưng gp: dùng → làm phép ni chính vi ∃: ∃x Sinh viên(x,CNTT) → Thơng minh(x) đúng nu cĩ bt kỳ ai khơng là sinh viên CNTT!
11. Vit FOL như th nào 11 1 1
    Mèo là đng vt cĩ vú [Mèo , ðngvtcĩvú ] ∀x.Mèo(x) → ðngvtcĩvú(x) 1 1
    Lan là sinh viên hc gii [Sinhviên , Hcgii ,Lan] Sinhviên(Lan) ∧ Hcgii(Lan) 2 2 2
    Cháu là con ca anh em [Cháu , Anhem , Con ] ∀x,y.Cháu(x,y) ↔ ∃z.(Anhem(z,y) ∧ Con(x,z))
    Bà ngoi là m ca m [các hàm: bàngoi, m] ∀xy. x= bàngoi(y) ↔ ∃z.(x= m(z) ∧ z= m(y)) 2
    Mi ngưi đu yêu ai đĩ [Yêu ] ∀x, ∃y.Yêu(x, y) ∃x, ∀y.Yêu(x, y)
12. Vit FOL như th nào (tt) 12
    Khơng ai yêu Lan ∀x. ¬Yêu(x, Lan) ¬∃ x. Yêu(x,Lan)
    Ai cũng cĩ mt cha ∀x, ∃y. Cha(y,x)
    Ai cũng cĩ mt cha và mt m ∀x, ∃yz. Cha(y,x) ∧ M(z,x)
    Bt kỳ ai cĩ mt cha cũng cĩ mt m ∀x. [[ ∃y.Cha(y,x)] → [∃y.M(y,x)]]
13. Suy dn trong FOL 13
    KB suy dn S: vi mi th hin I, nu KB tho trong I thì S cũng tho trong I
    Nĩi chung tính tốn suy dn là khơng kh thi vì cĩ vơ s các min phát biu cĩ th
    Ngay c vic tính tốn tính tho cũng khơng kh thi đi vi các min phát biu vơ hn
14. Chng minh và Suy dn 14
    Suy dn xut phát t khái nim tng quát ca phép “kéo theo”
    Khơng th tính tốn trc tip bng cách lit kê
    Do đĩ, ta s làm theo cách chng minh
    Trong FOL, nu KB suy dn đưc S thì cĩ mt tp hu hn các chng minh ca S t KB
    Tn ti h chng minh FOL đ và đúng
15. Hp gii Bc nht 15 ∀∀∀x, P(x)  Q(x) Tam đon lun: Mi ngưi đu cht P(A) Socrates là ngưi Hai vn đ mi: Q(A) Socrates cht • bin đi FOL thành dng mnh đ (clausal form) ∀∀∀x, ¬¬¬P(x) ∨∨∨ Q(x) • hp gii vi bin Tương đương theo P(A) đnh nghĩa ca phép Q(A) Suy ra Thay A vào x, vn ¬¬¬P(A) ∨∨∨ Q(A) đúng P(A) khi đĩ Q(A) Hp gii Mnh đ
16. Dng mnh đ (Clausal Form) 16
    cu trúc ngồi ging CNF
    khơng cĩ lưng t ∀x. ∃y. P(x) ⇒ R(x, y) ¬P(x) ∨ R(x, F(x))
17. Bin đi thành dng mnh đ 17 1. Loi b các du mũi tên α ↔ β ⇒ (α → β) ∧ (β → α) α → β ⇒ ¬α ∨ β 2. Phân phi ph đnh ¬¬α ⇒ α ¬(α ∨ β) ⇒ ¬α ∧ ¬β ¬(α ∧ β) ⇒ ¬α ∨ ¬β ¬∀ x. α ⇒ ∃x. ¬α ¬∃ x. α ⇒ ∀x. ¬α 3. ði tên các bin thành phn ∀x. ∃y.( ¬P(x) ∨ ∃x. Q(x,y)) ⇒∀ x1. ∃y.( ¬P(x 1) ∨ ∃x2. Q(x 2,y))
18. Skolem hố 18 4. Skolem hố
    thay tên mi cho tt c lưng t tn ti ∃x. P(x) ⇒ P(Lan) ∃x,y.R(x,y) ⇒ R(Thing1, Thing2) ∃x. P(x) ∧ Q(x) ⇒ P(Fleep) ∧ Q(Fleep) ∃x. P(x) ∧ ∃x. Q(x) ⇒ P(Frog) ∧ Q(Grog) ∃y, ∀x. Loves(x,y) ⇒ ∀x.Loves(x, Englebert)
    thay hàm mi cho tt c các lưng t tn ti tm vc ngồi ∀x ∃y. Loves(x,y) ⇒ ∀x.Loves(x, beloved(x)) ∀x ∃y ∀z ∃w. P(x,y,z) ∧ R(y,z,w) ⇒ ∀x ∀z. P(x,F(x),z) ∧ R(F(x),z,G(x,z))
19. Bin đi thành dng mnh đ 19 5. B các lưng t vi mi ∀x. ∃y Loves(x,y) ⇒ Loves(x, beloved(x)) 6. Phn phi or vào and; tr v các mnh đ P(z) ∨ (Q(z,w) ∧ R(w,z)) ⇒ {P(z) ∨ Q(z,w), P(z) ∨ Q(w,z)} 7. ði tên các bin trong tng mnh đ {P(z) ∨ Q(z,w), P(z) ∨ Q(w,z)} ⇒ {P(z 1) ∨ Q(z 1,w 1), P(z 2) ∨ Q(w 2,z 2)}
20. Hp gii Bc nht 20 ∀∀∀x, P(x)  Q(x) Tam đon lun: Mi ngưi đu cht P(A) Socrates là ngưi Q(A) Socrates cht ðiu ch yu là tìm các ∀∀∀x, ¬¬¬P(x) ∨∨∨ Q(x) phép th đúng đn cho Tương đương theo các bin P(A) đnh nghĩa ca phép Q(A) Suy ra Thay A vào x, vn ¬¬¬P(A) ∨∨∨ Q(A) đúng P(A) khi đĩ Q(A) Hp gii Mnh đ
21. Phép th 21 P(x, f(y), B): mt câu FOL Các th hin Phép th Ghi chú {v 1/t 1, v 2/t 2 } P(z, f(w), B) {x/z, y/w} ði tên bin P(x, f(A), B) {y/A} P(g(z), f(A), B) {x/g(z), y/A} P(C, f(A), B) {x/C, y/A} Phép th cơ s
22. Phép th 22 P(x, f(y), B): mt câu FOL Các th hin Phép th Ghi chú {v 1/t 1, v 2/t 2 } P(z, f(w), B) {x/z, y/w} ði tên bin P(x, f(A), B) {y/A} P(g(z), f(A), B) {x/g(z), y/A} P(C, f(A), B) {x/C, y/A} Phép th cơ s Áp dng mt phép th P(x, f(y), B) {y/A} = P(x, f(A), B) P(x, f(y), B) {y/A, x/y} = P(A, f(A), B)
23. ðng nht 23
    Hai biu thc ω1 và ω2 là đng nht đưc (unifiable ) khi vào ch khi tn ti phép th s sao cho ω1s = ω2s
    Gi ω1 = x và ω2 = y, dưi đây là các phép đng nht : s ω1s ω2s {y/x} x x {x/y} y y {x/f(f(A)), y/f(f(A))} f(f(A)) f(f(A)) {x/A, y/A} A A
24. ðng nht tng quát nht 24
    ð đng nht Knows(John,x) và Knows(y,z) , ta cĩ các phép th θ = {y/John, x/z } hay θ = {y/John, x/John, z/John}
    Phép đng nht đu tiên tng quát hơn cái th hai.
25. ðng nht tng quát nht 25
    g là phép đng nht tng quát nht (most general unifier MGU) ca ω1 và ω2 khi và ch khi vi mi phép đng nht s, tn ti s’ sao cho ω1.s = (ω1.g)s’ và ω2.s = (ω2.g)s’ ω1 ω2 MGU P(x) P(A) {x/A} P(f(x), y, g(x)) P(f(x), x, g(x)) {y/x} hay {x/y} P(f(x), y, g(y)) P(f(x), z, g(x)) {y/x, z/x} P(x, B, B) P(A, y, z) {x/A, y/B, z/B} P(g(f(v)), g(u)) P(x, x) {x/g(f(v)), u/f(v)} P(x, f(x)) P(x, x) Khơng cĩ MGU!
26. Qui tc đng nht 26
    E1 đng nht vi E 2 khi:
    Nu E 1, E 2 là hng: đng nht nu E 1 ging E 2.
    E1 là bin, E 2 bt kì: luơn đng nht vi E 2 thay th cho E 1.
    E2 là bin, E 1 bt kì: luơn đng nht vi E 1 thay th cho E 2.
    Nu E 1, E 2 là hàm hoc v t: đng nht khi E1, E2:  cùng functor và arity  các đi s đng nht vi nhau theo đúng th t  các phép th dùng trong đng nht các đi s phi tương thích nhau.
27. Mt s ví d v đng nht 27 ωωω1 ωωω2 MGU A(B,C) A(x,y) {x/B, y/C} A(x, f(D,x)) A(E, f(D, y)) {x/E, y/E} A(x, y) A(f(C, y), z) {x/f(C,y), y/z} P(A, x, f(g(y))) P(y, f(z), f(z)) {y/A,x/f(z), z/g(y)} P(x, g(f(A)), f(x)) P(f(y), z, y) Khơng cĩ P(x, f(y)) P(z, g(w)) Khơng cĩ
28. ðiu cn nm 28
    Ý nghĩa ca logic bc nht
    Cú pháp ca logic bc nht
    Cĩ th biu din mt vn đ dưi dng logic bc nht
    Chuyn đi KB thành dng mnh đ
    Hiu đưc phép th và phép đng nht
29. Thc mc 29