Một số thuật giải liên quan đến logic mệnh đề

Một trong những vấn đề khá quan trọng của logic mệnh đề là chứng minh tính đúng đắn của phép suy diễn (a → b). Đây cũng chính là bài toán chứng minh thường gặp trong toán học.

Rõ ràng rằng với hai phép suy luận cơ bản của logic mệnh đề (Modus Ponens, Modus Tollens) cộng với các phép biến đổi hình thức, ta cũng có thể chứng minh được phép suy diễn. Tuy nhiên, thao tác biến đối hình thức là rất khó cài đặt được trên máy tính. Thậm chí điều này còn khó khăn với cả con người!

Với công cụ máy tính, bạn có thể cho rằng ta sẽ dễ dàng chứng minh được mọi bài toán bằng một phương pháp "thô bạo" là lập bảng chân trị . Tuy về lý thuyết, phương pháp lập bảng chân trị luôn cho được kết quả cuối cùng nhưng độ phức tạp của phương pháp này là quá lớn, O(2ⁿ) với n là số biến mệnh đề. Sau đây chúng ta sẽ nghiên cứu hai phương pháp chứng minh mệnh đề với độ phức tạp chỉ có O(n).

Thuật giải Vương Hạo

Thuật giải Robinson

Thuật giải này hoạt động dựa trên phương pháp chứng minh phản chứng.

Phương pháp chứng minh phản chứng

Chứng minh phép suy luận (a → b) là đúng (với a là giả thiết, b là kết luận).

Phản chứng : giả sử b sai suy ra  b là đúng.

Bài toán được chứng minh nếu a đúng và  b đúng sinh ra một mâu thuẫn.

Ví dụ : Chứng minh rằng

B4 : Có tất cả 6 mệnh đề nhưng chưa có mệnh đề nào đối ngẫu nhau.

B5 : ⇒tuyển một cặp mệnh đề (chọn hai mệnh đề có biến đối ngẫu). Chọn hai mệnh đề đầu :