Các phương pháp biểu diễn diễn tri thức

Định nghĩa: Logic mênh đề là công cụ toán logic, trong đó các mênh đề được mã hoá (gán) cho một biến, hoặc hằng; còn vác biểu thức là sự liên kết co nghĩa giữa các biến hằng với một số toán tử nhất định.

Tri thức được mô tả dưới dạng các mệnh đề trong ngôn ngữ biểu diễn tri thức. Mỗi câu có thể xem như sự mã hóa một sự hiểu biết của ta về thế giới thực. Ngôn ngữ biểu diễn tri thức (cũng như mọi ngôn ngữ hình thức khác) gồm hai thành phần cơ bản là cú pháp và ngữ nghĩa.

• Cú pháp của một ngôn ngữ bao gồm các ký hiệu và các quy tắc liên kết các ký hiệu (các luật cú pháp) để tạo thành các câu (công thức) trong ngôn ngữ. Các câu ở đây là biểu diễn ngoài, cần phân biệt với biểu diễn bên trong máy tính. Các câu sẽ được chuyển thành các cấu trúc dữ liệu thích hợp được cài đặt trong một vùng nhớ nào đó của máy tính, đó là biểu diễn bên trong. Bản thân các câu chưa chứa đựng một nội dung nào cả, chưa mang một ý nghĩa nào cả.

• Ngữ nghĩa của ngôn ngữ cho phép ta xác định ý nghĩa của các câu trong một miền nào đó của thế giới hiện thực. Chẳng hạn, trong ngôn ngữ các biểu thức số học, dãy ký hiệu (x+y)*z là một câu viết đúng cú pháp. Ngữ nghĩa của ngôn ngữ này cho phép ta hiểu rằng, nếu x, y, z, ứng với các số nguyên, ký hiệu + ứng với phép toán cộng, còn * ứng với phép chia, thì biểu thức (x+y)*z biểu diễn quá trình tính toán: lấy số nguyên x cộng với số nguyên y, kết quả được nhân với số nguyên z.

• Ngoài hai thành phần cú pháp và ngữ nghĩa, ngôn ngữ biểu diễn tri thức cần được cung cấp cơ chế suy diễn. Một luật suy diễn (rule of inference) cho phép ta suy ra một công thức từ một tập nào đó các công thức. Chẳng hạn, trong logic mệnh đề, luật modus ponens cho phép từ hai công thức A và A⇒B suy ra công thức B. Chúng ta sẽ hiểu lập luận hoặc suy diễn là một quá trình áp dụng các luật suy diễn để từ các tri thức trong cơ sở tri thức và các sự kiện ta nhận được các tri thức mới. Như vậy chúng ta xác định:

Ngôn ngữ biểu diễn tri thức = Cú pháp + Ngữ nghĩa + Cơ chế suy diễn.

Một ngôn ngữ biểu diễn tri thức tốt cần có khả năng biểu diễn rộng, tức là mô tả được mọi điều mà chúng ta muốn. Nó cần hiệu quả để đi tới các kết luận; thủ tục suy diễn đòi hỏi ít thời gian tính toán và không gian nhớ. Người ta mong muốn ngôn ngữ biểu diễn tri thức gần với ngôn ngữ tự nhiên.

Trong mục này chúng ta sẽ xét việc chuẩn hóa các công thức, đưa các công thức về dạng thuận lợi cho việc lập luận, suy diễn. Trước hết ta sẽ xét các phép biến đổi tương đương. Sử dụng các phép biển đổi này, ta có thể đưa một công thức bất kỳ về dạng chuẩn tắc.

Ở trên ta đã chỉ ra, mọi công thức đều có thể đưa về dạng chuẩn hội, tức là hội của các tuyển, mỗi câu tuyển có dạng:

lP₁ ∨... ..∨ lP_m ∨ Q₁ ∨.....∨ Qn

trong đó P_i, Q_i là các ký hiệu mệnh đề (literal dương) câu này tương đương với câu:

P₁ ^... .^ lP_m => Q₁ ∨.....∨ Qn

Dạng câu này được gọi là câu Kowalski (do nhà logic Kowalski đưa ra năm 1971).

Khi n <=1, tức là câu tuyển chỉ chứa nhiều nhất một literal dương, ta có một dạng câu đặc biệt quan trọng được gọi là câu Horn (mang tên nhà logic Alfred Horn, năm 1951).

Nếu m>0, n=1, câu Horn có dạng:

P₁ ∧.....∧ Pm => Q

Trong đó Pi , Q là các literal dương. Các Pi được gọi là các điều kiện (hoặc giả thiết), còn Q được gọi là kết luận (hoặc hệ quả). Các câu Horn dạng này còn được gọi là các luật if-then và được biểu diễn như sau:

If P1 and....and Pm then Q.

Khi m=0, n=1 câu Horn trở thành câu đơn Q, hay sự kiện Q. Nếu m>0, n=0 câu Horn trở thành dạng lP₁ v......v lPm hay tương đương l(P1^...^ Pm).

Một công thức H được xem là hệ qủa logic (logical consequence) của một tập công thức G ={G1,.....,Gm} nếu trong bất kỳ minh họa nào mà {G1,... ..,Gm} đúng thì H cũng đúng. Nói cách khác bất kỳ mô hình nào của G cũng là mô hình của H.

Khi có một cơ sở tri thức, ta muốn sử dụng các tri thức trong cơ sở này để suy ra tri thức mới mà nó là hệ quả logic của các công thức trong cơ sở tri thức. Điều đó được thực hiện bằng cách sử dụng các luật suy diễn (rule of inference). Luật suy diễn giống như một thủ tục mà chúng ta sử dụng để sinh ra một công thức mới từ các công thức đã có. Một luật suy diễn gồm hai phần: một tập các điều kiện và một kết luận. Chúng ta sẽ biểu diễn các luật suy diễn dưới dạng “phân số ”, trong đó tử số là danh sách các điều kiện, còn mẫu số là kết luận của luật, tức là mẫu số là công thức mới được suy ra từ các công thức ở tử số.

Sau đây là một số luật suy diễn quan trọng trong logic mệnh đề. Trong các luật này α, α_i, β, γ là các công thức:

Luật Modus Ponens

Từ một kéo theo và giả thiết của kéo theo, ta suy ra kết luận của nó.

Luật Modus Tollens

Từ một kéo theo và phủ định kết luận của nó, ta suy ra phủ định giả thiết của kéo theo.

Luật bắc cầu

Từ hai kéo theo, mà kết luận của kéo theo thứ nhất trùng với giả thiết của kéo theo thứ hai, ta suy ra kéo theo mới mà giả thiết của nó là giả thiết của kéo theo thứ nhất, còn kết luận của nó là kết luận của kéo theo thứ hai.

Luật loại bỏ hội

Từ một hội ta suy ra một nhân tử bất kỳ của hội.

Luật đưa vào hội

Từ một danh sách các công thức, ta suy ra hội của chúng.

Luật đưa vào tuyển

Từ một công thức, ta suy ra một tuyển mà một trong các hạng tử của tuyển là công thức đó.

Luật phân giải

Từ hai tuyển, một tuyển chứa một hạng tử đối lập với một hạng tử trong tuyển kia, ta suy ra tuyển của các hạng tử còn lại trong cả hai tuyển.

Một luật suy diễn được xem là tin cậy (sound) nếu bất kỳ một mô hình nào của giả thiết của luật cũng là mô hình của kết luận của luật. Chúng ta chỉ quan tâm đến các luật suy diễn tin cậy.

Bằng phương pháp bảng chân lý, ta có thể kiểm chứng được các luật suy diễn nêu trên đều là tin cậy. Bảng chân lý của luật phân giải được cho trong hình 3.3. Từ bảng này ta thấy rằng, trong bất kỳ một minh họa nào mà cả hai giả thiết α ∨ β, ˥ β ∨ γ đúng thì kết luận α ∨ γ cũng đúng. Do đó luật phân giải là luật suy điễn tin cậy.

Ta có nhận xét rằng, luật phân giải là một luật suy diễn tổng quát, nó bao gồm luật Modus Ponens, luật Modus Tollens, luật bắc cầu như các trường hợp riêng. (Bạn đọc dễ dàng chứng minh được điều đó).

Tiên đề, định lý, chứng minh.

Giả sử chúng ta có một tập nào đó các công thức. Các luật suy diễn cho phép ta từ các công thức đã có suy ra công thức mới bằng một dãy áp dụng các luật suy diễn. Các công thức đã cho được gọi là các tiên đề. Các công thức được suy ra được gọi là các định lý. Dãy các luật được áp dụng để dẫn tới định lý được gọi là một chứng minh của định lý. Nếu các luật suy diễn là tin cậy, thì các định lý là hệ quả logic của các tiên đề.

Trong các hệ tri thức, chẳng hạn các hệ chuyên gia, hệ lập trình logic,..., sử dụng các luật suy diễn người ta thiết kế lên các thủ tục suy diễn (còn được gọi là thủ tục chứng minh) để từ các tri thức trong cơ sở tri thức ta suy ra các tri thức mới đáp ứng nhu cầu của người sử dụng.

Một hệ hình thức (formal system) bao gồm một tập các tiên đề và một tập các luật suy diễn nào đó (trong ngôn ngữ biểu diễn tri thức nào đó).

Một tập luật suy diễn được xem là đầy đủ, nếu mọi hệ quả logic của một tập các tiên đề đều chứng minh được bằng cách chỉ sử dụng các luật của tập đó.

Phương pháp chứng minh bác bỏ

Phương pháp chứng minh bác bỏ (refutation proof hoặc proof by contradiction) là một phương pháp thường xuyên được sử dụng trong các chứng minh toán học. Tư tưởng của phương pháp này là như sau: Để chứng minh P đúng, ta giả sử P sai (thêm ˥ P vào các giả thiết) và dẫn tới một mâu thuẫn. Sau đây ta sẽ trình bầy cơ sở của phương pháp chứng minh này.

Giả sử chúng ta có một tập các công thức G ={G1,.....,Gm} ta cần chứng minh công thức H là hệ quả logic của G. Điều đó tương đương với chứng minh công thức G1^....^Gm ⇒ H là vững chắc. Thay cho chứng minh G1^... ^Gm ⇒H là vững chắc, ta chứng minh G1^....^Gm ^˥ H là không thỏa mãn được. Tức là ta chứng minh tập G’= (G1,... .,Gm,˥ H) là không thỏa được. G sẽ không thoả được nếu từ G‘ta suy ra hai mệnh đề đối lập nhau. Việc chứng minh công thức H là hệ quả logic của tập các tiêu đề G bằng cách chứng minh tính không thỏa được của tập các tiêu đề được thêm vào phủ định của công thức cần chứng minh, được gọi là chứng minh bác bỏ.

Để thuận tiện cho việc sử dụng luật phân giải, chúng ta sẽ cụ thể hoá luật phân giải trên các dạng câu đặc biệt quan trọng.

Luật phân giải trên các câu tuyển

trong đó A_i, B_j và C là các literal. Luật phân giải trên các câu Horn:

Giả sử P_i, R_j, Q và S là các literal. Khi đó ta có các luật sau:

Một trường hợp riêng hay được sử dụng của luật trên là:

Khi ta có thể áp dụng luật phân giải cho hai câu, thì hai câu này được gọi là hai câu phân giải được và kết quả nhận được khi áp dụng luật phân giải cho hai câu đó được gọi là phân giải thức của chúng. Phân giải thức của hai câu A và B được kí hiệu là res(A,B). Chẳng hạn, hai câu tuyển phân giải được nếu một câu chứa một literal đối lập với một literal trong câu kia. Phân giải thức của hai literal đối lập nhau (P và ˥ P) là câu rỗng, chúng ta sẽ ký hiệu câu rỗng là [], câu rỗng không thoả được.

Giả sử G là một tập các câu tuyển (bằng cách chuẩn hoá ta có thể đưa một tập các công thức về một tập các câu tuyển). Ta sẽ ký hiệu R(G) là tập câu bao gồm các câu thuộc G và tất cả các câu nhận được từ G bằng một dãy áp dụng luật phân giải.

Luật phân giải là luật đầy đủ để chứng minh một tập câu là không thỏa được. Điều này được suy từ định lý sau:

Định lý phân giải:

Một tập câu tuyển là không thỏa được nếu và chỉ nếu câu rỗng [9] ∈ R(G).

Định lý phân giải có nghĩa rằng, nếu từ các câu thuộc G, bằng cách áp dụng luật phân giải ta dẫn tới câu rỗng thì G là không thỏa được, còn nếu không thể sinh ra câu rỗng bằng luật phân giải thì G thỏa được. Lưu ý rằng, việc dẫn tới câu rỗng có nghĩa là ta đã dẫn tới hai literal đối lập nhau P và ˥ P (tức là dẫn tới mâu thuẫn).

Từ định lý phân giải, ta đưa ra thủ tục sau đây để xác định một tập câu tuyển G là thỏa được hay không. Thủ tục này được gọi là thủ tục phân giải.

Dễ thấy, nếu G là tập các câu hữu hạn thì các literal có mặt trong các câu của G là hữu hạn. Do đó, số các câu tuyển thành lập được từ các literal đó là hữu hạn. Vì vậy, chỉ có một số hữu hạn câu được sinh ra bằng luật phân giải. Thủ tục phân giải sẽ dừng lại sau một số hữu hạn bước.

Chỉ sử dụng luật phân giải ta không thể suy ra mọi công thức là hệ quả logic của một tập công thức đã cho. Tuy nhiên, sử dụng luật phân giải ta có thể chứng minh được một công thức bất kì có là hệ quả của một tập công thức đã cho hay không bằng phương pháp chứng minh bác bỏ. Vì vậy luật phân giải được xem là luật đầy đủ cho bác bỏ. Thủ tục chứng minh bác bỏ bằng luật phân giải xem [9, 17]

˥ A ∨ ˥ B ∨ P (1)

˥ C ∨ ˥ D ∨ P (2)

˥ E ∨ C (3)

A (4)

E (5)

D (6)

Giả sử ta cần chứng minh P. Thêm vào G câu sau:

˥ P (7)

áp dụng luật phân giải cho câu (2) và (7) ta được câu:

˥ C ∨ ˥ D (8)

Từ câu (6) và (8) ta nhận được câu:

˥ C (9)

Từ câu (3) và (9) ta nhận được câu:

˥ E (10)

Tới đây đã xuất hiện mâu thuẫn, vì câu (5) và (10) đối lập nhau. Từ câu (5) và (10) ta nhận được câu rỗng [9].

Vậy P là hệ quả logic của các câu (1) --(6).

Thông thường chúng ta có thể bảng chân lý để chứng minh tính đúng đắn của môt biểu thức. Nhưng phương pháp đó tỏ ra cồng kênhf và có tính “thủ công”. Thay vào đó, chúng ta có thể sử dụng hai thuật toán sau đây để chứng minh biêu thức là đúng hoặc sai

Thuật toán Havard (1970)

Bước 1: Phát biểu lại giả thiết (GT) và kết luận của bài toán dưới dạng chuẩn sau: GT₁,GT₂,…, GT_n → KL₁,KL2,…, KLm

Trong đó các GT_i, KL_j được xây dựng từ các biến mệnh đề và các phép nối ∧ ,∨,˥,

Bước 2: Bước bỏ phủ định (nếu cần). Khi cần bỏ các các phủ định: chuyển vế GTi sang vế kết luận KLj và ngược lại (giống như chuyển dấu âm trong đai số từ vế phai sang trái và ngược lại)

Bước 3: Thay dấu “∧” ở GT_i và “∨” ở KL_j bằng các dấu “,”

Bước 4: Nếu GT_i còn dấu “∨” và KL_j còn dấu “∧” thì tách chúng thành hai dòng con

Bước 5: Một dòng được chứng minh nêu tồn tại chung một mệnh đề ở cả hai vế

Bước 6: Bài toán được chứng minh khi và chi khi tất cả các dòng được chứng minh. Ngược lại thì bài toán không được chứng minh.

Thuật toán Robin son (1971)

Robíson đã cai tiến thuật toán Havard. Cách thức chứng minh như sau:

Bước 1: Phát biểu lại giả thiết (GT) và kết luận của bài toán dưới dạng chuẩn sau: GT₁,GT₂,…, GT_n → KL₁,KL2,…, KLm

Trong đó các GT_i, KL_j được xây dựng từ các biến mệnh đề và các phép nối ∧ ,∨,˥,

Bước 2: Thay dấu “∧” ở GT_i và “∨” ở KL_j bằng các dấu “,”

Bước 3: Chuyển vế KLj sang vế Gti với dấu phủ định để còn một vế, tức là : GT1,GT2,…, GTn , ˥, KL1,˥, KL2,…, ˥KLm

Bước 4: Xây dựng một mệnh đề mới bằng cách tuyển một cặp mệnh đề từ danh sách các mệnh đề. Nếu mệnh đề mới có các biến mệnh đề đối ngẫu thì mệnh đề đó được loại bỏ.

Bước 5: Bổ sung mệnh đề mới này vào danh sách và lặp lai bươc 4

Bước 6: Bài toán được chứng minh khi và chi khi chỉ còn hai mệnh đề đói ngẫu. Ngược lại thì bài toán không được chứng minh.

Thuật toán này thực chất là chứng minh bằng phản chứng

Biểu diễn tri thức bằng Logic vị từ

Logic mệnh đề cho phép ta biểu diễn các sự kiện. Mỗi kí hiệu trong logic mệnh đề được minh họa như là một sự kiện trong thế giới hiện thực, sử dụng các kết nối logic ta có thể tạo ra các câu phức hợp biểu diễn các sự kiện mang ý nghĩa phức tạp hơn. Như vậy, khả năng biểu diễn của logic mệnh đề chỉ giới hạn trong phạm vi thế giới các sự kiện.

Thế giới hiện thực bao gồm các đối tượng. Mỗi đối tượng có những tính chất riêng để phân biệt nó với các đối tượng khác. Các đối tượng lại có quan hệ với nhau. Các mối quan hệ rất đa dạng và phong phú. Chúng ta có thể liệt kê rất nhiều ví dụ về đối tượng, tính chất, quan hệ.

Đối tượng: một cái bàn, một cái nhà, một cái cây, một con người, một con số...

Tính chất: Cái bàn có thể có tính chất: có bốn chân, làm bằng gỗ, không có ngăn kéo. Con số có thể có tính chất là số nguyên, số hữu tỉ, là số chính phương...

Quan hệ: cha con, anh em, bè bạn (giữa con người); lớn hơn, nhỏ hơn, bằng nhau (giữa các con số); bên trong, bên ngoài nằm trên nằm dưới (giữa các đồ vật)...

Hàm: Một trường hợp riêng của quan hệ là quan hệ hàm. Chẳng hạn, vì mỗi người có một mẹ, do đó ta có quan hệ hàm ứng mỗi người với mẹ của nó.

Mục này dành cho nghiên cứu logic vị từ cấp một với tư cách là một ngôn ngữ biểu diễn tri thức. Logic vị từ cấp một đóng vai trò quan trọng trong biểu diễn tri thức vì khả năng biểu diễn của nó (nó cho phép ta biểu diễn tri thức về thế giới với các đối tượng, các thuộc tính của đối tượng và các quan hệ của đối tượng), hơn nữa, nó là cơ sở cho nhiều ngôn ngữ logic khác.