Bài giảng Trí tuệ nhân tạo - Suy diễn logic bậc nhất

pdf 25 trang hapham 1100
Bạn đang xem 20 trang mẫu của tài liệu "Bài giảng Trí tuệ nhân tạo - Suy diễn logic bậc nhất", để tải tài liệu gốc về máy bạn click vào nút DOWNLOAD ở trên

Tài liệu đính kèm:

  • pdfbai_giang_tri_tue_nhan_tao_suy_dien_logic_bac_nhat.pdf

Nội dung text: Bài giảng Trí tuệ nhân tạo - Suy diễn logic bậc nhất

  1. TRÍ TU NHÂN TO Suy din vi Logic Bc Nht
  2. Ni dung trỡnh bày 2  Cơ s ca hp gii trờn logic bc nht  Hp gii trờn logic bc nht  Cỏc vớ d  Tha s húa  Suy din tin và suy din lựi  Thut gii suy din tin  Thut gii suy din lựi
  3. Cơ s ca hp gii FOL 3  Hp gii (Robinson): ủ chng minh mt tp KB cú suy dn logic ủưc mt cõu α hay khụng, vit li KB ∧ ơα dưi dng mnh ủ (clausal form) và c gng suy dn ra mnh ủ sai (hp gii hai mnh ủ ủi ngu)  Qui tc hp gii cho FOL α ∨ ϕ MGU( ϕ, ω) = θ ơω ∨ β ___ (α ∨ β)( θ) Substitute
  4. Vớ d 4 Chng minh rng (P(x) ⇒ Q(x)) và P(A) suy dn logic ∃z.Q(z) 1. ơP(x) ∨ Q(x) Tin ủ 2. P(A) Tin ủ 3. ơQ(z) Kt lun 4. ơP(z) 1, 3 θ1 = {x/z} 5. False 2, 4 θ2 = {z/A} Yes
  5. Vớ d (tt) 5 Cho trưc (P(x) ⇒ Q(x)) và P(A) và P(B), tỡm z sao cho Q(z) là ủỳng 1. ơP(x) ∨ Q(x) Tin ủ 2. P(A) Tin ủ 3. P(B) Tin ủ 4. ơQ(z) Kt lun 5. ơP(z) 1, 4 θ1 = {x/z} 6. False 2, 5 θ2 = {z/A} 7. False 3, 5 θ3 = {z/B} z = A z = B
  6. Vớ d Quan h h hàng 6 Art là cha ca Bob và Bud. Bob là cha ca Cal và Coe. ễng ni là cha ca cha. F(Art, Bob) F(Art, Bud) F(Bob, Cal) F(Bob, Coe) F(x, y) ∧ F(y,z) ⇒ G(x,z)
  7. Art cú phi là ễng ca Coe? 7 1. F(Art, Bob) Tin ủ 2. F(Art, Bud) Tin ủ 3. F(Bob, Cal) Tin ủ 4. F(Bob, Coe) Tin ủ 5. ơF(x, y) ∨ ơF(y,z) ∨ G(x,z) Tin ủ 6. ơG(Art, Coe) Kt lun 7. ơF(Art, y) ∨ ơF(y,Coe) 5, 6 θ1 ={x/Art, z/Coe} 8. ơF(Art, Bob) 4, 7 θ2 ={y/Bob} 9. False 1, 8 θ3 ={ } Yes
  8. Ai là ễng ca Coe? 8 1. F(Art, Bob) Tin ủ 2. F(Art, Bud) Tin ủ 3. F(Bob, Cal) Tin ủ 4. F(Bob, Coe) Tin ủ 5. ơF(x, y) ∨ ơF(y,z) ∨ G(x,z) Tin ủ 6. ơG(x 2, Coe) Kt lun 7. ơF(x 2, y) ∨ ơF(y,Coe) 5, 6 θ1 = {z/ Coe, x/x 2} 8. ơF(Bob, Coe) 1, 7 θ2 = {x 2/ Art, y/ Bob} 9. False 4, 8 θ3 = {} x2 = Art
  9. Ai là Chỏu ca Art? 9 1. F(Art, Bob) Tin ủ 2. F(Art, Bud) Tin ủ 3. F(Bob, Cal) Tin ủ 4. F(Bob, Coe) Tin ủ 5. ơF(x, y) ∨ ơF(y,z) ∨ G(x,z) Tin ủ 6. ơG(Art, z 2) Kt lun 7. ơF(Art, y) ∨ ơF(y,z 2) 5, 6 θ1 = {x/Art, z/z 2} 8. ơF(Bob, z 2) 1, 7 θ2 = {y/Bob} 9. ơF(Bud, z 2) 2, 7 θ3 = {y/Bud} 10. False 3, 8 θ4 = {z 2/Cal} 11. False 4, 8 θ5 = {z 2/Coe} z2 = Cal z2 = Coe
  10. ễng và chỏu? 10 1. F(Art, Bob) Tin ủ 2. F(Art, Bud) Tin ủ 3. F(Bob, Cal) Tin ủ 4. F(Bob, Coe) Tin ủ 5. ơF(x, y) ∨ ơF(y,z) ∨ G(x,z) Tin ủ 6. ơG(x 2, z 2) Kt lun 7. ơF(x 2, y) ∨ ơF(y,z 2) 5, 6 θ1 = {x/x 2, z/z 2} 8. ơF(Bob, z 2) 1, 7 θ2 = {x 2/Art, y/Bob} 9. ơF(Bud, z 2) 2, 7 θ3 = {x 2/Art, y/Bud} 10. False 3, 8 θ4 = {z 2/Cal} 11. False 4, 8 θ5 = {z 2/Coe} x2 = Art, z 2 = Cal x2 = Art, z 2 = Coe
  11. Hp gii nh phõn 11  Qui tc hp gii trờn cũn gi là hp gii nh phõn.  Hp gii nh phõn là khụng ủy ủ.  Vớ d: Th hp gii P(x) ∨ P(y) ơP(v) ∨ ơP(w)
  12. Tha s húa (Factoring) 12  Qui tc tha s húa α ∨ β ∨ γ MGU( α, β) = θ ___ (α ∨ γ)( θ)  Vớ d: Q(x) ∨ P(x) ∨ P(A) ___ θ = {x/A} Q(A) ∨ P(A)  Hp gii nh phõn + tha s húa là ủy ủ
  13. Suy din tin và suy din lựi 13  Suy din tin (Forward chaining) và suy din lựi (Backward chahining) ủưc ỏp dng lờn cỏc biu thc dng Horn mt cỏch rt hiu qu.  Biu thc dng Horn: p1 ∧ p2 ∧ ∧ pn ⇒ p (rule) p (fact)  Generalized Modus Ponens: α1, α2, , αn, ( β1 ∧ β1 ∧ ∧ βn ⇒ q) αi(θ) = βi(θ) , i = 1 n ___ q (θ)
  14. Thut toỏn Suy din Tin 14 FOLFCAsk(KB, α){ repeat until new là rng new  {} vi mi cõu r trong KB // r dng chun húa (p 1 ∧ ∧ pn => q) vi mi phộp th θ sao cho (p1 ∧ ∧ pn)( θ)= (p’ 1 ∧ ∧ p’ n)( θ) vi p’ 1, ,p’ n nào ủú trong KB q’  Subst( θ,q) if q’ khụng phi là mt cõu ủó cú trong KB hay new then thờm q’ vào new φ  Unify(q’, α) if φ thành cụng then return φ thờm new vào KB return false }
  15. Vớ d Quan h h hàng 15 1. F(Art, Bob) 2. F(Art, Bud) 3. F(Bob, Cal) 4. F(Bob, Coe) 5. M(Ave, Bee) 6. M(Bee, Coe) 7. M(Bee, Cal) 8. M(x,y) ⇒ P(x,y) 9. F(x,y) ⇒ P(x,y) 10. P(x, y) ∧ P(y,z) ⇒ G(x,z)
  16. Vớ d Suy din tin 16 8. M(x,y) ⇒ P(x,y) θ1 = {x/Ave, y/Bee} M(Ave,Bee) q’ = P(Ave, Bee) θ2 = {x/Bee, y/Cal} M(Bee,Cal) q’ = P(Bee,Cal) θ3 = {x/Bee, y/Coe} M(Bee,Coe) q’ = P(Bee,Coe)
  17. Vớ d Suy din tin (tt) 17 9. F(x,y) ⇒ P(x,y) θ1 = {x/Art, y/Bob} F(Art,Bob) q’ = P(Art,Bob) θ2 = {x/Art, y/Bud} F(Art,Bud) q’ = P(Art,Bud) θ3 = {x/Bob, y/Cal} F(Bob,Cal) q’ = P(Bob,Cal) θ4 = {x/Bob, y/Coe} F(Bob,Coe) q’ = P(Bob,Coe)
  18. Vớ d Suy din tin (tt) 18 10. P(x, y) ∧ P(y,z) ⇒ G(x,z) θ1 = {x/Ave,y/Bee,z/Cal} P(Ave,Bee) ∧ P(Bee,Cal) q’ = G(Ave, Cal) θ2 = {x/Ave,y/Bee,z/Coe}P(Ave,Bee) ∧ P(Bee,Coe) q’ = G(Ave, Coe) θ3 = {x/Art, y/Bob, z/Cal} P(Art,Bob) ∧ P(Bob,Cal) q’ = G(Art, Cal) θ4 = {x/Art, y/Bob, z/Coe} P(Art,Bob) ∧ P(Bob,Coe) q’ = G(Art, Coe)
  19. Thut toỏn Suy din Lựi 19 FOLBCASK(KB, goals, θ){ Inputs: KB , cơ s tri thc goals , danh sỏch dưi dng ni ri ca mt cõu truy vn θ, phộp th hin ti, ủưc khi to rng {} bin cc b: ans , mt tp cỏc phộp th, ủưc khi to rng if goals rng then return {θ} q’  SUBST( θ, first(goals)) for each r trong KB mà r cú dng chun (p 1 ∧ ∧ pn ⇒ q) và θ’  UNIFY(q, q’) thành cụng ans  FOLBCASK(KB, [p 1, ,p n| REST(goals)], θ . θ’)) ∪ ans return ans Compose }
  20. Vớ d Suy din lựi 20 Ask(G(Art,Cal), {}) q’ = G(Art,Cal) θ’ = {x/Art,z/Cal} // P(x,y) ∧ P(y,z) ⇒ G(x ,z) Ask({ P(x,y),P(y,z) },{x/Art,z/Cal}) q’ = P(Art,y) θ’ = {x 2/Art,y/y 2} // F(x 2,y 2) ⇒ P(x 2,y 2) Ask({ F(x 2,y 2),P(y,z) }, {x/Art,z/Cal,x 2/Art, y/y 2}} q’ = F(Art,y 2) θ’ = {y 2/Bob} // F(Art,Bob) Ask({ P(y,z) }, {x/Art,z/Cal,x 2/Art,y/Bob}) q’ = P(Bob,Cal) θ’ = {x 3/Bob,y 3/Cal} // F(x 3,y 3) ⇒ P(x 3,y 3) Ask({F(x 3,y 3)}, { x 3/Bob,y 3/Cal}  ans
  21. Vớ d Suy din lựi (tt) 21 Ask(G(Art,z), {}) q’ = G(Art,z) θ’ = {x/Art} // P(x,y) ∧ P(y,z) ⇒ G(x,z) Ask({ P(x,y),P(y,z) },{x/Art}) q’ = P(Art,y) θ’ = {x/Art} // F(x,y) ⇒ P(x,y) Ask({ F(x,y),P(y,z)}, {x/Art}) q’ = F(Art,y) θ’ = {x/Art,y/Bob} // F(Art,Bob) Ask({ P(y,z) }, {x/Art, y/Bob}) q’ = P(Bob,z) θ’ = {x 2/Bob, y 2/z} // F(x 2,y 2) ⇒ P(x 2,y 2)
  22. Vớ d Suy din lựi (tt) 22 Ask(G(Art,z), {}) Ask({ F(x 2,y 2)}, { x 2/Bob, y 2/z}) q’ = F(Bob,z) θ’ = {z/Cal} // F(Bob,Cal) Ask({}, { z/Cal })  ans θ’ = {z/Coe} // F(Bob,Cal) Ask({}, { z/Coe })  ans θ’ = {x/Art} // M(x,y) ⇒ P(x,y) Ask({ M(x,y),P(y,z) }, {x/Art}} q’ = M(Art,y)  false
  23. ðc ủim ca suy din lựi 23  Tỡm kim chng minh bng cỏch ủ qui theo chiu sõu: khụng gian tuyn tớnh theo kớch thưc ca chng minh  Khụng ủy ủ do lp vụ tn  Gii phỏp: Kim tra trng thỏi hin ti vi mi trng thỏi ủang cú trong stack  Khụng hiu qu do cỏc mc tiờu con b lp li (c khi tht bi cũng như thành cụng)  Gii phỏp: dựng b nh tm lưu li cỏc mc tiờu con ủó duyt qua  ðưc dựng nhiu trong lp trỡnh logic (ngụn ng Prolog)
  24. ðiu cn nm 24  Cỏc phương phỏp suy din trờn logic v t  Chy tay ủưc hp gii trờn logic v t  Cài ủt ủưc phương phỏp suy din lựi (và mt phương phỏp khỏc) trờn logic v t
  25. Thc mc 25