SUY DIỄN VỚI LOGIC BẬC SUY DIỄN VỚI LOGIC BẬC NHẤTNHẤT

Tô Hoài Việt Khoa Công nghệ Thông tin Đại học Khoa học Tự nhiên TPHCM thviet@fit.hcmuns.edu.vn

1

Tổng quát Tổng quát

• Cơ sở của hợp giải trên logic bậc nhất • Hợp giải trên logic bậc nhất • Các ví dụ • Suy diễn tiến và suy diễn lùi • Thuật giải suy diễn tiến • Thuật giải suy diễn lùi

2

Cơ sở của hợp giải FOL Cơ sở của hợp giải FOL

• Hợp giải (Robinson): để chứng minh một tập KB có suy

hay không, viết lại KB (cid:0) (cid:0)

dẫn logic được một câu (cid:0) 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))  (cid:0) = {x/A}

3

(cid:0)

Ví dụVí dụ

Chứng minh rằng (P(x) (cid:0)

Q(x)) và P(A) suy dẫn logic

(cid:0) z.Q(z)

Tiền đề Tiền đề Kết luận

1. (cid:0) P(x) (cid:0) Q(x) 2. P(A) 3. (cid:0) Q(z) 4. (cid:0) P(z)

1, 3

= {x/z}

(cid:0)

5. False

2, 4

= {x/z, z/A}

4

(cid:0)

Ví dụ (tt) Ví dụ (tt)

Q(x)) và P(A) và P(B), tìm z sao cho Q(z)

Cho trước (P(x) (cid:0)

là đúng

Tiền đề Tiền đề Tiền đề Kết luận 1, 4

= {x/z}

(cid:0)

1. (cid:0) P(x) (cid:0) Q(x) 2. P(A) 3. P(B) 4. (cid:0) Q(z) 5. (cid:0) P(z) 6. False

2, 5

= {x/z, z/A}

(cid:0)

7. False

3, 5

= {x/z, z/B}

5

(cid:0)

Ví dụ Quan hệ họ hàng Ví dụ Quan hệ họ hàng

Art là cha của Bob và Bud. Bob là cha của Cal và Coe. Ông nội là cha của cha.

6

F(Art, Bob) F(Art, Bud) F(Bob, Cal) F(Bob, Coe) F(x, y) (cid:0) F(y,z) (cid:0) G(x,z)

Art có phải là Ông của Coe? Art có phải là Ông của Coe?

7

1. F(Art, Bob) 2. F(Art, Bud) 3. F(Bob, Cal) 4. F(Bob, Coe) 5. (cid:0) F(x, y) (cid:0) (cid:0) F(y,z) (cid:0) G(x,z) 6. (cid:0) G(Art, Coe) 7. (cid:0) F(Art, y) (cid:0) (cid:0) F(y,Coe) 8. (cid:0) F(Art, Bob) 9. False 5, 6 4, 7 1, 8 Tiền đề Tiền đề Tiền đề Tiền đề Tiền đề Kết luận (cid:0) ={x/Art, z/Coe} (cid:0) ={x/Art, z/Coe, y/Bob} (cid:0) ={x/Art, z/Coe, y/Bob}

Ai là Ông của Coe? Ai là Ông của Coe?

5, 6

1. F(Art, Bob) 2. F(Art, Bud) 3. F(Bob, Cal) 4. F(Bob, Coe) 5. (cid:0) F(x, y) (cid:0) (cid:0) F(y,z) (cid:0) G(x,z) 6. (cid:0) G(x2, Coe) 7. (cid:0) F(x2, y) (cid:0) (cid:0) F(y,Coe) 8. (cid:0) F(Bob, Coe) 1, 7

8

9. False 4, 8 Tiền đề Tiền đề Tiền đề Tiền đề Tiền đề Kết luận (cid:0) = {z/ Coe, x/x2} (cid:0) = {z/ Coe, x/x2, x2/ Art, y/ Bob} (cid:0) = {z/ Coe, x/x2, x2/ Art, y/ Bob}

Ai là Cháu của Art? Ai là Cháu của Art?

5, 6

1, 7

2, 7

1. F(Art, Bob) 2. F(Art, Bud) 3. F(Bob, Cal) 4. F(Bob, Coe) 5. (cid:0) F(x, y) (cid:0) (cid:0) F(y,z) (cid:0) G(x,z) 6. (cid:0) G(Art, z2) 7. (cid:0) F(Art, y) (cid:0) (cid:0) F(y,z2) 8. (cid:0) F(Bob, z2) 9. (cid:0) F(Bud, z2) 10. False 3, 8

9

11. False 4, 8 Tiền đề Tiền đề Tiền đề Tiền đề Tiền đề Kết luận (cid:0) = {x/Art, z/z2} (cid:0) = {x/Art, z/z2,, y/Bob} (cid:0) = {x/Art, z/z2, y/Bud} (cid:0) = {x/Art, z/z2, y/Bob, z2/Cal} (cid:0) = {x/Art, z/z2, y/Bob, z2/Coe}

Ông và cháu? Ông và cháu?

10

1. F(Art, Bob) 2. F(Art, Bud) 3. F(Bob, Cal) 4. F(Bob, Coe) 5. (cid:0) F(x, y) (cid:0) (cid:0) F(y,z) (cid:0) G(x,z) 6. (cid:0) G(x, z) 7. (cid:0) F(x, y) (cid:0) (cid:0) F(y,z) 8. (cid:0) F(Bob, z) 9. (cid:0) F(Bud, z) 10. False 11. False 5, 6 1, 7 2, 7 3, 8 4, 8 Tiền đề Tiền đề Tiền đề Tiền đề Tiền đề Kết luận (cid:0) = {} (cid:0) = {x/Art, y/Bob} (cid:0) = {x/Art, y/Bud} (cid:0) = {x/Art, y/Bob, z/Cal} (cid:0) = {x/Art, y/Bob, z/Coe}

Suy diễn tiến và suy diễn lùi Suy diễn tiến và suy diễn lùi

• Suy 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 Horn

• Biểu thức dạng Horn: trong biểu thức có nhiều nhất một

literal khẳng định p1 (cid:0) (cid:0) p2

(cid:0) (cid:0) p3 (cid:0) … (cid:0) (cid:0) pn

• Hay dạng luật (luật sinh)

p2

(cid:0) p3 (cid:0) … (cid:0) pn

p1

11

(cid:0)

Thuật toán Suy diễn Tiến Thuật toán Suy diễn Tiến

FOL-FC-Ask(KB,(cid:0) ){

repeat until new là rỗng

// r ở dạng chuẩn hóa (p1 (cid:0) … (cid:0) pn => q)

new  {} với mọi câu r trong KB với mọi phép thế (cid:0) sao cho (p1 (cid:0) … (cid:0) pn)(cid:0) = (p’1 (cid:0) … (cid:0) p’n)(cid:0)

với p’1,…,p’n nào đó trong KB

q’  Subst((cid:0) ,q)

if q’ không phải là một câu đã có trong KB hay new then

(cid:0)

thêm q’ vào new  Unify(q’, (cid:0) ) if (cid:0) thành công then return (cid:0)

thêm new vào KB

return false

}

12

Ví dụ Quan hệ họ hàng Ví dụ Quan hệ họ hàng

P(x,y) P(x,y)

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) (cid:0) 9. F(x,y) (cid:0) 10. P(x, y) (cid:0) P(y,z) (cid:0)

G(x,z)

13

Ví dụ Suy diễn tiến Ví dụ Suy diễn tiến

8. M(x,y) (cid:0)

P(x,y)

M(Ave,Bee)

(cid:0)

M(Bee,Cal)

(cid:0)

M(Bee,Coe)

1 = {x/Ave, y/Bee} q’ = P(Ave, Bee) 2 = {x/Bee, y/Cal} q’ = P(Bee,Cal) 3 = {x/Bee, y/Coe} q’ = P(Bee,Coe)

14

(cid:0)

Ví dụ Suy diễn tiến (tt) Ví dụ Suy diễn tiến (tt)

9. F(x,y) (cid:0)

P(x,y)

F(Art,Bob)

(cid:0)

F(Art,Bud)

(cid:0)

F(Bob,Cal)

(cid:0)

F(Bob,Coe)

1 = {x/Art, y/Bob} q’ = P(Art,Bob) 2 = {x/Art, y/Bud} q’ = P(Art,Bud) 3 = {x/Bob, y/Cal} q’ = P(Bob,Cal) 4 = {x/Bob, y/Coe} q’ = P(Bob,Coe)

15

(cid:0)

Ví dụ Suy diễn tiến (tt) Ví dụ Suy diễn tiến (tt)

10. P(x, y) (cid:0) P(y,z) (cid:0)

P(Ave,Bee) (cid:0) P(Bee,Cal)

(cid:0)

P(Ave,Bee) (cid:0) P(Bee,Coe)

(cid:0)

P(Art,Bob) (cid:0) P(Bob,Cal)

(cid:0)

P(Art,Bob) (cid:0) P(Bob,Coe)

G(x,z) 1 = {x/Ave,y/Bee,z/Cal} q’ = G(Ave, Cal) 2 = {x/Ave,y/Bee,z/Coe} q’ = G(Ave, Coe) 3 = {x/Art, y/Bob, z/Cal} q’ = G(Art, Cal) 4 = {x/Art, y/Bob, z/Coe} q’ = G(Art, Coe)

16

(cid:0)

Thuật toán Suy diễn Lùi Thuật toán Suy diễn Lùi

FOL-BC-ASK(KB, goals, (cid:0) ){ 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 (cid:0) , 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

q) if goals rỗng then return {(cid:0) } q’  SUBST((cid:0) , first(goals)) for each r trong KB mà r có dạng chuẩn (p1 (cid:0) … (cid:0) pn (cid:0)

và (cid:0) ’  UNIFY(q, q’) thành công

(cid:0) ’)) (cid:0) ans

ans  FOL-BC-ASK(KB, [p1,…,pn| REST(goals)], (cid:0) (cid:0) return ans

17

}

Ví dụ Suy diễn lùi Ví dụ Suy diễn lùi

(cid:0) // P(x,y) (cid:0) P(y,z) (cid:0) G(x ,z)

Ask(G(Art,Cal), {}) q’ = G(Art,Cal) ’ = {x/Art,z/Cal} Ask({P(x,y},P(y,z)},{x/Art,z/Cal})

(cid:0) // F(x2,y2) (cid:0) P(x2,y2)

q’ = P(Art,y) ’ = {x2/Art,y/y2} Ask({F(x2,y2),P(y,z)}, {x/Art,z/Cal,x2/Art}}

(cid:0) // F(Art,Bob)

q’ = F(Art,y2) ’ = {y2/Bob} Ask({P(y,z)}, {x/Art,z/Cal,x2/Art,y2/Bob,y/y2})

(cid:0) // F(x3,y3) (cid:0) P(x3,y3)

18

q’ = P(Bob,Cal) ’ = {x3/Bob,y3/Cal} Ask({F(x3,y3)}, {…x3/Bob,y3/Cal}  ans

Ví dụ Suy diễn lùi (tt) Ví dụ Suy diễn lùi (tt)

(cid:0) Ask(G(Art,z), {}) q’ = G(Art,z) ’ = {x/Art} // P(x,y) (cid:0) P(y,z) (cid:0) G(x,z)

Ask({P(x,y),P(y,z)},{x/Art})

(cid:0) q’ = P(Art,y) ’ = {x/Art} // F(x,y) (cid:0) P(x,y)

Ask({F(x,y),P(y,z)}, {x/Art})

q’ = F(Art,y)

(cid:0) ’ = {x/Art,y/Bob} // F(Art,Bob)

Ask({P(y,z)}, {x/Art, y/Bob})

19

(cid:0) q’ = P(Bob,z) ’ = {x2/Bob, y2/z} // F(x2,y2) (cid:0) P(x2,y2)

Ví dụ Suy diễn lùi (tt) Ví dụ Suy diễn lùi (tt)

Ask(G(Art,z), {})

Ask({F(x2,y2)}, {…x2/Bob, y2/z})

(cid:0) q’ = F(Bob,z) ’ = {z/Cal} // F(Bob,Cal)

Ask({}, {…z/Cal})  ans

(cid:0) ’ = {z/Coe} // F(Bob,Cal)

Ask({}, {…z/Coe})  ans

’ = {x/Art} Ask({M(x,y),P(y,z)}, {x/Art}}

(cid:0) // M(x,y) (cid:0) P(x,y)

20

q’ = M(Art,y)  false

Đặc điểm của suy diễn lùi Đặc điểm của suy diễn lùi

• Tì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 minh

• Không đầy đủ do lặp vô tận

– Giải pháp: Kiểm tra trạng thái hiện tại với mọi trạng thái đang có

• Khô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

trong stack

• Được dùng nhiều trong lập trình logic (ngôn ngữ Prolog)

21

qua

Điều cần nắm Điều cần nắm

• Cá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