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

4) trên các cặp clause mà có ít nhất một literal đối của nhau để sinh ra một clause mới, clause mới này lại bổ sung vào danh sách các clause đã có rồi lặp lại áp dụng luật phân giải. Giải thuật dừng khi có câu [] được sinh ra (khi đó ta kết luận KB ╞ q) hoặc không có clause nào được sinh ra (khi đó ta kết luận KB không suy diễn được ra q). Chi tiết thuật giải cho trong hình ở trang sau. Giải thuật phân giải là giải thuật đầy đủ vì tất cả các câu trong logic mệnh đề đều có thể biểu diễn được dưới dạng hội của các clauses (dạng chuẩn hội). Tuy nhiên mỗi lần phân giải sinh ra clause mới thì lại bổ sung vào danh sách các clauses để thực hiện tìm kiếm các cặp clauses phân giải được với nhau; vì vậy số lượng clauses ở lần lặp sau lại tăng lên so với lần lặp trước, dẫn đến việc tìm kiếm các clauses phân giải được với nhau là khó khăn hơn. Giải thuật phân giải trình bày như trên là giải thuật suy phân giải tiến, có nghĩa là từ trạng thái đầu KB ∧ ¬q thực hiện các thao tác chuyển trạng thái (áp dụng luật phân giải trên cặp các clauses để sinh ra clauses mới và bổ sung vào danh sách các clauses hiện có) để sinh ra trạng thái mới, đến khi nào trạng thái mới chứa câu [] (trạng thái đích) thì dừng hoặc không sinh ra trạng thái mới được nữa. Một cách khác để thực hiện suy diễn phân giải KB ╞ q là xuất phát từ clause ¬q (coi như trạng thái đích) ta thực hiện phân giải với các clauses khác trong KB để sinh ra clauses mới, rồi từ các clauses mới này thực hiện tiếp với các clauses khác của KB để sinh ra clauses mới hơn, đến khi nào [] được sinh ra hoặc không sinh ra được clause mới thì dừng. Nói cách khác là chỉ thực hiện phân giải các clauses liên quan đến q. Giải thuật phân giải lùi sẽ làm việc hiệu quả hơn giải thuật phân giải tiến (chi tiết cài đặt coi như là bài tập). Function Resolution(KB, q) return true or false clauses=get_list_of_clauses(KB ∧ ¬q); new={}; do for each Ci, Cj in clauses new_clause= resol(Ci,Cj); if new_clause=[] return true; new=new Υ new_clause; if new⊆clauses return false; clauses=clauses Υ new;