Bài viết sưu tầm

1. Vương Hạo là ai?

Vương Hạo (Hao Wang, 1921–1995) là một nhà toán học và logic học người Mỹ gốc Trung Quốc, nổi tiếng với những đóng góp quan trọng trong:

• Logic toán học

• Nền tảng của toán học

• Tự động hóa chứng minh

• Phân tích các ý tưởng của Kurt Gödel

Ông từng làm việc tại Harvard, sau đó tại IBM, nơi ông nghiên cứu các thuật toán và chương trình tự động chứng minh mệnh đề bằng máy tính — một trong những nền móng của ngành Automated Theorem Proving ngày nay.

2. Đóng góp nổi bật

Trong các đóng góp của mình, Vương Hạo được biết đến nhiều nhất nhờ:

✔ Thuật toán chứng minh logic mệnh đề — Wang Algorithm (1957)

Đây là một phương pháp cơ học, có thể lập trình để máy tính tự động kiểm tra một công thức logic là đúng hay sai.

Thuật toán này được xem như một trong những hệ thống suy diễn tự động đầu tiên trên thế giới.

3. Ý tưởng của thuật toán Vương Hạo

Thuật toán dựa trên một ý tưởng trung tâm:

Một mệnh đề phức tạp có thể được tách thành nhiều mệnh đề đơn giản hơn bằng cách chọn một biến V và phân tích trường hợp V = True hoặc V = False.

Thuật toán liên tục tách biểu thức cho đến khi thu được các công thức đơn giản, nơi:

• Một dòng được xem là đúng nếu xuất hiện:

  • cùng một mệnh đề ở cả hai phía (A ở trái và A ở phải), hoặc

  • một mệnh đề và phủ định của nó (A và ¬A).

→ Khi đó dòng được chứng minh và nhánh được đánh dấu đúng.

Nếu tất cả các nhánh đều đúng → mệnh đề ban đầu là hằng đúng (tautology).

4. Mục tiêu của thuật toán

Thuật toán nhằm:

• Tự động hóa chứng minh trong logic mệnh đề (và sau này mở rộng sang logic vị từ).

• Cho phép máy tính kiểm tra mệnh đề đúng hay sai.

• Đơn giản hóa quá trình chứng minh bằng cách tách cấu trúc biểu thức.

Thuật toán là một dạng hệ thống chứng minh dạng bảng — giống như bảng chân trị, nhưng ít tốn tài nguyên hơn và hiệu quả hơn.

5. Các bước cơ bản của thuật toán Vương Hạo

Một cách tóm lược đơn giản:

B1 – Chuẩn hóa biểu thức

Đưa biểu thức về dạng:
A → B, hoặc A ∧ B → C ∨ D, nơi mỗi vế là một tập mệnh đề.

B2 – Tách theo một biến V

Chọn biến V xuất hiện trong biểu thức.

Tách thành hai nhánh:

1. V = True

2. V = False

Ở mỗi nhánh, ta loại bỏ hoặc thay thế các mệnh đề chứa V hoặc ¬V.

B3 – Kiểm tra một dòng có được chứng minh chưa

Một dòng được xem là đúng nếu:

• Có cùng một mệnh đề xuất hiện ở cả hai vế:
  Ví dụ: p ở trái và p ở phải.

• Hoặc có một mệnh đề và phủ định của nó xuất hiện:
  p ở trái và ¬p ở phải (hay ngược lại).

→ Vì khi đó công thức dạng
p → p hoặc p → ¬p
đều là mệnh đề hằng đúng.

B4 – Lặp lại đến khi tất cả dòng được chứng minh

Nếu tất cả các nhánh đều dẫn đến dòng đúng → Mệnh đề ban đầu là tautology.
Ngược lại → Không đúng.

6. Ví dụ ngắn

Chứng minh mệnh đề:

Tách theo p:

• Nhánh p = True

• Nhánh p = False

Cuối cùng, ta nhận được các dòng chứa q và r, và các nhánh đều rơi vào trường hợp:

• q ở cả hai vế

• hoặc r ở cả hai vế

→ Mệnh đề được chứng minh.

7. Ý nghĩa của thuật toán Vương Hạo

Thuật toán đóng vai trò quan trọng trong:

• Phát triển AI đầu tiên về chứng minh tự động

• Tiền đề của các kỹ thuật hiện đại:

  • SAT solving

  • Sequent calculus

  • Hệ thống suy diễn tự động

Nó cũng giúp sinh viên hiểu rõ:

• cách phân tích mệnh đề

• cách chia nhỏ biểu thức logic

• bản chất của tautology