Resolution và CNF - Chứng minh bằng mâu thuẫn

Resolution là một kỹ thuật suy luận quan trọng trong symbolic AI. Ý tưởng cốt lõi là:

1. đưa các sentence về dạng chuẩn;
2. tìm các literal bù nhau;
3. sinh clause mới;
4. nếu giả sử phủ định của query dẫn tới mâu thuẫn, query được chứng minh.

Mục tiêu

Sau bài này, bạn cần:

• phân biệt literal, clause và CNF;
• áp dụng resolution trên hai clause;
• chuyển các biểu thức đơn giản về CNF;
• hiểu proof by contradiction;
• nhận biết empty clause là dấu hiệu mâu thuẫn;
• so sánh cách làm của Resolution với Model Checking.

Resolution - suy luận bằng các literal bù nhau

Resolution là một inference rule mạnh và có thể dùng để xây hệ thống chứng minh tự động.

Bắt đầu bằng ví dụ:

và:

Nếu P không thể đúng, để P OR Q còn đúng thì Q phải đúng.

Do đó:

Complementary Literals

Hai literal như:

và:

được gọi là complementary literals - literal bù nhau.

Resolution tìm các cặp bù nhau để loại chúng và kết hợp phần còn lại.

Ví dụ tổng quát:

Resolution trên $P$ và $\neg P$ tạo:

Literal, Clause và CNF

Literal

Literal là:

• một propositional symbol như $P$;
• hoặc phủ định của symbol như $\neg P$.

Clause

Clause là một OR của các literal.

Ví dụ:

Conjunctive Normal Form - CNF

CNF là một AND của các clause.

Ví dụ:

Có thể nhớ cấu trúc:

CNF = AND của nhiều nhóm
mỗi nhóm = OR của các literal

Chuyển biểu thức về CNF

Một quy trình phổ biến:

1. loại biconditional;
2. loại implication;
3. đẩy NOT vào trong bằng De Morgan và double negation;
4. dùng distributive law để đạt dạng AND của các OR.

Ví dụ: chuyển $(P \lor Q) \to R$ sang CNF

Bắt đầu:

Loại implication:

Dùng De Morgan:

Phân phối OR qua AND:

Đây là CNF vì:

• toàn biểu thức là AND;
• mỗi thành phần là một clause OR của literal.

Resolution bằng proof by contradiction

Muốn chứng minh:

thay vì cố trực tiếp sinh $\alpha$, ta có thể giả sử điều ngược lại:

Nếu giả sử đó dẫn tới contradiction, thì $\neg\alpha$ không thể cùng đúng với KB.

Do đó:

Ý tưởng:

Empty Clause - dấu hiệu mâu thuẫn

Nếu Resolution cuối cùng cho ra empty clause:

thì ta đã sinh ra False.

Một cách hình dung:

Ta có P.
Ta cũng có ¬P.
Không có thế giới nhất quán nào làm cả hai cùng đúng.

Đó là contradiction.

Ví dụ Resolution từng bước

Knowledge Base:

Query:

Ta muốn kiểm tra:

Bước 1 - giả sử query sai

Thêm:

Ta có các clause:

1. A OR B
2. NOT B OR C
3. NOT C
4. NOT A

Bước 2 - resolve clause 2 và 3

Từ:

và:

suy ra:

Bước 3 - resolve clause 1 với $\neg B$

Từ:

và:

suy ra:

Bước 4 - resolve $A$ và $\neg A$

Ta có:

và:

=> empty clause.

Giả sử NOT A gây mâu thuẫn với KB, nên:

Model Checking và Resolution khác nhau thế nào?

Không nên hiểu Resolution là “luôn nhanh”. Trong logic tổng quát, suy luận vẫn có thể rất tốn tính toán. Điểm chính là Resolution cho một cơ chế proof có cấu trúc thay vì liệt kê toàn bộ model một cách ngây thơ.

Chốt lại

Để chứng minh:

Resolution thường biến bài toán thành:

Nếu các clause cuối cùng dẫn tới empty clause, giả sử $\neg\alpha$ không thể đồng thời đúng với KB, nên $\alpha$ được entail.

Điểm quan trọng không phải là học thuộc thao tác máy móc, mà là hiểu ba lớp:

Sentence logic
    -> CNF clauses
    -> Resolution
    -> Contradiction hoặc không sinh thêm tri thức mới

Bản tiếng Anh đang soạn.