Logic vị từ và hệ luật
Logic mệnh đề cho ta một ngôn ngữ chính xác để khẳng định câu nào đúng câu nào sai và để suy ra hệ quả bằng những luật máy móc. Nhưng nó dừng lại ở mức mỗi câu là một khối nguyên không chia nhỏ được. Bài này bổ sung phần còn thiếu đó: logic vị từ cho phép nói về đối tượng, thuộc tính và quan hệ, rồi dùng nó làm nền cho hệ luật dẫn, lõi của các hệ chuyên gia và nhiều công cụ suy diễn tự động.
Thử ngay: lượng từ trên một miền nhỏ
Hai khái niệm cần biết để bấm được công cụ dưới đây. Vị từ là một thuộc tính có thể đúng với đối tượng này và sai với đối tượng kia, ví dụ "x biết bay". Lượng từ nói vị từ ấy đúng với mọi đối tượng trong miền đang xét, hay chỉ cần đúng với ít nhất một đối tượng. Công cụ cho bạn chọn một vị từ và một lượng từ trên một miền nhỏ năm con vật rồi tự đánh giá mệnh đề đúng hay sai, đồng thời tô sáng những đối tượng thoả vị từ. Hãy để ý một phản ví dụ đủ làm câu với mọi thành sai, còn một nhân chứng đủ làm câu tồn tại thành đúng, và quan sát phủ định đảo lượng từ nhưng vẫn cho giá trị trái dấu với câu gốc.
∀ x, biet_bay(x)làsai¬ ( ∀ x, biet_bay(x) )tương đương∃ x, ¬biet_bay(x)làđúngHạn chế của logic mệnh đề
Trong logic mệnh đề, đơn vị nhỏ nhất là một mệnh đề nguyên tố nhận giá trị đúng hoặc sai, ví dụ P là "trời mưa", Q là "đường ướt". Ta ghép chúng bằng các phép nối quen thuộc: phủ định, hội (và), tuyển (hoặc), kéo theo (nếu thì). Cách này đủ cho nhiều bài toán, nhưng nó mù trước cấu trúc bên trong câu.
Xét câu "mọi người đều phải chết". Nếu ta mã hóa nó thành một ký hiệu mệnh đề duy nhất, chẳng hạn M, thì M chỉ là một biến đúng hoặc sai, không còn dấu vết của từ "mọi", của khái niệm "người", hay của thuộc tính "phải chết". Hậu quả là từ M và từ một câu khác "Socrates là người" (lại mã thành ký hiệu S), ta không có cách nào suy ra "Socrates phải chết". Hai ký hiệu M và S rời rạc, không chia sẻ thông tin gì với nhau.
Vấn đề gốc là logic mệnh đề không biểu diễn được ba thứ: đối tượng cụ thể (Socrates), thuộc tính của đối tượng (là người, phải chết), và phát biểu phổ quát hay tồn tại (mọi, có một). Logic vị từ ra đời để vá đúng ba lỗ hổng này.
Logic vị từ
Logic vị từ, còn gọi là logic bậc nhất, mở rộng logic mệnh đề bằng cách cho ta nói về đối tượng và quan hệ giữa chúng. Ngôn ngữ của nó gồm năm loại ký hiệu.
Hằng, biến, vị từ, hàm
- Hằng đặt tên cho một đối tượng cụ thể trong thế giới. Ví dụ
Socrates,DaNang,2. Mỗi hằng trỏ tới đúng một đối tượng. - Biến đứng thay cho một đối tượng chưa xác định, thường viết
x,y,z. Biến chỉ có nghĩa đầy đủ khi đi cùng một lượng từ. - Vị từ biểu diễn một thuộc tính hoặc một quan hệ. Nó nhận một hay nhiều đối tượng làm tham số rồi trả về đúng hoặc sai. Ví dụ
Nguoi(x)đúng khixlà người;Yeu(x, y)đúng khixyêuy. Số tham số gọi là ngôi của vị từ:Nguoilà vị từ một ngôi,Yeulà vị từ hai ngôi. - Hàm ánh xạ đối tượng sang đối tượng. Ví dụ
Cha(x)trả về cha củax,cong(x, y)trả về tổng. Điểm khác cốt lõi giữa hàm và vị từ: hàm trả về một đối tượng, còn vị từ trả về một giá trị chân lý. Vì vậyCha(Socrates)là một đối tượng (có thể đem làm tham số tiếp), cònNguoi(Socrates)là một câu đúng hoặc sai. - Lượng từ gắn ý nghĩa cho biến, gồm lượng từ "với mọi" và lượng từ "tồn tại", trình bày ngay dưới đây.
Ranh giới hàm và vị từ hay gây nhầm. Một mẹo: nếu cái bạn viết có thể đem so sánh đúng hay sai thì nó là vị từ; nếu nó là một thứ có thể đặt tên hay đem tính tiếp thì nó là hàm. cong(2, 3) là đối tượng 5; LonHon(5, 3) là câu đúng.
Lượng từ với mọi và tồn tại
Hai lượng từ cho phép phát biểu về cả một tập đối tượng thay vì từng đối tượng riêng lẻ. Ta viết chúng bằng chữ, hoặc bằng inline code forall cho "với mọi" và exists cho "tồn tại".
Lượng từ "với mọi" áp lên một biến khẳng định mệnh đề đúng với mọi đối tượng thay vào biến đó. Ví dụ:
forall x ( Nguoi(x) -> PhaiChet(x) )
đọc là "với mọi x, nếu x là người thì x phải chết".
Lượng từ "tồn tại" khẳng định có ít nhất một đối tượng làm mệnh đề đúng. Ví dụ:
exists x ( Sinhvien(x) and Gioi(x) )
đọc là "tồn tại x vừa là sinh viên vừa giỏi".
Hãy để ý cặp phép nối đi kèm mỗi lượng từ, vì đây là lỗi kinh điển của người mới. Với "với mọi" ta thường dùng kéo theo ->, còn với "tồn tại" ta thường dùng hội and. Nếu viết nhầm forall x ( Nguoi(x) and PhaiChet(x) ) thì câu trở thành "mọi đối tượng đều là người và đều phải chết", khẳng định cả hòn đá cũng là người, một điều sai. Ngược lại nếu viết exists x ( Sinhvien(x) -> Gioi(x) ) thì câu yếu đến vô nghĩa, vì chỉ cần tồn tại một đối tượng không phải sinh viên là kéo theo đã đúng rỗng.
Hai lượng từ phủ định lẫn nhau theo quy tắc De Morgan mở rộng:
not (forall x alpha) tương đương exists x (not alpha)
not (exists x alpha) tương đương forall x (not alpha)
Bằng lời: "không phải mọi sinh viên đều giỏi" tương đương "tồn tại một sinh viên không giỏi". Quy tắc này rất hữu ích khi ta cần đẩy phủ định vào sâu trong công thức.
Cụ thể hóa phổ quát
Sức mạnh của logic vị từ nằm ở chỗ một câu phổ quát duy nhất bao trùm vô số trường hợp riêng. Để dùng được câu phổ quát đó trong suy diễn, ta cần một bước biến nó thành một câu cụ thể: thay biến bằng một hằng. Bước này gọi là cụ thể hóa phổ quát.
Cụ thể, từ một câu dạng forall x alpha, ta được phép suy ra alpha với mọi biến x trong đó thay bằng một hằng tùy chọn. Ví dụ từ:
forall x ( Nguoi(x) -> PhaiChet(x) )
thế x = Socrates ta được câu cụ thể:
Nguoi(Socrates) -> PhaiChet(Socrates)
Câu này giờ chỉ còn các thành phần cố định, không còn biến, nên ta có thể áp các luật suy diễn của logic mệnh đề lên nó như bình thường.
Ví dụ Socrates
Ghép cụ thể hóa với modus ponens (từ A và A -> B suy ra B), ta tái hiện được suy luận cổ điển mà logic mệnh đề bó tay. Tri thức gồm một luật phổ quát và một sự kiện:
1. forall x ( Nguoi(x) -> PhaiChet(x) ) (luật)
2. Nguoi(Socrates) (sự kiện)
Các bước suy diễn:
3. Nguoi(Socrates) -> PhaiChet(Socrates) cụ thể hóa (1) với x = Socrates
4. PhaiChet(Socrates) modus ponens từ (2) và (3)
Ta kết luận PhaiChet(Socrates). Đây chính là điều logic mệnh đề không làm được, vì ở đó "mọi người phải chết" và "Socrates là người" là hai ký hiệu rời rạc không chia sẻ cấu trúc. Nhờ vị từ và lượng từ, hai câu giờ nối được với nhau qua hằng Socrates.
Ứng dụng: hệ luật dẫn
Một trong những ứng dụng trực tiếp nhất của logic là hệ luật dẫn, lõi của các hệ chuyên gia cổ điển. Ý tưởng là tách tri thức ra khỏi chương trình: ta lưu tri thức trong một cơ sở tri thức gồm sự kiện và luật, rồi để một bộ suy diễn chung chạy trên đó.
Biểu diễn tri thức bằng sự kiện và luật
Cơ sở tri thức gồm hai loại phần tử. Sự kiện là những điều đã biết là đúng, ví dụ Sot, HoKhan. Luật có dạng "nếu điều kiện thì kết luận", tức một câu kéo theo. Một cơ sở chẩn đoán đơn giản:
Sự kiện: Sot, HoKhan
Luật R1: Sot and HoKhan -> NghiCum
Luật R2: NghiCum -> KhuyenNghiXetNghiem
Việc tách tri thức khỏi thủ tục suy diễn mang lại ba lợi ích. Thứ nhất, thêm hay sửa một luật không buộc ta viết lại chương trình, chỉ cần sửa cơ sở tri thức. Thứ hai, vì mỗi luật là một câu logic và bộ suy diễn đúng đắn, kết luận luôn theo logic từ tri thức nên dễ kiểm chứng. Thứ ba, hệ thống giải thích được kết luận bằng cách truy ngược chuỗi luật đã dùng, một yêu cầu quan trọng của trí tuệ nhân tạo đáng tin cậy.
Suy diễn tiến
Suy diễn tiến xuất phát từ các sự kiện đã biết và lặp đi lặp lại việc áp luật. Mỗi vòng, nó tìm những luật có toàn bộ điều kiện đã nằm trong tập sự kiện rồi "cháy" luật đó, tức thêm kết luận của luật vào tập sự kiện. Quá trình dừng khi không sinh thêm được sự kiện mới, hoặc khi đã đạt mục tiêu cần tìm.
Chạy trên cơ sở trên, bắt đầu với Sot và HoKhan:
vòng 1: R1 có đủ điều kiện (Sot, HoKhan) -> thêm NghiCum
vòng 2: R2 có đủ điều kiện (NghiCum) -> thêm KhuyenNghiXetNghiem
vòng 3: không luật nào cháy thêm -> dừng
Tập sự kiện cuối cùng là {Sot, HoKhan, NghiCum, KhuyenNghiXetNghiem}. Suy diễn tiến hướng dữ liệu: nó rút mọi hệ quả có thể từ dữ liệu vào, phù hợp khi ta muốn biết tất cả những gì suy ra được.
Suy diễn lùi
Suy diễn lùi đi theo chiều ngược lại. Nó xuất phát từ một mục tiêu cần chứng, tìm luật nào có kết luận khớp mục tiêu, rồi đặt các điều kiện của luật đó thành những mục tiêu con và đệ quy chứng chúng. Khi một mục tiêu con trùng một sự kiện đã biết thì nó được chứng ngay.
Muốn chứng KhuyenNghiXetNghiem:
mục tiêu: KhuyenNghiXetNghiem
R2 kết luận ra nó -> mục tiêu con: NghiCum
R1 kết luận ra nó -> mục tiêu con: Sot, HoKhan
Sot là sự kiện -> đã chứng
HoKhan là sự kiện -> đã chứng
NghiCum được chứng
KhuyenNghiXetNghiem được chứng
Suy diễn lùi hướng mục tiêu: nó chỉ theo đuổi đúng những gì cần cho câu hỏi, phù hợp khi ta chỉ muốn trả lời một truy vấn cụ thể chứ không cần rút hết mọi hệ quả.
Cùng một cơ sở tri thức, suy diễn tiến và suy diễn lùi cho cùng kết luận nhưng khác cách làm việc. Tiến sinh mọi hệ quả nên tốn công khi cơ sở lớn mà ta chỉ cần một câu trả lời. Lùi chỉ bám mục tiêu nên tiết kiệm hơn cho truy vấn cụ thể, nhưng có thể lặp vô hạn nếu luật đệ quy mà không có cơ chế chặn.
Mã nguồn Python
Đoạn mã sau cài đặt một bộ suy diễn tiến nhỏ, chỉ dùng thư viện chuẩn. Mỗi sự kiện là một chuỗi. Mỗi luật là một cặp gồm tập điều kiện và một kết luận. Bộ suy diễn lặp cho tới khi không sinh thêm sự kiện mới, đúng như mô tả ở trên.
def forward_chaining(facts, rules):
# facts: a set of known fact strings
# rules: a list of (conditions, conclusion) pairs,
# where conditions is a set of fact strings
inferred = set(facts) # start from the known facts
changed = True
while changed: # keep looping until nothing new appears
changed = False
for conditions, conclusion in rules:
# a rule fires when all its conditions are already known
if conditions <= inferred and conclusion not in inferred:
inferred.add(conclusion)
changed = True
print(f"fired: {sorted(conditions)} -> {conclusion}")
return inferred
# simple diagnostic knowledge base
facts = {"Sot", "HoKhan"}
rules = [
({"Sot", "HoKhan"}, "NghiCum"), # R1
({"NghiCum"}, "KhuyenNghiXetNghiem"), # R2
]
result = forward_chaining(facts, rules)
print(sorted(result))
# expected: ['HoKhan', 'KhuyenNghiXetNghiem', 'NghiCum', 'Sot']
Phép kiểm tra conditions <= inferred dùng quan hệ tập con: luật chỉ cháy khi mọi điều kiện của nó đã nằm trong tập sự kiện đã biết. Vòng while lặp lại toàn bộ tập luật mỗi khi có sự kiện mới, vì một sự kiện vừa sinh ra có thể kích hoạt một luật ở lượt sau (như R2 chỉ cháy được sau khi R1 sinh ra NghiCum). Khi một vòng trọn vẹn không thêm gì, biến changed ở lại False và vòng lặp kết thúc.
Bài tập thực hành
Bài 1. Dịch các câu sau sang logic vị từ, nêu rõ hằng, vị từ, hàm và lượng từ dùng: (a) "Mọi sinh viên đều có một giảng viên hướng dẫn"; (b) "Không có số tự nhiên nào nhỏ hơn không"; (c) "Có ít nhất một thành phố lớn hơn Đà Nẵng".
Gợi ý
(a) cần lồng hai lượng từ: forall x ( Sinhvien(x) -> exists y ( Giangvien(y) and HuongDan(y, x) ) ). (b) phủ định một tồn tại, đưa về với mọi: forall x ( SoTuNhien(x) -> not NhoHon(x, 0) ), với 0 là hằng. (c) một tồn tại đơn giản: exists x ( ThanhPho(x) and LonHon(x, DaNang) ), với DaNang là hằng. Lưu ý cặp phép nối: với mọi đi với ->, tồn tại đi với and.
Bài 2. Cho cơ sở luật A and B -> C, C -> D, A -> B, cùng sự kiện A. Trình bày từng bước suy diễn tiến để rút ra D, rồi trình bày suy diễn lùi để chứng D. So sánh số luật cháy của hai chiến lược.
Gợi ý
Suy diễn tiến: từ A, luật A -> B cháy sinh B; giờ có cả A và B nên A and B -> C cháy sinh C; rồi C -> D cháy sinh D. Ba luật cháy. Suy diễn lùi cho D: C -> D cho mục tiêu con C; A and B -> C cho hai mục tiêu con A (là sự kiện) và B; A -> B cho mục tiêu con A (là sự kiện). Cùng dùng ba luật ở ví dụ nhỏ này, nhưng lùi chỉ mở đúng những nhánh cần cho D, còn tiến sẽ sinh cả những sự kiện không liên quan nếu cơ sở có thêm luật thừa.
Bài 3. Mở rộng đoạn mã Python thành suy diễn lùi: viết hàm backward_chaining(goal, facts, rules) trả về True nếu chứng được goal, bằng cách đệ quy trên các điều kiện của luật có kết luận khớp goal.
Gợi ý
Trường hợp cơ sở: nếu goal đã nằm trong facts thì trả về True ngay. Trường hợp đệ quy: duyệt các luật có conclusion == goal; với mỗi luật, gọi đệ quy backward_chaining trên từng điều kiện; nếu tất cả điều kiện của một luật nào đó đều chứng được thì trả về True. Nếu không luật nào thành công thì trả về False. Để tránh lặp vô hạn khi luật đệ quy, truyền thêm một tập các mục tiêu đang chứng dở và bỏ qua mục tiêu đã có trong tập đó.
Tự kiểm tra
Vì sao logic mệnh đề không suy được "Socrates phải chết" từ "mọi người phải chết" và "Socrates là người"?
Vì logic mệnh đề mã mỗi câu thành một ký hiệu nguyên không chia nhỏ được. "Mọi người phải chết" thành một ký hiệu, "Socrates là người" thành một ký hiệu khác, hai ký hiệu này rời rạc và không chia sẻ thông tin về đối tượng Socrates hay thuộc tính phải chết. Logic vị từ vá lỗ hổng bằng vị từ và lượng từ: câu phổ quát forall x ( Nguoi(x) -> PhaiChet(x) ) cụ thể hóa với x = Socrates rồi áp modus ponens với Nguoi(Socrates) để suy ra PhaiChet(Socrates).
Khác biệt cốt lõi giữa một hàm và một vị từ trong logic vị từ là gì?
Hàm trả về một đối tượng, còn vị từ trả về một giá trị chân lý. Cha(Socrates) là một đối tượng (cha của Socrates), có thể đem làm tham số cho vị từ hay hàm khác. Nguoi(Socrates) là một câu đúng hoặc sai, có thể đem nối với các câu khác bằng phép nối logic. Vì vậy hàm dùng để chỉ tới đối tượng, vị từ dùng để khẳng định điều gì đó về đối tượng.
Khi nào nên dùng suy diễn tiến và khi nào nên dùng suy diễn lùi?
Dùng suy diễn tiến khi muốn rút mọi hệ quả có thể từ một tập dữ liệu vào, vì nó hướng dữ liệu và sinh tất cả sự kiện suy ra được. Dùng suy diễn lùi khi chỉ cần trả lời một truy vấn cụ thể, vì nó hướng mục tiêu và chỉ theo đuổi những nhánh cần cho mục tiêu đó, tiết kiệm hơn khi cơ sở tri thức lớn mà câu hỏi hẹp.
Câu hỏi tự kiểm
- 1Lượng từ "với mọi" thường đi kèm phép nối nào để câu có nghĩa đúng?
- 2Khác biệt cốt lõi giữa một hàm và một vị từ trong logic vị từ là gì?
- 3Phủ định của một câu "với mọi x, alpha" tương đương với câu nào?
- 4Suy diễn lùi khác suy diễn tiến ở điểm cốt lõi nào?
Logic mệnh đề mù trước cấu trúc bên trong câu, nên không nói được về đối tượng, thuộc tính và phát biểu phổ quát. Logic vị từ vá điều đó bằng hằng, biến, vị từ, hàm và hai lượng từ "với mọi" và "tồn tại". Cụ thể hóa phổ quát biến một câu phổ quát thành câu cụ thể để áp modus ponens, tái hiện suy luận Socrates. Trên nền đó, hệ luật dẫn tách tri thức khỏi thủ tục suy diễn và chạy theo hai chiến lược: suy diễn tiến hướng dữ liệu, suy diễn lùi hướng mục tiêu, cùng kết luận nhưng khác cách làm việc.