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

7. Thuật toán suy diễn dựa trên luật phân giải

Để khắc phục nhược điểm độ phức tạp thời gian của giải thuật suy diễn dựa trên liệt kê ở trên, chúng ta đưa ra thuật giải nhanh hơn, thời gian thực hiện nhanh hơn. Giải thuật dựa trên thực hiện liên tiếp các luật phân giải trên các câu dạng chuẩn hội. Để chứng minh KB ╞ q ta sẽ chứng minh điều tương đương là (KB ∧ ¬q╞ []), tức là như chúng ta vẫn gọi là chứng minh bằng phản chứng: giả sử q không đúng (¬q), khi đó KB ∧ ¬q sẽ dẫn đến mâu thuẫn, tức là (KB ∧ ¬q)╞ []. Chúng ta sẽ chuyển (KB ∧ ¬q) về dạng chuẩn hội, tức là hội các clause, hay chúng ta chuyển KB và ¬q thành hội các clause, sau đó áp dụng liên tiếp luật phân giải (mục