Nếu G là một tập hợp các mệnh đề và phép hợp giải là một luật suy diễn đúng đắn và đầy đủ (đối với phép bác bỏ), ta có thể khẳng định rằng :

«G không nhất quán» cũng có nghĩa là «tồn tại một phép bác bỏ của G bởi hợp giải».

Tương tự, nếu G là tập hợp các CTC : «CTC H là hậu quả logic của G» tương đương với «tồn tại một phép bác bỏ của tất cả các dạng mệnh đề G ˄¬H».

Xét các CTC : ( $\forall$ X) ( $\exists$ Y) (¬P(X) →Q(Y) et ( $\forall$ Z) (P(b) → R(a, z)), nếu ta muốn chứng minh rằng : ¬R(a, b) → ( $\exists$ U) Q(U), thì ta có thể tìm kiếm phép hợp giải từ tập hợp các mệnh đề :

{ P(X) □ Q(f(X)), ¬P(b) □ R(a, Z), ¬R(a, b), ¬Q(U) }

Sau đây ta sẽ tìm các phương pháp luận của nguyên lý hợp giải để xây dựng phép bác bỏ.

Thủ tục tổng quát bác bỏ bởi hợp giải

Giả sử rằng ta muốn chứng minh rằng CTC H là hậu quả lôgic của tập hợp các mệnh đề :

G = { Gi }

Thủ tục bác bỏ tổng quát không đơn định (non-deterministic) như sau :

- Căn cứ vào các tính chất của tính hoàn toàn đối với phép bác bỏ của nguyên lý hợp giải, nếu H thực sự hậu quả lôgic của G, thì sẽ tồn tại ít nhất một dãy các lựa chọn (bước 3.1) dẫn đến mệnh đề rỗng và do đó thủ tục dừng.

Thủ tục trên đây không đảm bảo rằng một dãy như vậy nếu quả thật tồn tại thì sẽ tìm thấy. Các giai đoạn 3.1 và 3.2 sẽ không đơn định và rất thô sơ. Chẳng hạn, thủ tục này giải nhiều lần cùng một cặp mệnh đề từ cùng trực kiện.

Chiến lược hợp giải

Thủ tục tổng quát CHỨNG - MINH - BỞI - HỢP - GIẢI có thể được làm mịn hơn tại các bước 3.1 và 3.2. Theo cách chọn lựa các mệnh đề và các trực kiện của chúng, người ta có thể định nghĩa nhiều chiến lược bác bỏ bởi hợp giải. Một trong những chiến lược này lả hạn chế hay sắp xếp các lựa chọn mệnh đề và trực kiện để hợp giải tuỳ theo tiêu chuẩn đặc thù của chúng.

Một chiến lược hợp giải được gọi là đầy đủ đối với phép bác bỏ nếu tồn tại một phép bác bỏ bởi hợp giải của tập hợp G ban đầu, nghĩa là tồn tại một dãy hợp giải dẫn đến mệnh đề rỗng, thì cũng tồn tại một hợp giải làm thoả mãn các tiêu chuẩn lựa chọn hay thứ tự riêng cho chiến lược này.

Người ta cũng biểu diễn tính hoàn toàn đối với phép bác bỏ của một chiến lược hợp giải S theo cách sau. Ký hiệu :

R c(G) phép hợp của tập hợp mệnh đề G với tất cả các kết quả hợp giải (resolvent) của tất cả các cặp mệnh đề của G, có thể nhận được bằng cách tuân theo các tiêu chuẩn biểu diễn bởi C, gắn với chiến lược S.

R_{c^{p1}} (G) = R_{c} (R_{c^{p}} (G))

Chiến lược hợp giải S là đầu đủ nếu và chỉ nếu với mọi tập hợp không nhất quán các mệnh đề,tồn tại một sô nguyên dương n sao cho mệnh đề rỗng thuộc $R_{c^{p}} (G)$ :

- Tính hoàn toàn của một chiến lược hợp giải (đối với phép bác bỏ) không đồng nghĩa với tính hoàn toàn của một nguyên lý hợp giải (đối với phép bác bỏ).

- Các chiến lược không đầy đủ có thể có ích lợi thực tiễn.

- Một chiến lược là đầy đủ không có nghĩa là khi làm thoả mãn các tiêu chuẩn lựa chọn hay thứ tự tìm thấy một cách tất yếu, với một số hữu hạn các mệnh đề, mệnh đề rỗng xuất phát từ tất cả tập hợp G không nhất quán các mệnh đề. Sau đây, khi một chiến lược có tính chất này, người ta nói là đầy đủ trực tiếp.

Đồ thị định hướng, đồ thị tìm kiếm và đồ thị bác bỏ

Với mọi hệ thống các luật suy diễn, cho trước một hệ tiên đề, người ta có thể biểu diễn tập hợp các định lý được suy ra (và cách suy ra chúng) dưới dạng một đồ thị được gọi là đồ thị định hướng.

Trong trường hợp của nguyên lý hợp giải, các đỉnh là các mệnh đề và các cung nối các mệnh đề cha đến các mệnh đề kết quả resolvents.

Cho tập hợp các mệnh đề :

{ P(X) □ Q(f(X)), ¬P(b) □ R(a, Y), ¬R(a, b), ¬Q(Z) }

ta có thể vẽ đồ thị định hướng như sau :

Ký hiệu □ chỉ mệnh đề rỗng □ . Để đồ thị được rõ ràng, người ta đặt song song các kết quả hợp giải được dẫn đến từ nhiều cặp mệnh đề cha và không vẽ mũi tên cho các cung. Từ đồ thị định hướng này, ta có thể trích ra các đồ thị bác bỏ, chẳng hạn đồ thị sau :

Sau đây ta sẽ xem xét một cách ngắn gọn một số chiến lược tương ứng với nhiều cách tìm kiếm các đồ thị bác bỏ bên trong một đồ thị định hướng. Phần đồ thị định hướng rõ ràng để tìm ra một đồ thị bác bỏ được gọi là đồ thị tìm kiếm.

Chiến lược hợp giải bởi bác bỏ theo chiều rộng(breadth first resolution)

Trong chiến lược này, người ta gán cho mỗi mệnh đề một độ sâu có giá trị :

0 đối với các mệnh đề ban đầu,

1 đối với các kết quả hợp giải của các cặp mệnh đề có độ sâu 0,

...

n đối với các kết quả hợp giải của các cặp mệnh đề có độ sâu n-1.

Cách người ta đặt độ sâu là làm sao cho không tạo ra một mệnh đề có độ sâu p khi mà có khả năng tạo ra một mệnh đề có độ sâu p1. Rõ ràng rằng khi một kết quả hợp giải xuất hiện lần đầu tiên, thì nó sẽ có độ sâu sâu nhất có thể nhận được từ hai mệnh đề cha.

Ví dụ trên đây có thể áp dụng chiến lược hợp giải bởi bác bỏ theo chiều rộng để dẫn đến tại thời điểm dừng một đồ thị tìm kiếm như sau :

Từ đồ thị tìm kiếm này, ta có thể trích ra đồ thị bác bỏ sau :

- Chiến lược này không cấm việc tạo ra một phần tử nào đó của đồ thị định hướng của tập hợp mệnh đề G, nhưng chi phối tính rõ ràng của đồ thị định hướng bằng cách làm xuất hiện tập hợp $R^{p} (G)$ trước $R^{p1} (G)$ . Chiến lược này là đầy đủ.

- Mặt khác, từ G hữu hạn, người ta suy ra rằng R p(G) là hữu hạn, p = 1..n. Như vậy,chiến lược hợp giải bởi bác bỏ theo chiều rộng là đầy đủ trực tiếp : nếu G không nhất quán, thì chiến lược này sẽ làm xuất hiện mệnh đề rỗng.

- Người ta nhận được một phép bác bỏ với mệnh đề rỗng có độ sâu sâu nhất có thể.

Chiến lược hợp giải bởi bác bỏ với «tập hợp trợ giúp»

Cho G là một tập hợp không thoả mãn các mệnh đề và T là một tập hợp con của G, sao cho tập hợp các mệnh đề GT là nhất quán.

Theo định nghĩa, tập hợp trợ giúp của G quan hệ với T (giả thiết thoả mãn tính chất trước đây) gồm các mệnh đề của đồ thị định hướng,hoặc thuộc về T, hoặc là con cháu của T.

Một chiến lược hợp giải (đối với một tập hợp mệnh đề G đã cho) sử dụng tập hợp trợ giúp (set of support resolution) quan hệ với T (GT giả sử nhất quán) sao cho với mỗi hợp giải, ta lấy một mệnh đề cha trong tập hợp trợ giúp quan hệ với T.

Một chiến lược như vậy không hạn chế tính rõ ràng của đồ thị định hướng như chiến lược theo chiều rộng, làm thu hẹp đồ thị tìm kiếm được sinh ra. Ta chứng minh được rằng các chiến lược này là đầy đủ.

Ta có thể tạo ra các kết quả hợp giải mà không thu hẹp đồ thị hơn nữa, bằng cách kiểm tra độ sâu theo cách của chiến lược theo chiều rộng. Trong những điều kiện như vậy, các chiến lược hợp giải với tập hợp trợ giúp là đầy đủ trực tiếp.

Sau đây, ta sẽ biểu diễn một đồ thị tìm kiếm nhận được theo cách này.

Xuất phát từ ví dụ đầu mục trên. Lúc đầu, tập hợp trợ giúp chỉ có các mệnh đề ¬R(a, b)và ¬Q(Z). Các mệnh đề của đồ thị tìm kiếm thuộc về tập hợp trợ giúp được gạch chân.

Từ đó, đồ thị bác bỏ được trích ra như sau :

Chú ý rằng trong ví dụ này, đồ thị tìm kiếm được chứa trong đồ thị nhận được bởi chiến lược theo chiều rộng, và cũng là đồ thị bác bỏ.

Để tiến hành chiến lược tập hợp trợ giúp, cần chọn T sao cho GT là nhất quán. Sau đây là ba phương pháp đơn giản :

1. Định nghĩa T như là tập hợp các mệnh đề không chứa các trực kiện phủ định hay trực kiện âm (một trực kiện phủ định, negative literal, là một nguyên tử có dấu phủ định ¬ đặt trước).

không thể rỗng, nếu không một diễn giải làm cho các trực kiện của T có giá trị T (true) sẽ là một mô hình của G, mô hình này không nhất quán.

Mỗi mệnh đề của G-T sẽ chứa một trực kiện phủ định. Tập G-T sẽ nhất quán vì rằng một diễn giải làm cho tất cả các trực kiện phủ định của G-T có giá trị T sẽ là một mô hình của G-T.

2. Định nghĩa T như là tập hợp các mệnh đề không chứa các trực kiện khẳng định (hay trực kiện dương). Như vậy là nhất quán theo cách suy luận tương tự trên đây.

3. Định nghĩa T như là tập hợp các mệnh đề nhận được bằng cách phủ định CTC cần chứng minh. Trong trường hợp này, là tập hợp các tiên đề mà dễ dàng được xem là nhất quán.

Nếu một tập hợp mệnh đề G là không nhất quán, thì G phải chứa ít nhất một mệnh đề mà các trực kiện đều dương (nếu không, mọi trực kiện của G sẽ chứa ít nhất một trực kiện âm, ta có thể xây dựng một mô hình của G như đã chỉ ra ở phương pháp 1). Từ đó, ta có thể áp dụng chiến lược tập hợp trợ giúp theo phương pháp 1 trên đây. Tương tự như vậy, G phải chứa ít nhất một mệnh đề mà các trực kiện đều âm, và do đó, ta có thể áp dụng chiến lược tập hợp trợ giúp theo phương pháp 2. Ta có thể kiểm tra trong ví dụ trên đây rằng tập hợp T đã chọn thoả mãn phương pháp 2 và cả phương pháp 3.

Chiến lược hợp giải bởi bác bỏ dùng «khoá»(lock resolution)

Người ta đánh số một cách ngẫu nhiên tất cả các trực kiện của các mệnh đề cho trước. Phép hợp giải của hai mệnh đề chỉ có thể thực hiện được khi số thứ tự của chúng là nhỏ nhất. Các trực kiện của các mệnh đề kết quả (resolvents) thừa kế số thứ tự của các mệnh đề cha (trong trường hợp xảy ra trùng khả năng, người ta lấy lại số thấp nhất).

Chiến lược dùng khoá là đầy đủ.

Mặt khác, có thể sắp đặt, mà không thu hẹp hơn nữa, việc tạo sinh các kết quả hợp giải bằng cách kiểm tra độ sâu của chúng nhờ chiến lược theo chiều rộng. Trong những điều kiện như vậy, các chiến lược khoá là đầy đủ trực tiếp.

Tiến hành đánh số một cách ngẫu nhiên các trực kiện của các mệnh đề đã cho trong ví dụ đầu mục III, ta xây dựng được đồ thị tìm kiếm như sau :

Ở đây, ta thấy đồ thị bác bỏ phủ hoàn toàn lên đồ thị tìm kiếm.

Chiến lược hợp giải bởi bác bỏ là «tuyến tính»

Cho G là tập hợp mệnh đề không nhất quán, chọn C0 là mệnh đề sao cho G{Co} tạo thành tập hợp mệnh đề nhất quán, khi đó C0 được gọi là mệnh đề trung tâm xuất phát.

Mọi kết quả hợp giải cho phép sẽ có C0 là tổ tiên và được gọi là các mệnh đề trung tâm (central clauses).

Chiến lược tuyến tính (linear resolution) chỉ cho phép tiến hành hợp giải giữa một mệnh đề trung tâm CC (lúc đầu C0 là trung tâm) và một mệnh đề biên CB được chọn từ :

Hoặc trong số các mệnh đề của G (được gọi là các mệnh đề vào).
Hoặc trong số kết quả hợp giải tổ tiên (là các mệnh đề trung tâm) của CC.

Một mệnh đề trung tâm chỉ có thể được hợp giải với một mệnh đề trung tâm khác nếu một trong chúng là tổ tiên của mệnh đề kia.

Phép bác bỏ được vẽ theo sơ đồ sau :

Hay, bằng cách thay thế tên các mệnh đề biên trên các cung nối các mệnh đề trung tâm, ta nhận được đồ thị như sau :

Do đồ thị có dáng một đường thẳng nên người ta gọi đây là chiến lược tuyến tính (linear strategy). Tính chất tuyến tính ở chỗ hai mệnh đề trung tâm chiều có thể được hợp giải khi một trong chúng là tổ tiên của mệnh đề kia.

- Đồ thị tìm kiếm cho ở mục trên bởi áp dụng chiến lược theo chiều rộng không thể sinh ra bởi chiến lược tuyến tính, dù với cách chọn C0 nào trong số các mệnh đề ban đầu. Đồ thị bác bỏ cũng không phải là tuyến tính.

- Tương tự như vậy đối với đồ thị tìm kiếm và đồ thị bác bỏ cho ở mục III.2.3 bởi áp dụng chiến lược tập hợp trợ giúp.

- Đồ thị tìm kiếm ở mục trên được tạo bởi áp dụng chiến lược dùng khoá được xem là kết quả của việc áp dụng chiến lược tuyến tính xuất phát từ mệnh đề :

C0 = P(X) ˅Q(f(X)) hay C0 = ¬ P(b) ˅ R(a, Y)

Lúc này, đồ thị bác bỏ nhận được là lẫn lộn với đồ thị tìm kiếm.

- Sau đây là đồ thị tìm kiếm nhận được từ một chiến lược tuyến tính xuất phát từ mệnh đề

C0 = P(X) ∨ Q(f(X)) nhưng không lẫn lộn với đồ thị bác bỏ :

Đồ thị tìm kiếm trên đây nhận được bằng cách lái theo chiều rộng việc áp dụng chiến lược tuyến tính xuất phát từ P(X) □ Q(f(X)).

Các chiến lược tuyến tính là đầy đủ.

Nếu ta sắp đặt việc tạo ra các mệnh đề trung tâm nhờ chiến lược theo chiều rộng, thì chúng là đầy đủ trực tiếp.

Nhớ lại rằng tính hoàn toàn căn cứ vào giả thiết mệnh đề trung tâm xuất phát C0 sao cho G -{C0} là nhất quán. Thông thường, người ta chọn C0 là một trong các mệnh đề lấy ra từ phép phủ định của CTC mà người ta muốn chứng minh, nghĩa là phủ định của sự giả định hay sự phỏng đoán (conjecture).

Ta có thể giả thiết rằng G -{C0} là một tập hợp mệnh đề nhất quán, chỉ gồm các mệnh đề dạng tiên đề và chỉ có một số mệnh đề có tính phỏng đoán. Nếu phủ định sự phỏng đoán chỉ nhận biết được một mệnh đề, thì G -{C0} phải là nhất quán vì rằng đó là tập hợp các tiên đề.

Bây giờ giả thiết rằng phủ định sự phỏng đoán chỉ nhận biết được hai mệnh đề, chẳng hạn C1 và C2. Sự phỏng đoán sẽ có dạng : ¬˅C1 ˅ ¬C2. Nếu G -{C0} là không nhất quán, ta có ¬C2 là hậu quả logic của các tiên đề, có nghĩa rằng sự phỏng đoán ¬C1 ˅ ¬ C2 là không chính xác : ta có thể đề nghị sự phỏng đoán ¬C2 là thích hợp hơn cả.

Nếu vẫn còn hoài nghi về kết quả khắc phục này, người ta có thể vận dụng chiến lược tuyến tính xuất phát từ, một cách liên tiếp, mỗi mệnh đề có được từ phỏng đoán.

Quay lại ví dụ vừa rồi, từ 4 mệnh đề ban đầu đã cho :

{ P(X) □ Q(f(X)), ¬P(b) □ R(a, Y), ¬R(a, b), Q(Z) }

ta thấy hai mệnh đề cuối cùng là kết quả của phép phủ định phỏng đoán :

¬R(a, b) →(∃U) Q(U)

Nếu lấy mệnh đề xuất phát là C0 = ¬R(a, b) và nếu ta áp dụng chiến lược tuyến tính và theo chiều rộng, thì ta nhận được :

Tương tự, xuất phát từ C0 = ¬Q(Z), ta có :

Hình:Đồ thị tìm kiếm chiến lược tuyến tính

Trên đây ta đã giới thiệu một bác bỏ tuyến tính xuất phát từ mệnh đề : C0 = P(X) ∨ Q(f(X)) mà mệnh đề này không là kết quả của phép phủ định phỏng đoán. Thành công của bác bỏ, ngay cả khi tính đến tính không nhất quán của G đã không được bảo đảm ngay từ đầu. Thựctế, người ta có thể kiểm tra sau đó rằng tập hợp G của bốn mệnh đề ban đầu được cho là nhất quán một cách tối thiểu, nghĩa là dù bất kỳ mệnh đề C nào của G, tập hợp G -{C0} là nhất quán.

Từ nhận định này, ta có thể tìm thấy một bác bỏ tuyến tính xuất phát từ mệnh đề cuối cùng như sau :

Chiến lược bác bỏ bởi hợp giải là «tuyến tính theo đầu vào»

Chiến lược bác bỏ bởi hợp giải là «tuyến tính theo đầu vào» (linear input resolution) thực chất là chiến lược tuyến tính (chọn một mệnh đề C0 sao cho tập hợp G -{C0} là nhất quán), nhưng người ta yêu cầu thêm điều kiện chỉ lấy các mệnh đề biên trong số các mệnh đề vào đã cho.

Bốn phép bác bỏ tuyến tính trong mục trên vừa rồi cũng là bác bỏ tuyến tính theo đầu vào.

Nói chung, chiến lược tuyến tính theo đầu vào không là đầy đủ. Ví dụ sau đây là một minh chứng. Cho G là tập hợp các mệnh đề vào :

G = {P(a) □Q(X), P(Y) □ ¬ Q(Y), ¬ P(Z) ¬ Q(Z), ¬ P(U) □ Q(U)}

Sử dụng chiến lược tuyến tính theo đầu vào, xuất phát từ ¬ P(Z) □ ¬ Q(Z), ta nhận được đồ thị bác bỏ như sau :

Đồ thị bác bỏ chiến lược tuyến tính theo đầu vào

Trong ví dụ này, ta không thể nhận được phép bác bỏ tuyến tính theo đầu vào. Mỗi mệnh đề vào thuộc G đều có hai trực kiện. Để từng đôi trực kiện cùng được loại bỏ với nhau đối với phép hợp giải, cần thực hiện phép nhân tử hoá trong quá trình hợp giải, điều này là không thể xảy ra đối với mỗi một trong bốn mệnh đề vào.

Tuy nhiên, chiến lược tuyến tính theo đầu vào là đầy đủ (chỉ với hợp giải nhị phân mà không nhân tử hoá) nếu áp dụng cho tập hợp không nhất quán các mệnh đề Horn (người ta sẽ nói : đầy đủ đối với mệnh đề Horn). Các mệnh đề Horn là những mệnh đề chỉ chứa nhiều nhất một trực kiện dương, như :

¬R(a, b), ¬P(b) ˅R(a, Y).

Cả 4 mệnh đề trong ví dụ ở mục trên đều không phải là mệnh đề Horn. Dẫu sao ta cũng đã tạo ra 4 phép bác bỏ tuyến tính theo đầu vào : các chiến lược không đầy đủ theo lý thuyết, nhưng thực tiễn, chúng vẫn có hiệu quả.

Chiến lược hợp giải «LUSH»

Chiến lược hợp giải «LUSH» là sự vận dụng của «chiến lược tuyến tính theo đầu vào» với ưu điểm thu hẹp các hợp giải cho phép. Trong mệnh đề trung tâm hiện hành, người ta chọn một cách ngẫu nhiên một trực kiện và chỉ để ý đến những hợp giải chứa trực kiện cố định này.Chiến lược hợp giải «LUSH» là đầy đủ (chỉ với hợp giải nhị phân) đối với các mệnh đề Horn.

«LUSH» viết tắt từ cụm từ «Linear resolution with Unrestricted Selection function for Horn clauses». Ở đây, «Unrestricted» có nghĩa là việc chọn trực kiện trong mỗi mệnh đề trung tâm là tuỳ ý (nhưng không phải là tuỳ tiện).

Xét các tiên đề sau đây :

a1 : (∀X) EQUAL(X, X) thể hiện phép phảnxạ của quan hệ EQUAL.

a2 : (∀U) (∀V) (∀W) ((EQUAL(U, V) ∧ EQUAL (WV)) → EQUAL (U, W)

thể hiện phép nửa－phảnxạ (half－transitivity).

Ta muốn chứng minh rằng :

(∀X) (∀Y) EQUAL (X, Y) → EQUAL (Y, X) có nghĩa là đốixứng(symmetry). Thật vậy, ta có thể chứng minh trực tiếp : từ a2, bằng cách lấy V=U, ta có :

(∀U) (∀W) (EQUAL (U, U) ∧ EQUAL (W, U)) → EQUAL (U, W)).

Nhưng từ a1, ta được :

(∀U) (∀W) EQUAL (W, U) → EQUAL (U, W) dpcm.

Bây giờ ta có thể dùng phép bác bỏ để chứng minh. Ta cần chứng minh tính không nhất quán của :

a'1 : EQUAL (X, X)

a'2 : ¬EQUAL (U, V) ¬EQUAL (W, V) EQUAL (U, W)

c'1 : EQUAL (a, b)

c'2 : ¬EQUAL (b, a)

Sau đây là đồ thị hợp giải nhị phân theo đầu vào :

- Trong mục trên, ta đã chỉ ra rằng khi một tập hợp mệnh đề đã cho là không nhất quán thì phải tồn tại một mệnh đề không có trực kiện dương, và cần phải có một mệnh đề không có trực kiện dương tham gia vào mọi phép chứng minh tính không nhất quán bằng hợp giải. Trong ví dụ trên đây, ta đã phải chọn mệnh đề xuất phát là c'2 vì tập hợp các mệnh đề còn lại tạo thành một tập hợp nhất quán : toàn bộ trực kiện đều dương.

- Khi áp dụng các mệnh đề Horn, xuất phát từ một mệnh đề không có trực kiện dương, ta chỉ có thể tạo ra được các kết quả hợp giải cũng không có trực kiện dương.

- Khi một tập hợp các mệnh đề Horn là không nhất quán, thì cần phải có một mệnh đề đơn vị (unitary) (là mệnh đề chỉ có một trực kiện duy nhất) trong chúng là dương. Trong trường hợp này, nói chung sẽ tồn tại một phép bác bỏ (bởi hợp giải nhị phân) sao cho mỗi lần hợp giải, một trong các mệnh đề cha phải là một mệnh đề đơn vị dương.

Ví dụ minh hoạ : bài toán tìm người nói thật

Trên một hòn đảo nọ có hai loại người : những người thành thật luôn luôn chỉ nói sự thật và những người dối trá luôn luôn chỉ nói dối. Mỗi người dân của đảo hoặc là một người thành thật, hoặc là một người dối trá.

Một người nước ngoài đến đảo và gặp ba người dân của đảo là A, B và C. Ông ta hỏi A :«Ông là một người thành thật hay là một người dối trá ?». A trả lời ấp úng nên người nước ngoài nọ không hiểu gì. Ông ta quay sang hỏi B : «Anh ta đã nói gì vậy ?». B trả lời : «Anh ta đã nói rằng anh ta là người dối trá». Lúc này, C nói xen vào : «Ông đừng tin B, anh ta nói dối đấy !».

Hãy xác định xem B và C là những người thành thật hay là dối trá ?

Lời giải :

Ta sẽ biểu diễn các câu hỏi và câu trả lời trên đây bởi các công thức logic. Gọi S (sincere), L (lie) và SAY là các vị từ với quy ước như sau :

- S(X) chỉ rằng X luôn là người thành thật,

- L(X) chỉ rằng X luôn là người dối trá,

- SAY(X, Y) chỉ rằng X nói Y.

Ta có :

1. Mọi người dân trên đảo là thành thật hoặc dối trá : (∀X) S(X)) ˅ L(X)

2. Không có người nào lại vừa thành thật lại vừa dối trá : (∀X) ¬S(X) ˅ ¬L(X)

3. Nếu X là thành thật và nếu anh ta nói Y, thì Y là đúng :

(∀X) (∀Y) (S(X) ˄SAY(X, Y)) → Y)

4. Nếu X là dối trá và nếu anh ta nói Y, thì Y là sai : (∀X) (∀Y) (L(X) ˄ SAY(X, Y)) → ˄Y)

5. Nếu Y là đúng và nếu X nói Y, thì X là thành thật :

(∀X) (∀Y) (Y ˄ SAY(X, Y)) → S(X)

6. Nếu Y là sai và nếu X nói Y, thì X là dối trá : (∀X) (∀Y) (¬Y) ˄ SAY(X, Y)) →L(X)

7. Câu trả lời của A : SAY(a, không_thể_hiểu_được))

8. Câu trả lời của B : SAY(b, SAY(a, L(a)))

9. Câu trả lời của C : SAY(c, L(b))

Các hằng a, b, c biểu diễn ba người dân trên đảo ; hằng không_thể_hiểu_được biểu diễn câu nói lắp của A. Ta thấy có thể có nhiều cách để biểu diễn các vị từ. Trong các công thức 3,4, 5, 6 biến Y có thể được xem như là một ký hiệu vị từ. Trong công thức 8, các ký hiệu vị từ SAY và L được xem như các ký hiệu hàm, tương tự đối với L trong công thức 9.

Để làm việc với logic các vị từ bậc một, ta sẽ chỉ dùng một ký hiệu vị từ duy nhất là C. Ký hiệu C(X) có nghĩa đúng (Correct) là X. Có thể bỏ các vị từ S, L và SAY bằng cách thay vào các hàm là s, l và say (tuy nhiên vẫn có thể giữ vị từ S mà không thay nó bởi hàm s). Lúc này ta nhận được 9 công thức mới như sau :

1. (∀X) C(s(X)) ˅C(s(X))

2. (∀X) ¬C(s(X)) ˅ ¬C(s(X))

3. (∀X) (∀Y) (C(s(X)) ˄ C(say(X, Y))) → C(Y)

4. (∀X) (∀Y) (C(l(X)) ˄ C(say(X, Y))) → ¬C(Y)

5. (∀X) (∀Y) (C(Y) ˄ C(say(X, Y))) → C(s(X))

6. (∀X) (∀Y) (¬C(Y) ˄C(say(X, Y))) → C(s(X))

7. C(say(a, không_thể_hiểu_được))

8. C(SAY(b, say(a, l(a))))

9. C(SAY(c, l(b)))

Bây giờ ta chuyển 9 công thức này thành các mệnh đề, trừ mệnh đề đầu tiên đã là mệnh đề Horn, lần lượt được đánh số như sau :

Để tiến hành quá trình bác bỏ, ta cần chọn một phỏng đoán và thêm các mệnh đề nhận được bởi phủ định phỏng đoán này vào 9 mệnh đề trên.

Trước hết, ta phỏng đoán rằng B là một người dối trá, nghĩa là C(l(b)), khi đó cần thêm vào mệnh đề phủ định ¬C(l(b)). Tiếp theo, ta cần chọn một chiến lược tổng quát để tiến hành bác bỏ bởi hợp giải từ các chiến lược :

xây dựng tập hợp trợ giúp (tập hợp nào ?),
dùng khoá (cách đánh số các trực kiện như thế nào ?),
tuyến tính (mệnh đề nào được chọn làm mệnh đề xuất phát ?), v.v...

Mặt khác, cần chỉ rõ chiến lược hợp giải là theo chiều rộng hay chiều sâu ?

Dù chọn chiến lược nào và với lý do nào, việc tổ hợp các hợp giải cũng gặp rất khó khăn. Giả sử mệnh đề ¬C(l(b)) được đánh số là 0, sau đây là một quá trình bác bỏ :

Hợp giải 7 với 3, rồi lấy kết quả hợp giải với 1 :

7. Hợp giải 15 với 0, tức C(l(b)) với ¬C(l(b)), ta nhận được mệnh đề rỗng.Vậy ta đã chứng minh được rằng B là một người dối trá.

Ta nhận thấy rằng chiến lược bác bỏ trên đây không là tuyến tính, mà tương thích với chiến lược tập hợp trợ giúp. Các mệnh đề 2, 5 và 9 đã không được sử dụng. Chẳng hạn để xác định B là người như thế nào thì mệnh đề 9 với sự có mặt của C sẽ trở nên thừa.

Việc đưa ra các hợp giải khác nhau và các kết quả hợp giải khác nhau để có được phép bác bỏ cuối cùng là bổ ích. Chẳng hạn, kết quả hợp giải từ 8 và 3 có nghĩa rằng hoặc B không phải là người thành thật, hoặc quả đúng A đã nói rằng anh ta là người nói dối.

Phép hợp giải của 15 với 2, rồi lấy kết quả hợp giải với 11 dẫn đến C(s(c)). Nếu tiếp tục phỏng đoán rằng C là người nói dối, thì ta cần thêm vào mệnh đề ¬C(s(c) để hợp giải với C(s(c)), kết quả là một mệnh đề rỗng. Việc chứng minh C là người nói dối không sử dụng đến mệnh đề 5.

Cũng cần chú ý rằng thay vì sử dụng phép bác bỏ với phỏng đoán đã cho, ta có thể đưa ra các hợp giải bằng cách theo dõi sự không xuất hiện mệnh đề rỗng mà xuất hiện một trong bốn trực kiện C(l(c)), C(s(b)), ¬C(l(c)), ¬C(s(b)).

Thực tế, dạng thức vừa vận dụng trên đây không trung thành với phát biểu liên quan đến cách biểu diễn thái độ của A. Theo mệnh đề 7 thì ta đã xử lý câu trả lời của A như là một hằng, là không_thể_hiểu_được. Để tuân thủ điều này, ta đã cố tình không nói «A đã nói rằng anh ta là người thành thật», tức s(a), hay không nói «A đã nói rằng anh ta là người nói dối», tức l(a), vì rằng hằng không_thể_ hiểu_được không tương thích với các hạng s(a) hay l(a).

Tuy nhiên, mặc dù với hạn chế bổ sung như vậy, ta vẫn có thể nhận được mệnh đề rỗng, tức chứng minh được điều phỏng đoán. Để biểu diễn câu phát biểu một cách sát thực hơn, tacó thể thay thế mệnh đề 7 bởi mệnh đề 7’ :

7’. C(say(a, l(a))) ˅C(say(a, s(a)))

với giả thiết rằng dù là người thành thật hay là người nói dối, A chỉ trả lời trực tiếp vào câu hỏi của người lạ, mà không trả lời thật thà hay dối trá khác với kiểu «tôi là người thành thật», hay «tôi là người người nói dối», như là «ông là nước ngoài», hay «ông không phải là nước ngoài», hay là một câu nào đó đại loại như «B là người này người kia».

Nếu cải chính mệnh đề 7 bởi mệnh đề 7’ và thay vì dùng mệnh đề : C(say(a, không_thể_hiểu_được)) mà dùng một trong các trực kiện C(say(a, l(a))) hay C(say(a, s(a))), thì phép bác bỏ trên đây không còn duy nhất : mệnh đề rỗng không được sinh ra.

Sau đây là một phép bác bỏ khác không dùng đến mệnh đề 7’ :

Vậy B là một người nói dối. Phép hợp giải đã không dùng đến mệnh đề 9 (có sự tham gia của C), 5 và 7’. Đây là kết quả của một chiến lược tuyến tính, tuy nhiên vẫn có thể áp dụng chiến lược tập hợp trợ giúp.

Hợp giải 5 với 13’, cho kết quả hợp giải với 9 để nhận được C(s(c)), cuối cùng hợp giải C(s(c)) với ¬C(s(c)) nhận được mệnh đề rỗng, vậy C là người thành thật.

Các giai đoạn bác bỏ hình thức trên đây liên quan đến việc xác định B và C rất gần gũi với việc suy luận theo ngôn ngữ tự nhiên như sau :

«Không thể nào một người thành thật hay một người nói dối lại nói : “Tôi là người nói dối”, vì rằng một người thành thật thì không thể nói dối, còn một người dối trá thì không khi nào dám nói lên sự thật. Do vậy, A không nói rằng anh ta là một người nói dối và B nói dối khi nói rằng A đã khẳng định rằng anh ta là người nói dối. Do vậy, B là một người nói dối. Vì C đã nói rằng B đã nói dối, nên C đã nói lên điều đúng, nên C là một người thành thật».

Bài tập

Cho các ví dụ sử dụng cú pháp của ngôn ngữ vị từ bậc một :

a. Bảng ký hiệu

b. Hạng (term)

c. Nguyên tử (atom)

d. Các công thức chỉnh

Thế nào là tính hợp thức và không hợp thức, tính nhất quán và không nhất quán của một công thức ? Thế nào là tính không quyết định được và tính nửa quyết định được của logic vị từ bậc một?

Cho các ví dụ về công thức chỉnh và phép biến đổi mệnh đề.

Từ các ví dụ đã cho trong giáo trình, tự cho các ví dụ về các chiến lược hợp giải tìm kiếm và bác bỏ.

Tìm một ví dụ khác tương tự bài toán tìm người nói thật.

Các hệ thống bác bỏ bởi hợp giải