Suy diễn với logic bậc nhất

SUY DIỄN VỚI LOGIC BẬC NHẤTTô Hoài ViệtKhoa Công nghệ Thông tinĐại học Khoa học Tự nhiên TPHCMthviet@fit.hcmuns.edu.vn1Tổng quátCơ sở của hợp giải trên logic bậc nhấtHợp giải trên logic bậc nhấtCác ví dụSuy diễn tiến và suy diễn lùiThuật giải suy diễn tiếnThuật giải suy diễn lùi2Cơ sở của hợp giải FOLHợp giải (Robinson): để chứng minh một tập KB có suy dẫn logic được một câu  hay không, viết lại KB   dưới dạng mệnh đề (clausal form) và cố gắng suy dẫn ra mệnh đề sai (hợp giải hai mệnh đề đối ngẫu)Phép đồng nhất: Unify(P(x),P(A))   = {x/A}3Ví dụChứng minh rằng (P(x)  Q(x)) và P(A) suy dẫn logic z.Q(z)1. P(x)  Q(x) Tiền đề2. P(A) Tiền đề3. Q(z) Kết luận4. P(z) 1, 3  = {x/z}5. False 2, 4  = {x/z, z/A}4Ví dụ (tt)Cho trước (P(x)  Q(x)) và P(A) và P(B), tìm z sao cho Q(z) là đúng1. P(x)  Q(x) Tiền đề2. P(A) Tiền đề3. P(B) Tiền đề4. Q(z) Kết luận5. P(z) 1, 4  = {x/z}6. False 2, 5  = {x/z, z/A}7. False 3, 5  = {x/z, z/B}5Ví dụ Quan hệ họ hàngArt là cha của Bob và Bud.Bob là cha của Cal và Coe.Ông nội là cha của cha. F(Art, Bob) F(Art, Bud) F(Bob, Cal) F(Bob, Coe) F(x, y)  F(y,z)  G(x,z)6Art có phải là Ông của Coe? 1. F(Art, Bob) Tiền đề 2. F(Art, Bud) Tiền đề 3. F(Bob, Cal) Tiền đề 4. F(Bob, Coe) Tiền đề 5. F(x, y)  F(y,z)  G(x,z) Tiền đề 6. G(Art, Coe) Kết luận 7. F(Art, y)  F(y,Coe) 5, 6  ={x/Art, z/Coe} 8. F(Art, Bob) 4, 7  ={x/Art, z/Coe, y/Bob} 9. False 1, 8  ={x/Art, z/Coe, y/Bob}7Ai là Ông của Coe? 1. F(Art, Bob) Tiền đề 2. F(Art, Bud) Tiền đề 3. F(Bob, Cal) Tiền đề 4. F(Bob, Coe) Tiền đề 5. F(x, y)  F(y,z)  G(x,z) Tiền đề 6. G(x2, Coe) Kết luận 7. F(x2, y)  F(y,Coe) 5, 6  = {z/ Coe, x/x2} 8. F(Bob, Coe) 1, 7  = {z/ Coe, x/x2, x2/ Art, y/ Bob} 9. False 4, 8  = {z/ Coe, x/x2, x2/ Art, y/ Bob}8Ai là Cháu của Art? 1. F(Art, Bob) Tiền đề 2. F(Art, Bud) Tiền đề 3. F(Bob, Cal) Tiền đề 4. F(Bob, Coe) Tiền đề 5. F(x, y)  F(y,z)  G(x,z) Tiền đề 6. G(Art, z2) Kết luận 7. F(Art, y)  F(y,z2) 5, 6  = {x/Art, z/z2} 8. F(Bob, z2) 1, 7  = {x/Art, z/z2,, y/Bob} 9. F(Bud, z2) 2, 7  = {x/Art, z/z2, y/Bud} 10. False 3, 8  = {x/Art, z/z2, y/Bob, z2/Cal} 11. False 4, 8  = {x/Art, z/z2, y/Bob, z2/Coe}9Ông và cháu? 1. F(Art, Bob) Tiền đề 2. F(Art, Bud) Tiền đề 3. F(Bob, Cal) Tiền đề 4. F(Bob, Coe) Tiền đề 5. F(x, y)  F(y,z)  G(x,z) Tiền đề 6. G(x, z) Kết luận 7. F(x, y)  F(y,z) 5, 6  = {} 8. F(Bob, z) 1, 7  = {x/Art, y/Bob} 9. F(Bud, z) 2, 7  = {x/Art, y/Bud} 10. False 3, 8  = {x/Art, y/Bob, z/Cal} 11. False 4, 8  = {x/Art, y/Bob, z/Coe}10Suy diễn tiến và suy diễn lùiSuy diễn tiến (Forward chaining) và suy diễn lùi (Backward chahining) được áp dụng lên các biểu thức dạng HornBiểu thức dạng Horn: trong biểu thức có nhiều nhất một literal khẳng định p1  p2  p3   pnHay dạng luật (luật sinh) p2  p3   pn  p111Thuật toán Suy diễn TiếnFOL-FC-Ask(KB,){ repeat until new là rỗng new  {} với mọi câu r trong KB // r ở dạng chuẩn hóa (p1   pn => q) với mọi phép thế  sao cho (p1   pn)= (p’1   p’n) với p’1,,p’n nào đó trong KB q’  Subst(,q) if q’ không phải là một 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}12Ví dụ Quan hệ họ hàng1. 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)13Ví dụ Suy diễn tiến8. 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) 14Ví dụ Suy diễn tiến (tt)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) 15Ví dụ Suy diễn tiến (tt)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)16Thuật toán Suy diễn LùiFOL-BC-ASK(KB, goals, ){ Inputs: KB, cơ sở tri thức goals, danh sách dưới dạng nối rời của một câu truy vấn , phép thế hiện tại, được khởi tạo rỗng {} biến cục bộ: ans, một tập các phép thế, được khởi tạo rỗng if goals rỗng then return {} q’  SUBST(, first(goals)) for each r trong KB mà r có dạng chuẩn (p1   pn  q) và ’  UNIFY(q, q’) thành công ans  FOL-BC-ASK(KB, [p1,,pn| REST(goals)],   ’))  ans return ans}17Ví dụ Suy diễn lùiAsk(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) ’ = {x2/Art,y/y2} // F(x2,y2)  P(x2,y2) Ask({F(x2,y2),P(y,z)}, {x/Art,z/Cal,x2/Art}} q’ = F(Art,y2) ’ = {y2/Bob} // F(Art,Bob) Ask({P(y,z)}, {x/Art,z/Cal,x2/Art,y2/Bob,y/y2}) q’ = P(Bob,Cal) ’ = {x3/Bob,y3/Cal} // F(x3,y3)  P(x3,y3) Ask({F(x3,y3)}, {x3/Bob,y3/Cal}  ans 18Ví dụ Suy diễn lùi (tt)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) ’ = {x2/Bob, y2/z} // F(x2,y2)  P(x2,y2)19Ví dụ Suy diễn lùi (tt)Ask(G(Art,z), {}) Ask({F(x2,y2)}, {x2/Bob, y2/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)  false20Đặc điểm của suy diễn lùiTìm kiếm chứng minh bằng cách đệ qui theo chiều sâu: không gian tuyến tính theo kích thước của chứng minhKhông đầy đủ do lặp vô tậnGiải pháp: Kiểm tra trạng thái hiện tại với mọi trạng thái đang có trong stackKhông hiệu quả do các mục tiêu con bị lặp lại (cả khi thất bại cũng như thành công)Giải pháp: dùng bộ nhớ tạm lưu lại các mục tiêu con đã duyệt quaĐược dùng nhiều trong lập trình logic (ngôn ngữ Prolog)21Điều cần nắmCác phương pháp suy diễn trên logic vị từChạy tay được hợp giải trên logic vị từCài đặt được phương pháp suy diễn lùi (và một phương pháp khác) trên logic vị từ22