Nhập môn Trí tuệ nhân tạo

NHẬP MÔN TRÍ TUỆ NHÂN TẠO
@copyrights by Dr Nguyễn Xuân Hoài
Biểu Diễn Tri Thức và Lập Luận dựa trên Logic mệnh đề
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
Cơ Sở Tri Thức
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ích hợp trên cơ sở suy diễn.
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.
Đặ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ó
Ví dụ
Ví dụ
Ví dụ
Ví dụ
Ví dụ
Ví dụ
Ví dụ
Ví dụ
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
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.
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(α)
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
Ví dụ
Ví dụ
KB = luật + quan sát, tiếp nhận từ môi trường
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
Ví dụ
KB = luật + quan sát tiếp nhận từ môi trường
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
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 α
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 đề
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:

P1,2  (P2,2  P3,1) = true  (true  false) = true  true = true
Bảng giá trị luận lý
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)
Lập Luận Dựa Trên Bảng Luận Lý
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)
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 β╞ α
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.
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 đủ)

Phép Giải
Chuyển công thức sang dạng CNF
B1,1  (P1,2  P2,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 :
(B1,1  P1,2  P2,1)  ((P1,2  P2,1)  B1,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)
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
Ví dụ
KB = (B1,1  (P1,2 P2,1))  B1,1 α = P1,2
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.
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)
Thuật Toán cho lập luận tiến
Lập luận tiến là chặt & đủ đối vớicác KB dạng Horn
Ví dụ minh hoạ
Ví dụ minh hoạ
Ví dụ minh hoạ
Ví dụ minh hoạ
Ví dụ minh hoạ
Ví dụ minh hoạ
Ví dụ minh hoạ
Ví dụ minh hoạ
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�