CHƯƠNG 6 – CÁC PHƯƠNG PHÁP LẬP LUẬN TRÊN LOGIC MỆNH ĐỀ

8. Thuật toán suy diễn tiến, lùi dựa trên các câu Horn

Như ta đã thấy trong mục 5, luật Modus ponens là đóng trong các câu dạng Horn dương, có nghĩa là nếu hai câu dạng Horn dương thỏa mãn các điều kiện của luật Modus ponens thì sẽ sinh ra câu dạng Horn dương mới. Nếu chúng ta biểu diễn được KB và q bằng các câu dạng Horn dương thì có thể sử dụng luật Modus ponens để suy diễn. Khi KB biểu diễn bằng hội các câu Horn dương, chúng ta các câu Horn dương này thành 2 loại: (1) câu có đúng một literal dương mà không có literal âm nào, đây là các câu đơn hay là các ký hiệu mệnh đề; (2) câu có đúng một literal dương và có ít nhất một literal âm, đây là các câu kéo theo mà phần thân của phép kéo theo chỉ là một ký hiệu mệnh đề. Có hai cách cài đặt thuật giải suy diễn dựa trên luật Modus ponens trên các câu Horn dương. Cách thứ nhất là bắt đầu từ các ký hiệu mệnh đề được cho là đúng trong KB, áp dụng liên tiếp các luật Modus ponens trên các câu kéo theo trong KB để suy diễn ra các ký hiệu mới, đến khi nào danh sách các hiệu được suy diễn ra chứa ký hiệu đích q thì dừng và thông báo suy diễn thành công. Nếu danh sách các ký hiệu suy diễn không chứa q và cũng không thể sinh tiếp được nữa thì thông báo suy diễn thất bại. Cách suy diễn này gọi là suy diễn tiến (hay suy diễn tam đoạn luận tiến để phân biệt với suy diễn phân giải tiến ở trên). Chi tiết giải thuật cho trong bảng ở phía dưới. Giải thuật sử dụng danh sách các ký hiệu mệnh đề được xác định là true, true_symbols , danh sách này khởi tạo từ các ký hiệu độc lập trong KB, sau đó bổ sung khi một ký hiệu mệnh đề được suy diễn ra là true, đến khi nào danh sách chưa ký hiệu truy vấn q thì dừng hoặc không bổ sung được ký hiệu nào nữa vào danh sách này. Cách cài đặt thứ hai là xuất phát từ đích q, chúng ta xem có bao nhiêu câu Horn kéo theo nào trong KB có q là phần đầu của luật kéo theo, chúng ta lại kiểm tra xem các ký hiệu mệnh đề nằm trong phần điều kiện của các luật này (các đích trung gian) xem có suy diễn được từ KB không, cứ áp dụng ngược các luật đến khi nào các đích trung gian được xác nhận là đúng trong KB thì kết luận suy diễn thành công, hoặc kết luận không thành công khi có tất cả các nhánh đều không chứng minh được các đích trung gian không suy diễn được từ KB. Giải thuật này gọi là giải thật suy diễn lùi (hoặc là giải thuật suy diễn tam đoạn luận lùi). Function Forward_Horn(KB, q) return true or false Input: - KB tập các câu Horn dương, đánh số clause

1

, .., clause

n

- q: câu truy vấn dạng câu đơn (ký hiệu mệnh đề) Output: true or false Các biến địa phương: - Int count[0.. n], count[i] là số ký hiệu xuất hiện trong phần điều kiện của clause

i

. - Bool proved[danhsach_kyhieu]: proved[kyhieu]=1 nếu kyhieu đã được chứng minh là suy diễn được từ KB, ngược lại =0; ban đầu khởi tạo=0 với mọi ký hiệu - working_symbols: danh sách ký hiệu đang xem xét, khởi đầu bằng danh sách các ký hiệu độc lập trong KB while working_symbols is not empty p= pop(working_symbols); if (!proved[p]) proved[p]=1; for each clause

i

whose p appears count[clause

i

] = count[clause

i

] -1; if count[clause

i

]==0 if head[clause

i

]==q return true; push (head[clause

i

], working_symbols); return false;