Logic mệnh đề và suy diễn
Các chương trước giải bài toán bằng tìm kiếm: máy duyệt không gian trạng thái để tới đích. Chương này chuyển sang một năng lực khác của trí tuệ nhân tạo, đó là lập luận (reasoning). Thay vì thử mọi khả năng, máy biểu diễn tri thức thành các câu logic, rồi suy ra tri thức mới đúng theo luật suy diễn. Logic cho ta một ngôn ngữ chính xác để mô tả thế giới, một ngữ nghĩa để nói câu nào đúng, và những thủ tục máy móc để chứng minh hệ quả mà không cần con người can thiệp. Đây là nền của các hệ chuyên gia, hệ luật dẫn và nhiều công cụ kiểm chứng phần mềm ngày nay.
Thử ngay: bảng chân trị của các phép nối
Logic mệnh đề định nghĩa mỗi phép nối (not, AND, OR, kéo theo, tương đương) bằng một bảng chân trị, liệt kê công thức nhận giá trị đúng hay sai ứng với từng cách gán P và Q. Bảng ấy đọc suông thì dễ quên, nhất là chỗ kéo theo. Hãy tự tay bật tắt giá trị của P và Q ở công cụ dưới đây rồi quan sát từng phép nối đổi giá trị ra sao. Chú ý cột kéo theo chỉ có đúng một ô sai, khi P đúng mà Q sai.
| P | Q | not P | P AND Q | P OR Q | P kéo theo Q | P tương đương Q |
|---|---|---|---|---|---|---|
| sai | sai | đúng | sai | sai | đúng | đúng |
| sai | đúng | đúng | sai | đúng | đúng | sai |
| đúng | sai | sai | sai | đúng | sai | sai |
| đúng | đúng | sai | đúng | đúng | đúng | đúng |
Logic mệnh đề
Logic mệnh đề (propositional logic) là dạng logic đơn giản nhất. Đơn vị nhỏ nhất là mệnh đề (proposition), một câu khẳng định chỉ nhận một trong hai giá trị chân lý: đúng hay sai. Ta dùng các ký hiệu như P, Q, R để đặt tên cho mệnh đề nguyên tố, ví dụ P là "trời mưa", Q là "đường ướt". Từ các mệnh đề nguyên tố, ta ghép thành công thức phức tạp bằng các phép nối logic.
Cú pháp
Cú pháp (syntax) quy định công thức nào viết đúng quy tắc. Một công thức hợp lệ được dựng đệ quy như sau:
- Hai hằng
true(đúng) vàfalse(sai) là công thức; mỗi ký hiệu mệnh đềP,Q,R, ... là công thức. - Nếu
alà công thức thìnot a(phủ định) là công thức. - Nếu
avàblà công thức thìa AND b(hội),a OR b(tuyển),a -> b(kéo theo),a <-> b(tương đương) đều là công thức.
Để bớt dấu ngoặc, ta quy ước thứ tự ưu tiên các phép nối giảm dần: not, rồi AND, rồi OR, rồi ->, cuối cùng <->. Ví dụ not P OR Q -> R được hiểu là ((not P) OR Q) -> R.
Ngữ nghĩa và bảng chân trị
Cú pháp chỉ nói công thức viết có đúng quy tắc không. Ngữ nghĩa (semantics) mới cho biết công thức đúng hay sai. Một phép gán chân trị (truth assignment), hay một thế giới (model), gán cho mỗi ký hiệu mệnh đề một giá trị đúng hoặc sai. Khi đã có phép gán, giá trị của công thức phức được tính theo bảng ngữ nghĩa của từng phép nối. Quy ước 1 là đúng, 0 là sai:
P | Q | not P | P AND Q | P OR Q | P -> Q | P <-> Q | P XOR Q |
|---|---|---|---|---|---|---|---|
| 0 | 0 | 1 | 0 | 0 | 1 | 1 | 0 |
| 0 | 1 | 1 | 0 | 1 | 1 | 0 | 1 |
| 1 | 0 | 0 | 0 | 1 | 0 | 0 | 1 |
| 1 | 1 | 0 | 1 | 1 | 1 | 1 | 0 |
Hai chỗ dễ nhầm cần lưu ý. Thứ nhất, phép kéo theo P -> Q chỉ sai duy nhất khi P đúng mà Q sai; khi P sai thì P -> Q luôn đúng bất kể Q, gọi là chân lý rỗng. Thứ hai, tuyển OR trong logic là tuyển không loại trừ: P OR Q đúng cả khi cả hai cùng đúng. Phép tuyển loại trừ ghi là XOR, đúng khi đúng đúng một trong hai.
Câu tiếng Việt "nếu trời mưa thì đường ướt" không nói gì khi trời không mưa. Trong logic, P -> Q vẫn nhận giá trị đúng trong trường hợp đó. Đừng đọc P -> Q thành quan hệ nhân quả; nó chỉ là một hàm chân trị.
Bảng chân trị (truth table) liệt kê giá trị của một công thức trên mọi phép gán. Với n ký hiệu mệnh đề có 2^n dòng. Bảng chân trị là cách kiểm tra vét cạn, luôn cho câu trả lời nhưng tốn theo cấp số nhân.
Xét công thức phi = (P -> Q) AND (not P OR R). Có ba ký hiệu nên 2^3 = 8 dòng:
P Q R | P->Q | not P OR R | phi
0 0 0 | 1 | 1 | 1
0 0 1 | 1 | 1 | 1
0 1 0 | 1 | 1 | 1
0 1 1 | 1 | 1 | 1
1 0 0 | 0 | 0 | 0
1 0 1 | 0 | 1 | 0
1 1 0 | 1 | 0 | 0
1 1 1 | 1 | 1 | 1
Công thức đúng ở 4 trên 8 phép gán nên nó thỏa được (satisfiable) nhưng không phải hằng đúng.
Hằng đúng, mâu thuẫn và hệ quả logic
Một công thức gọi là hằng đúng (tautology) nếu đúng trên mọi phép gán, ví dụ P OR not P. Nó là mâu thuẫn (contradiction) nếu sai trên mọi phép gán, ví dụ P AND not P. Nếu có ít nhất một phép gán làm nó đúng thì nó thỏa được.
Khái niệm trung tâm của lập luận là hệ quả logic. Tập câu G kéo theo về mặt logic (entails) câu a, viết G |= a, nếu mọi phép gán làm tất cả câu trong G đúng thì cũng làm a đúng. Nói cách khác, a đúng trong mọi thế giới mà tri thức G thừa nhận.
G |= a khi và chỉ khi công thức (tích các câu trong G) AND not a là mâu thuẫn. Đây là quy về chứng minh bằng phản chứng: muốn chứng a là hệ quả, ta giả sử not a rồi chỉ ra điều đó dẫn tới vô lý. Phép phân giải ở mục sau khai thác đúng ý này.
Tương đương logic
Hai công thức a và b tương đương logic (logically equivalent), viết a == b, nếu chúng có cùng giá trị trên mọi phép gán. Tương đương cho phép biến đổi công thức về dạng tiện hơn mà không đổi ngữ nghĩa. Bảng dưới liệt kê các tương đương dùng thường xuyên:
| Tên | Tương đương |
|---|---|
| Khử kéo theo | P -> Q == not P OR Q |
| Khử tương đương | P <-> Q == (P -> Q) AND (Q -> P) |
| Phủ định kép | not (not P) == P |
| Giao hoán | P AND Q == Q AND P ; P OR Q == Q OR P |
| Kết hợp | (P AND Q) AND R == P AND (Q AND R) |
| Phân phối | P AND (Q OR R) == (P AND Q) OR (P AND R) |
| De Morgan | not (P AND Q) == not P OR not Q |
| De Morgan | not (P OR Q) == not P AND not Q |
| Phản đảo | P -> Q == not Q -> not P |
Dạng chuẩn hội CNF
Nhiều thủ tục suy diễn yêu cầu công thức ở một dạng chuẩn. Dạng chuẩn hội (conjunctive normal form), viết tắt CNF, là hội của các mệnh đề tuyển (clause), mỗi mệnh đề tuyển là tuyển của các văn tự (literal), mỗi văn tự là một ký hiệu hoặc phủ định của nó. Một ví dụ CNF là (not P OR Q) AND (not Q OR R) AND (P OR R).
Mọi công thức mệnh đề đều đưa được về CNF tương đương qua ba bước:
- Khử
<->và->bằng hai tương đương khử kéo theo và khử tương đương. - Đẩy
notvào sát ký hiệu bằng De Morgan và phủ định kép, để chỉ còn phủ định trên ký hiệu nguyên tố. - Phân phối
ORquaANDđể được hội của các tuyển.
Ví dụ đưa P -> (Q AND R) về CNF. Bước 1: not P OR (Q AND R). Bước 2 không phải làm vì phủ định đã sát ký hiệu. Bước 3 phân phối: (not P OR Q) AND (not P OR R). Kết quả là hai mệnh đề tuyển.
Suy diễn trong logic mệnh đề
Bảng chân trị kiểm tra hệ quả được nhưng tốn 2^n dòng. Suy diễn (inference) cho cách rút ra câu mới bằng các luật suy diễn thao tác trên cú pháp, thường nhanh hơn nhiều.
Modus ponens và các luật quen thuộc
Modus ponens là luật suy diễn cổ điển nhất: từ a và a -> b suy ra b. Ví dụ biết "trời mưa" và "nếu trời mưa thì đường ướt", ta suy "đường ướt". Vài luật hữu ích khác: modus tollens từ not b và a -> b suy not a; luật và-loại từ a AND b suy a; luật tam đoạn luận từ a -> b và b -> c suy a -> c.
Mỗi luật phải đúng đắn (sound), nghĩa là chỉ suy ra câu thật sự là hệ quả logic. Modus ponens đúng đắn vì kiểm bảng chân trị thấy mọi thế giới làm a và a -> b đúng thì b cũng đúng.
Khẳng định ngược lại modus ponens là ngụy biện. Từ b và a -> b không suy được a. Biết "đường ướt" và "mưa thì đường ướt" không cho phép kết luận trời mưa, vì đường có thể ướt do tưới cây.
Phép phân giải resolution
Khó khăn của modus ponens là nó chỉ áp được khi công thức có đúng dạng. Phép phân giải (resolution) mạnh hơn: chỉ cần một luật duy nhất, áp trên các mệnh đề tuyển ở dạng CNF, là đủ chứng minh mọi hệ quả logic. Luật phân giải lấy hai mệnh đề tuyển chứa một ký hiệu ở hai cực trái dấu rồi gộp phần còn lại. Nếu một mệnh đề chứa văn tự L và mệnh đề kia chứa not L, hai văn tự này triệt tiêu nhau, phần còn lại của hai mệnh đề gộp thành mệnh đề mới gọi là phân giải thức (resolvent).
Ví dụ cho hai mệnh đề (not P OR Q) và (P OR R). Cặp ký hiệu trái dấu là not P và P. Triệt tiêu chúng, phân giải thức là (Q OR R).
Nếu hai mệnh đề là L và not L thì phân giải thức là mệnh đề rỗng, ký hiệu bằng ô vuông trống, biểu thị mâu thuẫn.
Thủ tục chứng minh bằng phản chứng dùng phân giải như sau: muốn chứng G |= a, ta đưa G cùng với not a về CNF, rồi liên tục phân giải các cặp mệnh đề. Nếu sinh ra mệnh đề rỗng thì tập ban đầu mâu thuẫn, suy ra G |= a. Phép phân giải đầy đủ (complete) cho phản chứng: nếu thật sự có hệ quả thì luôn dẫn được tới mệnh đề rỗng.
Lấy ví dụ tri thức { P -> Q, Q -> R, P }, ta muốn chứng R. Sau khi đưa về CNF và thêm not R (phủ định kết luận), tập mệnh đề là { not P OR Q, not Q OR R, P, not R }. Các bước phân giải dẫn tới mệnh đề rỗng:
1. not P OR Q (tri thức)
2. not Q OR R (tri thức)
3. P (tri thức)
4. not R (phủ định kết luận)
5. Q = phân giải (1) với (3) trên P
6. not Q = phân giải (2) với (4) trên R
7. rỗng = phân giải (5) với (6) trên Q -> mâu thuẫn, vậy R là hệ quả
Sinh ra mệnh đề rỗng khẳng định R là hệ quả logic của tri thức.
Cài đặt bằng Python
Ta dựng bảng chân trị rồi kiểm tra hệ quả logic bằng định nghĩa vét cạn. Mỗi công thức biểu diễn bằng một hàm Python nhận một dict (phép gán) và trả về True hoặc False.
from itertools import product
def truth_table(symbols, formula):
# enumerate all 2**n assignments and record the value of the formula
rows = []
for values in product([False, True], repeat=len(symbols)):
model = dict(zip(symbols, values))
rows.append((model, formula(model)))
return rows
def entails(symbols, premises, conclusion):
# KB |= alpha iff every model satisfying all premises satisfies alpha
for values in product([False, True], repeat=len(symbols)):
model = dict(zip(symbols, values))
if all(p(model) for p in premises): # model satisfies the KB
if not conclusion(model): # but not the conclusion
return False # found a counter-model
return True
# Example: { P -> Q, Q -> R, P } |= R
symbols = ["P", "Q", "R"]
premises = [
lambda m: (not m["P"]) or m["Q"], # P -> Q
lambda m: (not m["Q"]) or m["R"], # Q -> R
lambda m: m["P"], # P
]
conclusion = lambda m: m["R"] # R
print(entails(symbols, premises, conclusion)) # True
Hàm entails chạy qua đúng 2^n phép gán, giống hệt định nghĩa hệ quả logic: nếu tìm được một thế giới làm toàn bộ tri thức đúng mà kết luận sai thì kết luận không phải hệ quả.
Tiếp theo là một bước phân giải. Ta biểu diễn một văn tự bằng chuỗi như "P" hay "~P" (dấu ngã là phủ định), một mệnh đề tuyển bằng frozenset các văn tự.
def negate(lit):
# toggle the negation of a literal encoded as a string
return lit[1:] if lit.startswith("~") else "~" + lit
def resolve(clause_a, clause_b):
# return every resolvent obtainable from one complementary pair
resolvents = set()
for lit in clause_a:
if negate(lit) in clause_b: # complementary literals
merged = (clause_a - {lit}) | (clause_b - {negate(lit)})
resolvents.add(frozenset(merged)) # cancel the pair, merge rest
return resolvents
# Resolve (~P v Q) with (P v R) -> (Q v R)
a = frozenset({"~P", "Q"})
b = frozenset({"P", "R"})
print(resolve(a, b)) # { frozenset({'Q', 'R'}) }
Lặp lại resolve trên mọi cặp mệnh đề, thêm phân giải thức mới vào tập, cho tới khi sinh ra frozenset() rỗng (mệnh đề rỗng) hoặc không sinh thêm gì, ta được thủ tục phân giải đầy đủ. Mệnh đề rỗng báo tri thức mâu thuẫn, tức kết luận ban đầu là hệ quả.
Bài tập thực hành
Bài 1. Dựng bảng chân trị đầy đủ cho công thức (P OR Q) -> (not P AND R) với ba ký hiệu P, Q, R. Cho biết công thức là hằng đúng, mâu thuẫn hay chỉ thỏa được.
Gợi ý
Lập 8 dòng cho 3 ký hiệu. Vế trái P OR Q đúng ở 6 dòng, vế phải not P AND R chỉ đúng khi P sai và R đúng. Công thức đúng ở một số dòng (ví dụ khi P, Q cùng sai thì vế trái sai nên kéo theo đúng) và sai ở một số dòng khác, vậy nó chỉ thỏa được, không hằng đúng cũng không mâu thuẫn.
Bài 2. Dùng các phép tương đương trong bảng tương đương, chứng minh P -> (Q -> R) == (P AND Q) -> R. Ghi rõ tương đương dùng ở mỗi bước.
Gợi ý
Khử kéo theo hai lần ở vế trái: P -> (Q -> R) thành not P OR (not Q OR R). Dùng kết hợp gộp thành (not P OR not Q) OR R. Dùng De Morgan ngược: not P OR not Q == not (P AND Q). Vậy vế trái thành not (P AND Q) OR R, đúng bằng (P AND Q) -> R sau khi khử kéo theo.
Bài 3. Đưa các công thức sau về dạng chuẩn hội CNF: not (P -> Q) ; P <-> Q ; not (P OR Q) -> R.
Gợi ý
Với not (P -> Q): khử kéo theo thành not (not P OR Q), De Morgan thành P AND not Q. Với P <-> Q: khử tương đương thành (not P OR Q) AND (not Q OR P). Với not (P OR Q) -> R: khử kéo theo thành not (not (P OR Q)) OR R, phủ định kép thành (P OR Q) OR R, tức một mệnh đề tuyển P OR Q OR R.
Bài 4. Cho tri thức { P OR Q, not Q OR R, not R }. Dùng phép phân giải để chứng minh tri thức này kéo theo P. Vẽ sơ đồ phân giải dẫn tới mệnh đề rỗng.
Gợi ý
Thêm phủ định kết luận not P. Phân giải not Q OR R với not R trên R được not Q. Phân giải P OR Q với not Q trên Q được P. Phân giải P với not P trên P được mệnh đề rỗng. Vậy P là hệ quả.
Bài 5. (Lập trình) Mở rộng hàm resolve thành thủ tục phân giải đầy đủ: nhận một danh sách mệnh đề CNF, lặp sinh phân giải thức cho tới khi gặp mệnh đề rỗng hoặc không sinh thêm. Kiểm thử trên tri thức { not P OR Q, not Q OR R, P, not R } và xác nhận thủ tục báo mâu thuẫn.
Gợi ý
Giữ một tập các mệnh đề. Trong mỗi vòng, duyệt mọi cặp mệnh đề, gọi resolve, gom mọi phân giải thức mới. Nếu có frozenset() rỗng thì báo mâu thuẫn (kết luận là hệ quả). Nếu không có phân giải thức nào mới so với tập hiện tại thì dừng và báo không suy được.
Tự kiểm tra
Vì sao P -> Q lại đúng khi P sai, dù trực giác thấy lạ?
Kéo theo trong logic chỉ là một hàm chân trị, không phải quan hệ nhân quả. Ta định nghĩa P -> Q sai duy nhất ở trường hợp P đúng mà Q sai, vì đó là trường hợp duy nhất một lời hứa dạng "nếu P thì Q" bị vi phạm. Khi P sai, lời hứa chưa bị thử thách nên không bị coi là sai; ta quy ước nó đúng, gọi là chân lý rỗng. Quy ước này làm cho P -> Q tương đương not P OR Q, rất tiện khi biến đổi công thức.
Vì sao phép phân giải lại chứng minh hệ quả qua việc phủ định kết luận?
Vì G |= a khi và chỉ khi (tích các câu trong G) AND not a là mâu thuẫn. Thay vì kiểm trực tiếp rằng a đúng trong mọi thế giới của G, ta giả sử ngược lại not a rồi tìm mâu thuẫn. Phép phân giải sinh dần các mệnh đề mới; nếu suy ra mệnh đề rỗng thì tập là mâu thuẫn, vậy giả sử not a sai, tức a là hệ quả. Phân giải đầy đủ cho phản chứng nên nếu hệ quả tồn tại thì luôn tìm được mệnh đề rỗng.
Câu hỏi tự kiểm
- 1Phép kéo theo P kéo theo Q nhận giá trị sai trong trường hợp duy nhất nào?
- 2Công thức P OR not P thuộc loại nào?
- 3Tương đương khử kéo theo phát biểu điều gì?
- 4Trong chứng minh bằng phép phân giải, sinh ra mệnh đề rỗng nghĩa là gì?
Logic mệnh đề cho ta một ngôn ngữ với cú pháp dựng đệ quy và ngữ nghĩa định nghĩa qua bảng chân trị. Hệ quả logic G |= a nghĩa là a đúng trong mọi thế giới làm G đúng, và kiểm được vét cạn bằng bảng chân trị tốn 2^n dòng. Tương đương logic cho phép biến đổi công thức về CNF. Suy diễn bằng modus ponens nhanh nhưng kén dạng; phép phân giải chỉ một luật mà đầy đủ, chứng minh hệ quả bằng cách phủ định kết luận rồi phân giải tới mệnh đề rỗng.