›

Bài giảng Nhập môn trí tuệ nhân tạo - Chương 2: Logic hình thức - Ngô Hữu Phúc

pdf 143 trang cucquyet12 5930
Download
Bạn đang xem 20 trang mẫu của tài liệu "Bài giảng Nhập môn trí tuệ nhân tạo - Chương 2: Logic hình thức - Ngô Hữu Phúc", để 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_nhap_mon_tri_tue_nhan_tao_chuong_2_logic_hinh_thuc.pdf

Nội dung text: Bài giảng Nhập môn trí tuệ nhân tạo - Chương 2: Logic hình thức - Ngô Hữu Phúc

  1. NHẬP MÔN TRÍ TUỆ NHÂN TẠO Chương 2: Logic hình thức Biên soạn: TS Ngô Hữu Phúc Bộ môn: Khoa học máy tính Mobile: 098 56 96 580 Email: ngohuuphuc76@gmail.com 1 Chương 2: Logic
  2. Thông tin chung  Thông tin về nhóm môn học: TT Họ tên giáo viên Học hàm Học vị Đơn vị công tác (Bộ môn) 1 Ngô Hữu Phúc GVC TS BM Khoa học máy tính 2 Trần Nguyên Ngọc GVC TS BM Khoa học máy tính 3 Hà Chí Trung GVC TS BM Khoa học máy tính 4 Trần Cao Trưởng GV ThS BM Khoa học máy tính  Thời gian, địa điểm làm việc: Bộ môn Khoa học máy tính Tầng 2, nhà A1.  Địa chỉ liên hệ: Bộ môn Khoa học máy tính, khoa Công nghệ thông tin.  Điện thoại, email: 069-515-329, ngohuuphuc76.mta@gmail.com. 2 Chương 2: Logic
  3. Cấu trúc môn học  Chương 1: Giới thiệu chung.  Chương 2: Logic hình thức.  Chương 3: Các phương pháp tìm kiếm mù.  Chương 4: Các phương pháp tìm kiếm có sử dụng thông tin.  Chương 5: Các chiến lược tìm kiếm có đối thủ.  Chương 6: Các bài toán thỏa rằng buộc.  Chương 7: Nhập môn học máy. 3 Chương 2: Logic
  4. Bài 2: Logic hình thức Chương 2, mục: 2.1 – 2.4 Tiết: 1-3; 4-6; Tuần thứ: 2,3. Mục đích, yêu cầu: 1. Nắm được Logic hình thức. 2. Nắm được sự tương đương logic. 3. Nắm được phương pháp lập luận và suy diễn sử dụng logic. Hình thức tổ chức dạy học: Lý thuyết. Thời gian: 3 tiết. Địa điểm: Giảng đường do Phòng Đào tạo phân công Nội dung chính: (Slides) 4 Chương 2: Logic
  5. Nội Dung •Lựa chọn hành động dựa trên tri thức. •Hang Wumpus . •Logic. •Logic Mệnh đề. •Tính tương đương, tính thoả được. •Lập luận & chứng minh tự động trên Logic Mệnh đề lập luận tiến lập luận lùi phép giải Chương 2: Logic 5
  6. Cơ Sở Tri Thức • Cơ sở tri thức = tập các câu trong một ngôn ngữ hình thức nào đó • Giải quyết vấn đề bằng đặc tả – Cơ sở tri thức (KB) biểu diễn điều mà agent cần biết • Sau đó để giải quyết vấn đề chỉ cần ra lệnh “what to do?”. Cơ sở tri thức và cơ chế lập luận sẽ giúp agent tự giải quyết vấn đề. • Do đó agent có thể được dùng tuỳ thuộc vào cấp độ tri thức chứ không phụ thuộc vào cài đặt. (cấu trúc dữ liệu, thuật toán, ). Chương 2: Logic 6
  7. Khung mẫu cho Agent tựa tri thức • Agent phải có khả năng: – biểu diễn trạng thái, hành động etc. – Tiếp nạp dữ liệu mới từ bên ngoài. – Thay đổi nhận thức (biểu diễn) thê giới bên ngoài. – Suy diễn những sự kiện ẩn (không thấy) của thế giới bên ngoài – Dẫn đến hành động thíchChương hợp 2: trên Logic cơ sở suy diễn. 7
  8. Hang Wumpus • Điểm hiệu quả – gold +1000, death -1000 – -1 / 1 bước, -10 nếu dùng cung • Môi Trường – ô cạnh ô có Wumpus có mùi thối. – Ô cạnh bẫy có tiếng gió thổi. – Ô bên cạnh ô đựng vàng có ánh kim – Bắn Wumpus nếu đối diện với nó. – Chỉ được dùng một mũi tên – Chộp lấy vàng nếu ở cùng ô – Thả vàng rơi trong cùng ô • Sensors: mùi, tiếng gió, ánh kim, xóc, tiếng rên la. • Actuators: quay trái, phải, tiến, chộp, thả, bắn. Chương 2: Logic 8
  9. Đặc Điểm bài toán Hang Wumpus • Quan sát tất cả các trạng thái? không – chỉ quan sát được cục bộ • Đơn định? Có • Lời giải? Dãy các hành động để đạt được điểm thưởng cao nhất. • Tính động? Tĩnh – Wumpus và bẫy ở nguyên vị trí. • Rời rạc Có Chương 2: Logic 9
  10. Ví dụ Chương 2: Logic 10
  11. Ví dụ Chương 2: Logic 11
  12. Ví dụ Chương 2: Logic 12
  13. Ví dụ Chương 2: Logic 13
  14. Ví dụ Chương 2: Logic 14
  15. Ví dụ Chương 2: Logic 15
  16. Ví dụ Chương 2: Logic 16
  17. Ví dụ Chương 2: Logic 17
  18. Logic • Logics ngôn ngữ hình thức biểu diễn thông tin như các kết luận có thể trích rút, suy diễn từ tri thức và quan sát môi trường xung quanh. • Cú pháp định nghĩa cấu trúc câu cho Logic. • Ngữ nghĩa xác định nghĩa của câu – i.e. xác lập tính đúng đắn của một mệnh đề trong hoàn cảnh (thế giới) cụ thể. • Ví dụ ngôn ngữ số học – x+2 ≥ y là câu; x2+y > {} không phải là câu – x+2 ≥ y là đúng nếu số x+2 không nhỏ hơn số y – x+2 ≥ y đúng khi x = 7, y = 1 – x+2 ≥ y sai khi x = 0, y = 6 Chương 2: Logic 18
  19. Hệ quả logic • Hệ quả logic là việc đúng của một (số) mệnh đề dẫn theo mệnh đề khác đúng KB ╞ α • Cơ sở tt KB dẫn ra α (hay α là hệ quả Logic của KB) khi và chỉ khi α đúng trong mọi thế giới mà KB đúng. – VD KB có “đội MU thắng” và “Đội Chelsea thắng” dẫn ra “Một trong hai đội MU hoặc Chelsea thắng” – E.g., x+y = 4 dẫn ra 4 = x+y – Quan hệ dẫn được (hệ quả logic) là mối quan hệ giữa các mệnh đề (i.e., cú pháp) dựa trên ngữ nghĩa. Chương 2: Logic 19
  20. Models • models, thế giới (ngữ cảnh) mà tại đó các mệnh đề Logic được đánh giá tính đúng sai. • Gọi m là model của mệnh đề α nếu α đúng trong m • M(α) là tập tất cả các model của α • Ta có KB ╞ α khi và chỉ khi M(KB)  M(α) Chương 2: Logic 20
  21. Ví dụ Sau khi xuất phát tại [1,1], sang phải, nghe tiếng gió ở ô [2,1] • Xét các mô hình có thể, giải sử chỉ tính khả năng có hay không có hố ở các ô bên cạnh. 3 lựa chọn ô 8 mô hình Chương 2: Logic 21
  22. Ví dụ Chương 2: Logic 22
  23. Ví dụ • KB = luật + quan sát, tiếp nhận từ môi trường Chương 2: Logic 23
  24. Ví dụ • KB = luật + quan sát tiếp nhận từ môi trường • α1 = "[1,2] là an toàn", KB ╞ α1, chứng minh bằng kiểm tra models Chương 2: Logic 24
  25. Ví dụ • KB = luật + quan sát tiếp nhận từ môi trường Chương 2: Logic 25
  26. Ví dụ • KB = luật + quan sát tiếp nhận từ môi trường • α2 = "[2,2] an toàn", KB ╞ α2 Chương 2: Logic 26
  27. Lập Luận • KB ├i α = mệnh đề α dẫn được từ KB bằng thủ tục (cơ chế lập luận) i. • Chặt: i là chặt khi và chỉ khi nếu KB ├i α, thì KB╞ α. • Đủ: i là đủ khi và chỉ khi KB╞ α, thì KB ├i α Chương 2: Logic 27
  28. Logic Mệnh Đề: Cú pháp • Logic mệnh đề là loại logic đơn giản nhất (tương đương đại số Boolean), dùng để biểu diễn tri thức bậc 0 (monadic). • Giả sử P1, P2 là các mệnh đề – Nếu S là mệnh đề, S là mệnh đề – Nếu S1 và S2 là các mệnh đề, S1  S2 là mệnh đề – Nếu S1 và S2 là các mệnh đề, S1  S2 là một mệnh đề – Nếu S1 và S2 là các mệnh đề, S1 S2 là một mệnh đề – Nếu S1 và S2 là các mệnh đề, S1 S2 là một mệnh đề Chương 2: Logic 28
  29. Logic mệnh đề: ngữ nghĩa Mỗi model xác lập giá trị true/false cho mỗi ký hiệu mệnh đề E.g. P1,2 P2,2 P3,1 false true false Với 3 mệnh đề thì có thể có 8 model có thể liệt kê đầy đủ Luật để xác định giá trị dựa trên Model m: S is true iff S is false S1  S2 is true iff S1 is true and S2 is true S1  S2 is true iff S1is true or S2 is true S1 S2 is true iff S1 is false or S2 is true i.e., is false iff S1 is true and S2 is false S1 S2 is true iff S1 S2 is true andS2 S1 is true Thực chất là đánh giá đệ quy: P (P P ) = true (true false) = true true = true  1,2  2,2  3,1 Chương 2: Logic  29
  30. Bảng giá trị luận lý Chương 2: Logic 30
  31. Ví dụ Pi,j nhận giá trị đúng nếu có hố trong ô [i, j]. Bi,j nhận giá trị đúng nếu có tiếng gió trong ô [i, j].  P1,1 B1,1 B2,1 • “Hố tạo nên tiếng gió ở các ô xung quanh" B1,1 (P1,2  P2,1) B2,1 (P1,1  P2,2  P3,1) Chương 2: Logic 31
  32. Lập Luận Dựa Trên Bảng Luận Lý Chương 2: Logic 32
  33. Lập Luận Bằng Liệt Kê Models • Tìm kiếm (theo chiều sâu) và liệt kê các mô hình • Với n mệnh đề, độ phức tạp thời gian O(2n), không gian O(n) Chương 2: Logic 33
  34. Quan hệ Logic Tương Đương • Hai mệnh đề là khi và chỉ khi chúng cùng đúng trên các model : α ≡ ß iff α╞ β and β╞ α Chương 2: Logic 34
  35. Tính chân lý và Thoả được Một mệnh đề được gọi là chân lý (toàn đúng) nếu nó đúng trên mọi models, e.g., True, A A, A A, (A  (A B)) B Liên hệ với phép suy dẫn qua định lý suy diễn: KB ╞ α khi và chỉ khi (KB α) là chân lý Một mệnh đề gọi là thoả được nếu nó đúng trên một số model nào đó: e.g., A B, C Một mệnh đề gọi là toàn sai nếu nó sai trên mọi model e.g., AA Liên hệ với phép suy dẫn; KB ╞ α khi và chỉ khi (KB α) là toàn sai. Chương 2: Logic 35
  36. Phương Pháp Chứng Minh (suy dẫn) • Chia làm hai loại – Áp dụng luật suy diễn: • Sinh hợp lệ các mệnh đề mới từ mệnh đề cũ. • Chứng minh = Dãy các áp dụng luật suy diễn, có thể dùng các luật suy diễn như toán tử chuyển trạng trong các thuật toán tìm kiếm. – Kiểm tra Model • Xét bảng luận lý (tỷ lệ mũ với n) • Cải tiến Back-Tracking, Davis Putnam-Logemann-Loveland (DPLL) • Tìm kiếm Heuristic trong không gian các Model (chặt nhưng không đủ) Chương 2: Logic 36
  37. Phép Giải Dạng chuẩn (CNF) E.g., (A  B)  (B  C  D) • Luật suy dẫn bằng phép giải (cho CNF): li   lk, m1   mn li   li-1  li+1   lk  m1   mj-1  mj+1   mn trong đó li và mj là các literal nghịch nhau: E.g., P1,3  P2,2, P2,2 P1,3 • Phép giải là chặt và Chươngđủ đối 2: Logic với Logic mệnh đề. 37
  38. Chuyển công thức sang dạng CNF B1,1 (P1,2  P2,1)β 1. Khử : thay α β bằng (α β)(β α). (B1,1 (P1,2  P2,1))  ((P1,2  P2,1) B1,1) 2. Khử : Thay α β bằng α β. (B1,1  P1,2  P2,1)  ((P1,2  P2,1)  B1,1) 3. Đẩy  vào trong: sử dụng luật de Morgan's và phủ định của phủ định : (B  P  P )  ((P P )  B ) 1,1 1,2 2,1 1,2 ^ 2,1 1,1 4. Áp dụng luật phân phối : (B1,1  P1,2  P2,1)  (P1,2  B1,1)  (P2,1  B1,1) Chương 2: Logic 38
  39. Thuật Toán cho Phép Giải • chứng minh bằng phản chứng, i.e., chứng minh rằng KBα là luôn sai Chương 2: Logic 39
  40. Ví dụ • KB = (B1,1 (P1,2 P2,1))  B1,1 α = P1,2 Chương 2: Logic 40
  41. Lập Luận Tiến/Lùi • Dạng Horn (restricted) KB = kết hợp của các câu dạng Horn – Câu dạng Horn = • ký hiệu mệnh đề; hoặc • (hợp (and) các mệnh đề) mệnh đề – E.g., C  (B A)  (C  D B) – • Tam đoạn luận (cho dạng Horn): đủ Horn KBs α1, ,αn, α1   αn β β • có thể cài đặt cơ chế lập luận hướng tiến/lùi. • Các thuật toán này tự nhiên và chạy với thời gian đa thức. Chương 2: Logic 41
  42. Lập luận tiến • Ý tưởng: “cháy” luật có phần tiền đề thoả được trong KB, sau đó thêm phần kết luậ vào KB cho đến khi tìm được đích (trả lời câu hỏi) cần tìm) Chương 2: Logic 42
  43. Thuật Toán cho lập luận tiến • Lập luận tiến là chặt Chương& đủ 2: đốiLogic vớicác KB dạng Horn43
  44. Ví dụ minh hoạ Chương 2: Logic 44
  45. Ví dụ minh hoạ Chương 2: Logic 45
  46. Ví dụ minh hoạ Chương 2: Logic 46
  47. Ví dụ minh hoạ Chương 2: Logic 47
  48. Ví dụ minh hoạ Chương 2: Logic 48
  49. Ví dụ minh hoạ Chương 2: Logic 49
  50. Ví dụ minh hoạ Chương 2: Logic 50
  51. Ví dụ minh hoạ Chương 2: Logic 51
  52. Lập luận lùi Ý tưởng: lần ngược từ câu hỏi q: để chứng minh q kiểm tra xem q đã được dẫn ra chưa, nếu không tìm cách chứng minh các mệnh đề ở phần đầu luật có chứa q ở phần kết luận. Tránh lặp quẩn: Lưu trữ các đích đã được chứng minh và trước khi chứng minh kiểm tra xem đích cần chứng minh đã có trong goal stack chưa? Chương 2: Logic 52
  53. Ví Dụ Minh Hoạ Chương 2: Logic 53
  54. Ví Dụ Minh Hoạ Chương 2: Logic 54
  55. Ví Dụ Minh Hoạ Chương 2: Logic 55
  56. Ví Dụ Minh Hoạ Chương 2: Logic 56
  57. Ví Dụ Minh Hoạ Chương 2: Logic 57
  58. Ví Dụ Minh Hoạ Chương 2: Logic 58
  59. Ví Dụ Minh Hoạ Chương 2: Logic 59
  60. Ví Dụ Minh Hoạ Chương 2: Logic 60
  61. Ví Dụ Minh Hoạ Chương 2: Logic 61
  62. Ví Dụ Minh Hoạ Chương 2: Logic 62
  63. So Sánh Lập Luận Tiến/Lùi • FC hướng dữ liệu, tự động, xử lý không hướng đích. – e.g., nhận dạng, ra quyết định, • chứng minh nhiều thứ không liên quan đến đích • BC hướng đích, thích hợp cho giải quyết vấn đề, chuẩn đoán nguyên nhân, Chương 2: Logic 63
  64. Một Số Thuật Toán Kiểm Tra Model cho Bài Toán Thoả Được 1. BackTracking (đầy đủ): DPLL (Davis, Putnam, Logemann, Loveland) 2. Tìm kiếm địa phương (không đầy đủ): – WalkSAT Chương 2: Logic 64
  65. Giải Thuật DPLL Kiểm tra tính thoả được của công thức Logic ở dạng CNF Liệt kê mô hình với một số Heuristics: 1. Kết thúc sớm: Một câu là đúng nếu cớ một literal là đúng. Một câu là sai nếu tất cả các literal là sai (do đó toàn công thức sai) 2. Mệnh đề nhất quán luôn xuất hiện với cùng một đấu trong mọi câu e.g., (A  B), (B  C), (C  A), A và B nhất quán, C không nhất quán. cho mệnh đề nhất quán bằng true. 3. Câu đơn vị Câu đơn vị: câu chỉ có một literal Literal trong câu đó phải bằng true. Chương 2: Logic 65
  66. Giải Thuật DPLL Chương 2: Logic 66
  67. Giải Thuật WalkSAT • tìm kiếm địa phương – không đầy đủ. • hàm lượng giá: min-conflict heuristic - tối thiếu hóa số lượng các câu không thoả. • Cân bằng giữa chiến lược tham ăn và chiến lược tìm kiếm ngẫu nhiên. Chương 2: Logic 67
  68. Giải Thuật WalkSAT Chương 2: Logic 68
  69. Agent có khả năng lập luận cho bài toán hang Wumpus Sủ dụng cơ sở tri thức dạng logic mệnh đề: P1,1 W1,1 Bx,y (Px,y+1  Px,y-1  Px+1,y  Px-1,y) Sx,y (Wx,y+1  Wx,y-1  Wx+1,y  Wx-1,y) W1,1  W1,2   W4,4 W1,1  W1,2 W1,1  W1,3 64 mệnh đề, 155 câu Chương 2: Logic 69
  70. Chương 2: Logic 70
  71. Hạn chế của Logic mệnh đề • Trong ví dụ trên, mỗi một ô phải có công thức mà tính chất rất giống nhau. Nguyên nhân là do Logic mệnh đề không có khả năng biểu diễn quan hệ giữa các đối tượng trong thế giới của Agent. Một số ví dụ khác Chỉ có thể giải quyết được với Logic vị từ! Chương 2: Logic 71
  72. Đọc Thêm 1. Giáo trình chương 7. 2. Symbolic Logic and Mechanical Theorem Proving, C.L. Chang and R.C. Lee (chương 5). 3. Automated Reasoning, L. Wos, R. Overbeek, E. Lusk, and J. Boyle (ứng dụng của lập luận tự động). 4. An Introduction to Expert Systems, P. Jackson (chương 5). Chương 2: Logic 72
  73. Câu hỏi ôn tập 1. Trình bầy về logic mệnh đề: cú pháp, ngữ nghĩa, mô hình, tính chân lý, tính thoả được, tính hằng sai. 2. Trình bày phương pháp chuyển công thức logic mệnh đề sang dạng CNF. 3. Cài đặt phép giải và xây dựng chương trình chứng minh tự động cho phép giải. 4. Cài đặt cơ chế lập luận tiến/lùi trên cơ sở tri thức gồm các câu dạng horn và ứng dụng để xây dựng các hệ chuyên gia. 5. Cài đặt, thí nghiệm và đánh giá DPLL, WalkSAT 6. Nghiên cứu cài đặt các phương pháp tìm kiếm heuristics khác (SA, GA, ACO, ) cho bài toán SAT. 7. Cài đặt Agent có khả năng lập luận cho bài toán hang Wumpus. Chương 2: Logic 73
  74. NHẬP MÔN TRÍ TUỆ NHÂN TẠO Chương 2: Logic hình thức Biên soạn: TS Ngô Hữu Phúc Bộ môn: Khoa học máy tính Mobile: 098 56 96 580 Email: ngohuuphuc76@gmail.com 1 TTNT - Học viện Kỹ thuật Quân sự
  75. Thông tin chung  Thông tin về nhóm môn học: TT Họ tên giáo viên Học hàm Học vị Đơn vị công tác (Bộ môn) 1 Ngô Hữu Phúc GVC TS BM Khoa học máy tính 2 Trần Nguyên Ngọc GVC TS BM Khoa học máy tính 3 Hà Chí Trung GVC TS BM Khoa học máy tính 4 Trần Cao Trưởng GV ThS BM Khoa học máy tính  Thời gian, địa điểm làm việc: Bộ môn Khoa học máy tính Tầng 2, nhà A1.  Địa chỉ liên hệ: Bộ môn Khoa học máy tính, khoa Công nghệ thông tin.  Điện thoại, email: 069-515-329, ngohuuphuc76.mta@gmail.com. 2 TTNT - Học viện Kỹ thuật Quân sự
  76. Cấu trúc môn học  Chương 1: Giới thiệu chung.  Chương 2: Logic hình thức.  Chương 3: Các phương pháp tìm kiếm mù.  Chương 4: Các phương pháp tìm kiếm có sử dụng thông tin.  Chương 5: Các chiến lược tìm kiếm có đối thủ.  Chương 6: Các bài toán thỏa rằng buộc.  Chương 7: Nhập môn học máy. 3 TTNT - Học viện Kỹ thuật Quân sự
  77. Bài 2: Logic hình thức Chương 2, mục: 2.1 – 2.4 Tiết: 1-3; 4-6; Tuần thứ: 2,3. Mục đích, yêu cầu: 1. Nắm được Logic vị từ bậc 1. 2. Nắm được phương pháp biểu diễn tri thức trong Logic vị từ bậc 1. 3. Nắm được phương pháp lập luận và suy diễn trong Logic vị từ bậc 1. Hình thức tổ chức dạy học: Lý thuyết. Thời gian: 3 tiết. Địa điểm: Giảng đường do Phòng Đào tạo phân công Nội dung chính: (Slides) 4 TTNT - Học viện Kỹ thuật Quân sự
  78. Nội dung • Logic vị từ bậc 1. • Biểu diễn tri thức trong Logic vị từ bậc 1. • Lập luận và suy diễn trong Logic vị từ bậc 1.
  79. ưu nhược điểm của logic mệnh đề  logic mệnh đề mang tính đặc tả.  logic mệnh đề cho phép biểu diễn thông tin bộ phận, kết hợp, phủ định  Logic mệnh đề có tính cấu thành về ngữ nghĩa – ngữ nghĩa B1,1  P1,2 dẫn được từ ngữ nghĩa B1,1 và P1,2  Ngữ nghĩa của logic mệnh đề là độc lập ngữ cảnh. – (không giống như trong ngôn ngữ tự nhiên, ngữ nghĩa phụ thuộc ngũ cảnh)  Năng lực biểu diễn tri thức của logic mệnh đề hạn chế
  80. Logic Vị từ bậc 1 • Trong thế giới của Logic mệnh đề chỉ có các facts (mệnh đề bài trung), • Thê giới của Logic vị từ: – đối tượng: người, nhà cửa, xe, máy tính, – quan hệ: đỏ, xanh, cay, đắng, anh em, yêu, – hàm: cha của, ban tốt nhất, nhiều hơn một, cộng, trừ,
  81. Cú pháp của Logic vị từ • hằng Hà nội, 2, HVKTQS, • vị từ Anh em, >, • Functions Sqrt, Điểm cao nhất của, • biến x, y, a, b, • phép toán , , , , • đồng nhất = • lượng từ , 
  82. Câu nguyên thuỷ Câu nguyên thuỷ = vịtừ (term1, ,termn) hoặc term1 = term2 Term = hàm (term1, ,termn) hoặc hằng hoặc biến • VD: Brother(KingJohn,RichardTheLionheart) > (Length(LeftLegOf(Richard)), Length(LeftLegOf(KingJohn)))
  83. Mệnh đề phức hợp • tạo nên từ những câu (mệnh đề) nguyên thuỷ thông qua các phép toán logic: S, S1  S2, S1  S2, S1 S2, S1 S2, E.g. Sibling(KingJohn,Richard) Sibling(Richard,KingJohn) >(1,2)  ≤ (1,2) >(1,2)   >(1,2)
  84. Luận lý trong logic vị từ • mệnh đề được xem xét giá trị đúng/sai trên một model và một diễn dịch. • Model gồm các đối tượng và quan hệ giữa chúng. • Diễn dịch là ngữ nghĩa, tham chiếu, diễn giải trên model: ký hiêu hằng → đối tượng ký hiệu vị từ → quan hệ ký hiệu hàm → quan hệ hàm • Một câu (mệnh đề) nguyên thuỷ predicate(term1, ,termn) là đúng khi và chỉ khi các đối tượng tham chiếu bởi term1, term2, termn, có quan hệ predicate trên model. • Ví dụ: ???
  85. Models cho LGVT: Ví dụ
  86. Lượng từ phổ dụng •  Mọi học viên tại HVKTQS đều thông minh: x At(x,HVKTQS) Smart(x) • x P là đúng trên model m khi và chỉ khi P là đúng với x tham chiếu bằng bất cứ đối tượng nào thuộc m. • Tương đương với việc kiểm tra mệnh đề trên từng đối tượng của m At(Nam,HVKTQS) Smart(Nam)  At(Lan,HVKTQS) Smart(Lan)  At(Minh,HVKTQS) Smart(Minh) 
  87. Lỗi thông dụng • Thông thường, là phép toán chính trong phạm vi ảnh hưởng của  • Ví dụ lỗi (dùng ): x At(x,HVKTQS)  Smart(x) có nghĩa là “Mọi người đều là học viên HVKTQS và mọi người đều thông minh”.
  88. Lượng từ tồn tại •  • Tại học viện KTQS có học viên thông minh: • x At(x,HVKTQS)  Smart(x) • x P là đúng trên model m khi và chỉ khi P là đúng với x được tham chiểu bởi một (vài) đối tượng trong m. • Tương đương với: At(Nam,HVKTQS)  Smart(Nam)  At(Lan,HVKTQS)  Smart(Lan)  At(Minh,HVKTQS)  Smart(Minh) 
  89. Lỗi thường gặp • Thông thường,  là phép toán chính gắn với  • Lỗi thông dụng: Sử dụng làm phép toán chính trong : x At(x,HVKTQS) Smart(x) đúng nếu có người không thuộc HVKTQS!
  90. Tính chất của lượng từ • x y giống như y x • x y giống như y x • x y có thể khác y x • • x y Loves(x,y) – “Tồn tại người yêu tất cả mọi người trên thế giới” • y x Loves(x,y) – “Mọi người trên thế giới này đều có ít nhất một người yêu” • Đối ngẫu lượng từ: • x Likes(x,IceCream) x Likes(x,IceCream) • x Likes(x,Broccoli) x Likes(x,Broccoli)
  91. Phép Đồng Nhất • term1 = term2 là đúng trong một diễn dịch khi và chỉ khi term1 và term2 cùng tham chiếu đến một đối tượng • E.g., định nghĩa of Sibling dùng Parent: x,y Sibling(x,y) [(x = y)  m,f  (m = f)  Parent(m,x)  Parent(f,x)  Parent(m,y)  Parent(f,y)]
  92. Dùng LGVT cho biểu diễn tri thức Biểu diễn quan hệ huyết thống: (tiếng anh) • Brothers are sibling x,y Brother(x,y) Sibling(x,y) • One's mother is one's female parent m,c Mother(c) = m (Female(m)  Parent(m,c)) • “Sibling” is symmetric x,y Sibling(x,y) Sibling(y,x)
  93. Dùng LGVT cho biểu diễn tri thức Tri thức về tập hợp • s Set(s) (s = {} )  (x,s2 Set(s2)  s = {x|s2}) • x,s {x|s} = {} • x,s x s s = {x|s} • x,s x s [ y,s2} (s = {y|s2}  (x = y  x s2))] • s1,s2 s1  s2 (x x s1 x s2) • s1,s2 (s1 = s2) (s1  s2  s2  s1) • x,s1,s2 x (s1  s2) (x s1  x s2) • x,s1,s2 x (s1  s2) (x s1  x s2)
  94. Cơ sở tri thức trên Logic vị từ cho bài toán hang Wumpus • Quan sát – t,s,b Percept([s,b, Ánh kim],t) Có vàng (t) • Hành động: –  Ánh kim(t) BestAction(Chộp,t)
  95. Biểu diễn các tri thức ẩn • x,y,a,b Liền_kề ([x,y],[a,b]) [a,b] {[x+1,y], [x-1,y],[x,y+1],[x,y-1]} Ô có tiếng gió nếu gần ô có hầm chông: s Breezy(s) r Liền _Kề (r,s)  Hầm_chông (r) r Hầm_chông (r) [s Liền_kề (r,s) Có_tiếng_ gió (s) ]
  96. Biểu diễn tri thức trong LGVT 1. Xác định bài toán. 2. Thu thập tri thức liên quan. 3. Xác định vị từ, hàm, hằng 4. Biểu diễn tri thức chung về miền giá trị của bài toán 5. Biểu diễn tri thức cụ thể liên quan đến bài toán 6. Đặt câu hỏi để máy suy diễn tự lập luận và trả lời 7. Debug cơ sở tri thức.
  97. Ví dụ về mạch điện tử Bộ cộng 1 bit (có nhớ):
  98. Ví dụ về mạch điện tử 1. Xca định bài toán – Mạch có cộng chính xác? (Kiểm tra mạch) 2. Thu thập tri thức liên quan – Mạch gồm đường nối với các cổng logic; loại cổng (AND, OR, XOR, NOT) – không liên quan: kích thước, hình dạng, mầu sắc, chi phí của các loại cổng. 3. Xác định từ vựng (vị từ, hàm, hằng): Type(X1) = XOR Type(X1, XOR) XOR(X1)
  99. Ví dụ về mạch điện tử 4. Biểu diễn tri thức chung của miền giá trị bài toán – t1,t2 Connected(t1, t2) Signal(t1) = Signal(t2) – t Signal(t) = 1  Signal(t) = 0 – 1 ≠ 0 – t1,t2 Connected(t1, t2) Connected(t2, t1) – g Type(g) = OR Signal(Out(1,g)) = 1 n Signal(In(n,g)) = 1 – g Type(g) = AND Signal(Out(1,g)) = 0 n Signal(In(n,g)) = 0 – g Type(g) = XOR Signal(Out(1,g)) = 1 Signal(In(1,g)) ≠ Signal(In(2,g)) – g Type(g) = NOT Signal(Out(1,g)) ≠ Signal(In(1,g))
  100. Ví dụ về mạch điện tử 5. Biểu diễn tri thức liên quan trực tiếp đến bài toán. Type(X1) = XOR Type(X2) = XOR Type(A1) = AND Type(A2) = AND Type(O1) = OR Connected(Out(1,X1),In(1,X2)) Connected(In(1,C1),In(1,X1)) Connected(Out(1,X1),In(2,A2)) Connected(In(1,C1),In(1,A1)) Connected(Out(1,A2),In(1,O1)) Connected(In(2,C1),In(2,X1)) Connected(Out(1,A1),In(2,O1)) Connected(In(2,C1),In(2,A1)) Connected(Out(1,X2),Out(1,C1)) Connected(In(3,C1),In(2,X2)) Connected(Out(1,O1),Out(2,C1)) Connected(In(3,C1),In(1,A2))
  101. Ví dụ về mạch điện tử 6. Đặt câu hỏi cho máy suy diễn: Tập các giá trị đầu ra có thể với tập các giá trị vào có thể của mạch? i1,i2,i3,o1,o2 Signal(In(1,C_1)) = i1  Signal(In(2,C1)) = i2  Signal(In(3,C1)) = i3  Signal(Out(1,C1)) = o1  Signal(Out(2,C1)) = o2 7. Debug cơ sở tri thức Có thể quên biểu diễn 1 ≠ 0
  102. Tóm tắt • Logic vị từ (bậc 1): – Đối tượng ngữ nghĩa nguyên thuỷ là đối tượng và quan hệ. – Cú pháp: hằng, hàm, vị từ, đồng nhất, lượng từ. • Khả năng diễn đạt mạnh hơn logic mệnh đề: - đủ để biểu diễn tri thức cho bài toán hang Wumpus.
  103. Lập Luận Trên LGVT • Đưa lập luận trên LGVT về lập luận trên logic mệnh đề. • Phép hợp nhất (Unification) • Lập luận tam đoạn luận tổng quát. • Lập luận hướng tiến. • Lập luận hướng lùi. • Phép giải.
  104. Khởi trị cho phép lượng từ phổ dụng (UI) • Thế các biến bằng tất cả các hằng (đối tượng) trên model: v α Subst({v/g}, α) với mọi biến v term g. • E.g., x King(x)  Greedy(x) Evil(x) : King(John)  Greedy(John) Evil(John) King(Richard)  Greedy(Richard) Evil(Richard) King(Father(John))  Greedy(Father(John)) Evil(Father(John)) . .
  105. Khởi trị lượng từ tồn tại • Với mọi mệnh đề α, biến v, và ký hiệu hằng k không xuất hiện trong KB: v α Subst({v/k}, α) • E.g., x Crown(x)  OnHead(x,John) yields: Crown(C1)  OnHead(C1,John) Với C1 là một hằng, gọi là hằng Skolem
  106. Đưa về lập luận trên Logic mệnh đề Giải sử KB như sau: x King(x)  Greedy(x) Evil(x) King(John) Greedy(John) Brother(Richard,John) • Khởi trị cho lượng từ phổ dụng ta có: King(John)  Greedy(John) Evil(John) King(Richard)  Greedy(Richard) Evil(Richard) King(John) Greedy(John) Brother(Richard,John) • Cơ sở tri thưc đã được mệnh đề hoá: King(John), Greedy(John), Evil(John), King(Richard),
  107. Đưa về lập luận trên Logic mệnh đề • Mọi cơ sở tt biểu diễn bằng logic vị từ đều có thể mệnh đề hoá • ý tưởng: mệnh đề hoá cơ sở tri thức và câu hỏi, áp dụng phép giải, thu kết quả. • Hạn chế: Với ký hiệu hàm, có thể có vô hạn term tương ứng – e.g., Father(Father(Father(John)))
  108. Đưa về lập luận trên Logic mệnh đề Định lý: Herbrand (1930). mệnh đề α là dẫn được từ cơ sở tri thức LGVT KB, nếu nó dẫn được từ một tập con hữu hạn của cơ sở tri thức mệnh đề hoá từ KB. Do đó: For n = 0 to ∞ do Tạo cơ sở tri thức mệnh đề hoá từ KB khởi trị với các term có độ sâu n. Kiểm tra xem α có dẫn được từ cơ sở tri thức này không? (giống như làm trong logic mệnh đề) Hạn chế: sẽ kết thúc nếu α dẫn được, lặp vô tận nếu α không dẫn được. Định lý: Turing (1936), Church (1936) Bài toán dẫn được trong cơ sở tri thức dùng LGVT là nửa quyết định được (có thuật toán tồn tại để trả lời YES cho những mệnh đề dẫn được, nhưng không tồn tại thuật toán trả lời NO cho những mệnh đê không dẫn được.)
  109. Hạn chế của việc mệnh đề hoá • Mệnh đề hoá sinh ra rất nhiều những mệnh đề không liên quan đến quá trình suy diễn. • Ví dụ: x King(x)  Greedy(x) Evil(x) King(John) y Greedy(y) Brother(Richard,John) • Dễ thấy KB dẫn ra Evil(John), nhưng quá trình mệnh đề hoá dẫn tới nhiều mệnh đề chẳng liên quan như Greedy(Richard) • với p k-ary vị từ và n hằng số, có p·nk mệnh đề tương ứng.
  110. Phép hợp nhất • Có thể có phép suy luận đơn giản nếu tìm được phép thế θ sao cho King(x) và Greedy(x) khớp với King(John) và Greedy(y) θ = {x/John,y/John} • Unify(α,β) = θ if αθ = βθ p q θ Knows(John,x) Knows(John,Jane) Knows(John,x) Knows(y,OJ) Knows(John,x) Knows(y,Mother(y)) Knows(John,x) Knows(x,OJ)
  111. Phép hợp nhất p q θ Knows(John,x) Knows(John,Jane) {x/Jane}} Knows(John,x) Knows(y,OJ) Knows(John,x) Knows(y,Mother(y)) Knows(John,x) Knows(x,OJ)
  112. Phép hợp nhất p q θ Knows(John,x) Knows(John,Jane) {x/Jane}} Knows(John,x) Knows(y,OJ) {x/OJ,y/John}} Knows(John,x) Knows(y,Mother(y)) Knows(John,x) Knows(x,OJ)
  113. Phép hợp nhất p q θ Knows(John,x) Knows(John,Jane) {x/Jane}} Knows(John,x) Knows(y,OJ) {x/OJ,y/John}} Knows(John,x) Knows(y,Mother(y)) {y/John,x/Mother(John)}} Knows(John,x) Knows(x,OJ)
  114. Phép hợp nhất p q θ Knows(John,x) Knows(John,Jane) {x/Jane}} Knows(John,x) Knows(y,OJ) {x/OJ,y/John}} Knows(John,x) Knows(y,Mother(y)) {y/John,x/Mother(John)}} Knows(John,x) Knows(x,OJ) {fail}
  115. Phép hợp nhất • hợp nhất Knows(John,x) và Knows(y,z) cần có phép thế: θ = {y/John, x/z } or θ = {y/John, x/John, z/John} • Phép hợp nhất thứ nhất tổng quát hơn thứ hai. • Chỉ có một phép hợp nhất tổng quát nhất (MGU) (chỉ sai khác tên biến). MGU = { y/John, x/z }
  116. Thuật toán hợp nhất
  117. Thuật toán hợp nhất
  118. Tam đoạn luận tổng quát (GMP) p1', p2', , pn', ( p1  p2   pn q) qθ where pi'θ = pi θ for all i p1' is King(John) p1 is King(x) p2' is Greedy(y) p2 is Greedy(x) θ is {x/John,y/John} q is Evil(x) q θ is Evil(John) • GMP sử dụng các câu có tối đa một literal dương (câu dạng Horn) • Tất cả các biến chỉ chưa lượng từ phổ dụng.
  119. Ví dụ • Theo luật lệ nếu một người Mỹ bán vũ khí cho quốc gia thù địch với nước Mỹ thì bị coi là phạm tội. Nước Nono, là kẻ thù của nước Mỹ, Nono có tên lửa, và tất cả tên lửa của nước này đều mua của đại tá West, Một người Mỹ. • Chứng minh đại tá West có tội.
  120. Ví dụ một người Mỹ bán vũ khí cho quốc gia thù nghịch là có tội: American(x)  Weapon(y)  Sells(x,y,z)  Hostile(z) Criminal(x) Nono có tên lửa, i.e., x Owns(Nono,x)  Missile(x): Owns(Nono,M1) and Missile(M1) Tất cả tên lửa đều do đại tá West bán: Missile(x)  Owns(Nono,x) Sells(West,x,Nono) Tên lửa là vũ khí: Missile(x) Weapon(x) Kẻ thù của nước Mỹ được gọi là “thù nghịch “: Enemy(x,America) Hostile(x) West là một người Mỹ American(West) Nước Nono lè kẻ thù của Mỹ Enemy(Nono,America)
  121. Thuật toán lập luận hướng tiến
  122. Chứng Minh Với Lập Luận Hướng Tiến
  123. Chứng Minh Với Lập Luận Hướng Tiến
  124. Chứng Minh Với Lập Luận Hướng Tiến
  125. Đặc điểm của lập luận hướng tiến • Chặt và đủ đối với các KB dùng logic vị từ bậc 1. • Datalog = Các câu Horn bậc 1 + không dùng hàm • FC kết thúc với Datalogsau một số hữu hạn bước lặp. • Có thể không dừng nếu α không dẫn được. • Thường dùng trong Deductive Database • Nhắc lại: Bài toán suy dẫn trên câu dạng Horn là nửa quyết định được.
  126. Thuật Toán Lập Luận Lùi SUBST(COMPOSE(θ1, θ2), p) = SUBST(θ2, SUBST(θ1, p))
  127. Đặc điểm của lập luận lùi • Tìm kiếm đệ quy theo chiều sâu. Không gian nhớ tuyến tính với độ dài chứng minh. • Không đầy đủ do có thể rơi vào vòng lặp vô tận • Không hiệu quả dó có thể có các subgoals lặp đi lặp lại . • Dùng trong lập trình Logic (logic programming)
  128. Lập Trình Logic: Prolog • Chương trình = Logic + Control • Cơ bản: Dùng lập luận lùi với các câu dạng Horn • Dùng tại Châu âu, Nhật bản (Ngôn ngữ máy cho thế hệ thứ 5) • Program = set of clauses = head :- literal1, literaln. criminal(X) :- american(X), weapon(Y), sells(X,Y,Z), hostile(Z). • Lập luận lùi với chiến lược tìm kiếm Depth-first, left-to-right • Các vị từ có sẵn etc., e.g., X is Y*Z+3 • Các vị từ có sẵn tạo hiệu ứng lề (input and output predicates, assert/retract predicates) • Giả thiết đóng (Phủ định được gán bằng thất bại - "negation as failure"). – e.g., alive(X) :- not dead(X). – alive(joe) thành công nếu dead(joe) thất bại (không chứng minh được)
  129. Prolog • Ghép nối hai danh sách: append([],Y,Y). append([X|L],Y,[X|Z]) :- append(L,Y,Z). • query: append(A,B,[1,2]) ? • answers: A=[] B=[1,2] A=[1] B=[2] A=[1,2] B=[]
  130. Phép Giải: Tóm tắt • Trên LGVT bậc 1: l1  ···  lk, m1  ···  mn (l1  ···  li-1  li+1  ···  lk  m1  ···  mj-1  mj+1  ···  mn)θ trong đó Unify(li, mj) = θ. • Hai câu độc lập được đổi tên biến sao cho chúng không chung biến (tránh gây nhập nhằng) • VD: Rich(x)  Unhappy(x) Rich(Ken) Unhappy(Ken) với θ = {x/Ken} • Dùng phép giải trên công thức dạng CNF(KB  α); • Đầy đủ đối với Logic vị từ.
  131. Đổi sang dạng CNF • Tất cả những ai yêu động vật thì được người khác yêu: x [y Animal(y) Loves(x,y)] [y Loves(y,x)] • 1. Khử dấu tương đương và kéo theo: x [y Animal(y)  Loves(x,y)]  [y Loves(y,x)] • 2. Chuyển  vào trong: x p ≡ x p,  x p ≡ x p x [y (Animal(y)  Loves(x,y))]  [y Loves(y,x)] x [y Animal(y)  Loves(x,y)]  [y Loves(y,x)] x [y Animal(y)  Loves(x,y)]  [y Loves(y,x)]
  132. Đổi sang dạng CNF 3. Chuẩn hoá biến sao cho mỗi lượng từ gắn với 1 biến: x [y Animal(y)  Loves(x,y)]  [z Loves(z,x)] 4. Skolem hoá để khử lượng từ tồn tại mỗi biến thuộc lượng từ tt được thay bằng một hàm Skolem function của các biến gắn lượng từ phổ dụng khác: x [Animal(F(x))  Loves(x,F(x))]  Loves(G(x),x) 5. Xoá bỏ lượng từ phổ dụng: [Animal(F(x))  Loves(x,F(x))]  Loves(G(x),x) 6. Áp dụng luật phấn phối với  và  : [Animal(F(x))  Loves(G(x),x)]  [Loves(x,F(x))  Loves(G(x),x)]
  133. Chứng minh dựa vào phép giải (Proof Tree)
  134. Đọc thêm • Sách giáo trình: – Chương 8,9. • Open Courseware: – Ch9, ch10, ch11 • Logic toán: – A Mathematical Introduction to Logic, Hebert B. Ederton; – Introduction to Mathematical Logic, Mendenson; – Mathematical Logic, Y.L. Ershov và E.A. Palyutin. • Phép giải và lập luận tự động: – Symbolic Logic and Mechanical Theorem Proving, C.L. Chang and C.T. Lee. – Automated Reasoning, L. Wos et al. • LOGIC PROGRAMMING và PROLOG: – Foundations of Logic Programming, J. W. Lloyd – Logic, Programming and PROLOG, U. Nilsson. – PROLOG: Programming for Artificial Intelligence, I. Bratko
  135. Ôn tập 1. Nêu ưu/nhược điểm của logic mệnh đề. 2. Nêu cú pháp, ngữ nghĩa của Logic vị từ. 3. Nêu phương pháp mệnh đề hoá LGVT. 4. Định nghĩa phép hợp nhất và cài đặt thuật toán tìm phép hợp nhất khái quát nhất trong LGVT. 5. Cài đặt Lập luận tiến/lùi trên Logic vị từ. 6. Đưa công thức logic vị từ về dạng CNF. 7. Cài đặt phép giải trên Logic vị từ. 8. Xây dựng cơ sở tri thức cho bài toán hang wumpus dùng logic vị từ cài đặt chương trình.