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 CSTT 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.
Giả sử chúng ta có một tập hợ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 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ỏ.
3.4. Luật phân giải. Thủ tục chứng minh bác bỏ bằng luật phân giải
Để thuận tiện cho việc sử dụng luật giải, chúng ta sẽ cụ thể hoá luật giải trên các dạng câu đặc biệt quan trọng.
Luật giải trên các câu tuyển:
A1 .... Am C
CB1 ..... Bn
A1 ....AmB1 ...Bn
trong đó Ai, Bj và C là các literal.
Luật giải trên các câu Horn:
Giả sử Pi (1im), Rj (1jn), Q và S là các literal. Khi đó ta có các luật sau P1 ....Pm S Q,
R1 .... Rn S
P1 ...Pm R1 ... Rn Q
Một trường hợp riêng hay được sử dụng của luật trên là
P1 ... Pm S Q,
S
P1 ...Pm Q
Khi ta có thể áp dụng luật giải cho hai câu, thì hai câu này được gọi là hai câu giải được và kết quả nhận được khi áp dụng luật giải cho hai câu đó được gọi là giải thức của chúng. 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 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. Giải thức của hai literal đối lập nhau (P và P) là câu rỗng.
Ký hiệu câu rỗng là [] (hoặc ), 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). 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 [] 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 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.
Input Tập G các câu tuyển
Output: Kết luận G thỏa được hay không thỏa được. Procedure Resolution;
Begin
1. Repeat
1.1. Chọn hai câu A và B thuộc G;
1.2. if A và B phân giải được then tính Res (A, B) ;
1.3. if Res (A, B) là câu mới then thêm Res (A, B) vào G;
until
nhận được [] hoặc không có câu mới xuất hiện;
2. if nhận được câu rỗng then thông báo G không thoả được
else thông báo G thoả được;
End;
Nhận xét: nếu G là tập hữu hạn các câu 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 giải được xem là luật đầy đủ cho bác bỏ. Sau đây là thủ tục chứng minh bác bỏ bằng luật giải:
input Tập G các công thức;
Công thức cần chứng minh H; Output: Kết luận H được chứng minh. Procedure Refutation_Proof
Begin
End;
1. Thêm H vào G;
2. Chuyển các công thức trong G về dạng chuẩn hội;
3. Từ các dạng chuẩn hội ở bước hai, thành lập tạp các câu tuyển G‟;
4. Áp dụng thủ tục giải cho tập câu G‟;
5. if G‟ không thoả được then thông báo H là hệ quả logic; else thông báo H không là hệ quả logic của G;
Ví dụ 3.6 Giả giử G là tập hợp các câu tuyển sau
AB P (1)
CDP (2)
EC (3)
A (4)
E (5)
D (6)
Hãy chứng minh P.
Ta thêm vào G câu sau:
P (7)
áp dụng luật giải cho câu (2) và (7) ta được câu:
CD (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.
Vậy P được chứng minh.
Ví dụ 3.7 Cho các câu sau:
1) QT S
2) APQ C
3) PQ B 4) BC T
5) PA
6) PQ
Hãy chuẩn hóa các câu và chứng minh S bằng phản chứng.
- Chuẩn hóa:
+ QT S QTS
+ APQ C APQC
+ PQ B PQB
- Thành lập các câu tuyển:
(1) | |
APQC | (2) |
PQB | (3) |
BC T | (4) |
PA | (5) |
P | (6) |
Q | (7) |
Có thể bạn quan tâm!
-
Nhập môn trí tuệ nhân tạo - 11 -
Cú Pháp Và Ngữ Nghĩa Của Logic Mệnh Đề -
Các Quy Tắc Xây Dựng Các Công Thức -
Sử Dụng Phương Pháp Chứng Minh Phản Chứng. -
Nhập môn trí tuệ nhân tạo - 16 -
Nhập môn trí tuệ nhân tạo - 17
Xem toàn bộ 272 trang tài liệu này.
- Chứng minh S bằng phản chứng: bổ sung S (8)
- Từ (8), (1) QT (9)
- Từ (9), (7) T (10)
- Từ (10), (4) BC (11)
- Từ (5), (6) A (12)
- Từ (12), (6), (7), (2) C (13)
- Từ (3), (6), (7) B (14)
- Từ (13), (14), (11) []
Kết luận: S được chứng minh.
Ví dụ 3.8 Cho các câu sau: 1) (AC) B F
2) E FA
3) GF I
4) (E F) B G
5) BC
Hãy chuẩn hóa các câu và chứng minh I bằng phản chứng.
- Chuẩn hóa:
+ (AC) B F (AC) B F (AC)B F (AB F)(CB F)
+ GF I G F I
+ (E F) B G (E F) BG (EF) BG (E BG) (FBG)
- Thành lập các câu tuyển:
(1) | |
CB F | (2) |
G F I | (3) |
E BG | (4) |
FBG | (5) |
E FA | (5) |
B | (6) |
C | (7) |
- Chứng minh I bằng phản chứng:
+ Bổ sung I (8)
+ Từ (8), (3) G F (9)
+ Từ (6), (7), (2) F (10)
+ Từ (9), (10) G (11)
+ Từ (11), (5) FB (12)
+ Từ (12), (10), (6) []
Kết luận: I được chứng minh.
Ví dụ 3.9 Cho các câu sau:
Nếu trời mưa thì Lan mang theo dù
Nếu Lan mang theo dù thì Lan không bị ướt Nếu trời không mưa thì Lan không bị ướt
a) Xây dựng các câu trên bằng các biểu thức logic mệnh đề
b) Hãy chứng minh rằng"Lan không bị ướt"
- Xây dựng các câu trên bằng các biểu thức logic mệnh đề R="Trời mưa”
U ="Lan mang theo dù” W ="Lan bị ướt”
Lúc đó, ta có các biểu thức logic sau: R U (1)
U W (2)
R W (3)
- Chứng minh rằng"Lan không bị ướt"
+ Giả sử"Lan bị ướt"tức là có W (4)
+ Chuẩn hóa:
(1) RU (5)
(2) UW (6)
(3) (R) W R W (7)
+ Ta có:
(4), (6) U (8)
(8), (5) R (9)
(9), (7) W (10)
(10), (4) câu
- Kết luận: W tứ là"Lan không bị ướt”.
Ví dụ 3.10 Cho các câu sau: A F
A (F P)
PQ D A
AD G
Hãy chứng minh G.
- Chuẩn hóa:
A F AF
A (F P) A F P
PQ D (PQ)D (PD) (Q D) AD G AD G
- Các công thức đã chuẩn hóa:
AF (1)
A F P (2)
PD (3)
Q D (4)
AD G (5) A (6)
- Chứng minh bằng phản chức: Giả sử G (7)
(7), (5)AD (8)
(9) | |
(9), (3) P | (10) |
(6), (1) F | (11) |
(11), (2), (6) P (12)
(12), (10) câu
- Kết luận: G được chứng minh.
Ví dụ 3.11 Cho các câu sau: A B C
B C D
D
Chứng minh: A B.
- Chuẩn hóa:
A B C A B C
B C D B C D
D
- Giả sử: (A B) (A B) A B
- Ta có:
A B C (1)
D | (4) |
A | (5) |
B | (6) |
B C D
- (1), (2) A D (7)
- (7), (4) A (8)
(8), (5) câu
- Kết luận: A B.
Ví dụ 3.12 Cho các câu sau: