GIỚI THIỆU:
Như đã giới thiệu trong chương I, suy luận tự động có thể xem là nhánh nghiên cứu lâu đời nhất của AI, bắt nguồn từ Logic Theorist và General Problem Solver của Newell và Simon.
Sức hấp dẫn của suy luận tự động nằm trong tính chặt chẽ và tổng quát của logic. Bởi vì logic là một hệ thống hình thức, nên ta có thể tự động hóa nó. Rất nhiều vấn đề khác nhau có thể giải quyết được bằng cách biểu diễn các mô tả vấn đề và các thông tin liên quan ở dạng các tiên đề luận lý và xem bài toán như là các định lý cần chứng minh.
Nổ lực của các nhà khoa học trong lĩnh vực này là tự động hóa quá trình chứng minh các định lý dựa vào các tiên đề cơ sở. Mặc dù cho đến nay vẫn chưa đạt được mục tiêu ban đầu, nhưng nhánh nghiên cứu này đã tạo ra nhiều kết quả rất quan trọng trong việc hình thức hóa các giải thuật tìm kiếm và phát triển các ngôn ngữ biểu diễn hình thức như Đại số quan hệ mà ta đã học ở chương II.
Trong chương này ta sẽ tiếp tục khảo sát một trong những thành quả của lĩnh vực này, đó là phương pháp chứng minh Hợp Giải (resolution). Một ứng dụng quan trọng của hợp giải đó là làm nền tảng cho trình thông dịch của ngôn ngữ PROLOG đang được sử dụng hiện nay.
Hợp giải là một kỹ thuật chứng minh định lý được biểu diễn bằng đại số mệnh đề hay đại số vị từ. Hợp giải được phát triển vào giữa thập niên 60 do Robinson đề xướng. Hợp giải sử dụng phản chứng để chứng minh một vấn đề. Hay nói cách khác, để chứng minh một câu (nghĩa là chứng minh câu này đúng), hợp giải sẽ chỉ ra rằng phủ định của câu sẽ tạo ra một mâu thuẫn với các câu đã biết. Tiếp cận này trái ngược với kỹ thuật mà chúng ta đã sử dụng để chứng minh ở chương II, chương III, tức là sử dụng phép dẫn xuất để chứng minh.
Trước khi đi vào phương pháp chứng minh hợp giải, chúng ta sẽ xem một ví dụ sử dụng Logic Vị Từ để biểu diễn tri thức và sử dụng phép dẫn xuất ở chương II để chứng minh.
Thí dụ 8.1: Xét ví dụ với tập hợp các câu như sau:
- Marcus was a man.
- Marcus was a Pompeian.
- All Pompeians were Romans.
- Caesar was a ruler.
- All Romans were either loyal to Caesar or hated him.
- Everyone is loyal to someone.
- People only try to assasinate rulers they are not loyal to.
- Marcus tried to assasinate Caesar.
Hãy chứng minh ‘Was Marcus loyal to Caesar?’
Các câu trên có thể được biểu diễn dưới dạng các câu hay công thức dạng chuẩn (wff) trong ngôn ngữ Phép tính vị từ như sau:
Để chứng minh mục tiêu trên, chúng ta sử dụng luật suy diễn để biến đổi thành mục tiêu mới (hay nhiều mục tiêu con mới), và cứ tiếp tục cho đến khi không còn mục tiêu nào chưa thỏa mãn.
Quá trình này có thể biểu diễn bằng một đồ thị AND/OR. Ở đây, để đơn giản ta chỉ vẽ một đường duy nhất.
Hình bên dưới minh họa một cách chứng minh cho mục tiêu trên:
∀X man (X) ∨ woman (X) → person(X)
Với câu 9 vừa thêm vào, ta có thể chứng minh thành công mục tiêu trên.
Từ chứng minh trên, chúng ta có nhận xét như sau:
- Thậm chí các kết luận rất đơn giản cũng đòi hỏi phải chứng minh qua nhiều bước.
- Quá trình tạo ra một chứng minh có liên quan đến nhiều quá trình khác nhau như quá trình đối sánh, thay thế, áp dụng luật Modus Ponens. Quá trình này sẽ phức tạp hơn nếu như các luật có nhiều từ hai mục ở vế phải hay vế trái gồm nhiều biểu thức phức tạp And hay Or với nhau.
Từ những nhận xét này cho thấy việc xây dựng một chương trình có thể chứng minh được như con người là không dễ dàng chút nào. Vì vậy, ta cần một phương pháp chứng minh đơn giản hơn. Và Hợp Giải (resolution) ra đời như là một công cụ chứng minh hiện đại và mạnh mẽ hơn cho ngành suy luận tự động. Sự đơn giản trong phép chứng minh của hợp giải xuất phát từ nguyên nhân: Thay vì suy luận trên các câu vị từ, hợp giải thao tác trên các câu đã được chuyển thành một dạng chuẩn trước khi bắt đầu quá trình chứng minh để làm giảm tính phức tạp của vấn đề. Phần còn lại của chương này sẽ giới thiệu về thủ tục Hợp giải này.
Download slide bài giảng tại đây