Phép hợp giải

Dạng chuẩn trước của một công thức chỉnh

Dạng chuẩn trước (prenex normal form) của một CTC đã cho được suy ra bởi áp dụng liên tiếp bốn phép biến đổi sau đây :

Loại bỏ các phép nối → và ↔

Sử dụng các luật tương đương :

(G → H) và ((¬G) ˅ H)

(G ↔ H) và ((G → H) ˄ (H → G))

Ghép các phép nối ¬ với các nguyên tử liên quan

Sử dụng các luật tương đương :

Phân biệt các biến

Dùng luật tương đương để tác động dấu lượng tử lên một biến sơ khởi :

( ∀ size 12{ forall } {}X) P(X) và ( ∀ size 12{ forall } {}Y) P(Y)

( ∃ size 12{ exists } {}X) P(X) và ( ∃ size 12{ exists } {}Y) P(Y) Luật dùng chung các biến

Các phép biến đổi a, b, c dẫn CTC đã cho thành một CTC mới tương đương.

Dịch chuyển các dấu lượng tử

Khi dịch chuyển các dấu lượng tử trong một CTC, ta nhận được một CTC mới tươngđương. Bởi vì sau bước c, không còn sự xung đột giữa các nhãn biến được lượng tử hoá.

Sau bốn bước biến đổi, ta nhận được công thức có dạng chuẩn trước tương đương với CTC đã cho. Phần tiếp theo của các dấu lượng tử được gọi là tiền tố (prefix) và phần còn lại được gọi là ma trận (matrix).

Có nhiều dạng chuẩn trước khác nhau cho cùng một CTC bằng cách áp dụng các luật tương đương nhưng vẫn tuân theo nội dung của các bước a, b, c, d.

Chuyển qua “dạng mệnh đề” của công thức chỉnh

Từ dạng chuẩn trước G’ của CTC G, ta có thể tạo ra dạng mệnh đề (form of clauses) G” từ G bằng cách áp dụng 5 bước chuyển đổi sau đây. Trước tiên cần chú ý rằng nếu các công thức G và G’ luôn luôn tương đương với nhau thì các công thức G và G’’ có thể không tương đương với nhau.

Ta chỉ xét G không nhất quán tương đương với G” không nhất quán. Quan hệ này vẫn đủ cho phép tạo cơ sở cho việc chứng minh tự động sau này.

Loại bởi các dấu lượng tử tồn tại

Cho công thức dạng ( ∃ size 12{ exists } {}X) G(X) và giả sử G(X) được tạo thành từ một hoặc nhiều công thức chỉ được lượng tử hoá toàn thể ( ∀ size 12{ forall } {}) đối với các biến Y1,..., Yn mà thôi. Ta sẽ loại bỏ lượng tử tồn tại ( ∃ size 12{ exists } {}X), sau đó thay thế mỗi vị trí của X trong G(X) bởi một hàm có dạng f(Y1,..., Yn).

Chú ý rằng hàm này phải chứa tất cả các biến được lượng tử hoá toàn thể nằm bên trái lượng tử tồn tại trong công thức ( ∃ size 12{ exists } {}X) G(X). Đây là một hàm cho biết có sự tương ứng giữa các nhóm giá trị của Y1,..., Yn và các giá trị của X. Giá trị của X được chỉ định bởi lượng tử tồn tại ∃ size 12{ exists } {}.

Những hàm như vậy được gọi là các hàm Skolem (Skolem functions). Vì rằng ta không biết gì khác ngoài các tham biến của các hàm này, ta phải sử dụng một ký hiệu gốc để biểu diễn chúng mỗi lần cần thay thế một lượng tử toàn thể khi nó xuất hiện.

Khi không có dấu « ∀ size 12{ forall } {}» nào bên trái của « ∃ size 12{ exists } {}» đã cho, hàm Skolem sẽ không có tham biến, và được gọi là một hằng Skolem (Skolem constant).

Loại bỏ tất cả các dấu lượng tử

Sau bước a trên đây, công thức chỉ còn các dấu lượng tử toàn thể. Với giả thiết rằng tất cả các biến đều được lượng tử hoá toàn thể, ta có thể loại bỏ chúng.

Chuyển qua «dạng chuẩn hội»

Trong bước này, người ta sử dụng các luật kết hợp và phân phối đối với các phép toán logic ˅ và ^ để rút gọn CTC nhận được chỉ còn toàn là phép hội (conjonction) của các phép hoặc (disjonction) của các mệnh đề hay các trực kiện (literal).

Loại bỏ tất cả các dấu phép toán logic

Phép hội của các mệnh đề nhận được từ bước trên đây được xem như một tập hợp của các mệnh đề một cách truyền thống. Chẳng hạn trong bước trên, ta nhận được tập hợp hai mệnh đề là :

Phân biệt các biến của các mệnh đề

Các mệnh đề trong tập hợp trên đây phải được đặt lại tên biến sao cho không có sự trùng tên. Muốn vậy, ta sử dụng các luật tương đương tổng quát :

đối với các mệnh đề cụ thể

Người ta nói một trực kiện là cụ thể (concrete) nếu nó không chứa các biến.

Chẳng hạn, ¬P(a), Q(a, f(b)) là các trực kiện cụ thể, nhưng ¬P(X), Q(a, f(Y)) không phải là các trực kiện cụ thể.

Một mệnh đề cụ thể là phép hoặc của các trực kiện cụ thể. Cho hai mệnh đề cụ thể :

G = G1 ˅... ˅Gn và

H = ¬ G1˅ H2 ˅... ˅ Hm

với Gi và Hi là các trực kiện cụ thể. Các trực kiện G1 và ¬ G1 có mặt trong G và H tương ứng,được gọi là các trực kiện bù nhau (complementary literals).

Xuất phát từ các mệnh đề cha (parent clauses) là G và H, luật suy diễn, hay phép hợp giải, sẽ tạo ra một mệnh đề:

K = G2 ˅... ˅ Gn ˅ H2 ˅... ˅ Hm

K được gọi là mệnh đề kết quả (resolvent clause) hay kết quả hợp giải (resolvent) của G và H. Người ta cũng nói rằng G và H được hợp giải với nhau (resolved) để tạo thành K. Một kết quả hợp giải là sự loại bỏ các trực kiện bù nhau và tuyển với tất cả các trực kiện khác của các mệnh đề cha.

Một số trường hợp đặc biệt :

• Q là một kết quả hợp giải của các mệnh đề cụ thể P và ¬P ˅ Q(hay P và P→Q). này thực chất là luật suy diễn modus ponens (trên các mệnh đề cụ thể).
• ¬G ˅ K (hay G→K) là kết quả hợp giải của các mệnh đề cụ thể ¬G ¬ H và ˅ H ˅ K (hay G→H và H→K). Quy tắc suy diễn này là một trường hợp đặc biệt của phép hợp giải còn được gọi là phép liên kết (chỉ đối với các mệnh đề cụ thể).
• Các mệnh đề cụ thể G và ¬G được hợp giải với nhau để tạo thành mệnh đề rỗng (empty clause)

- Hai mệnh đề cụ thể không có kết quả hợp giải. Chẳng hạn G và ¬H, với G và H là các nguyên tử khác nhau.

- Hai mệnh đề cụ thể có thể có nhiều kết quả hợp giải. Chẳng hạn hai mệnh đề G ˅ H ˅ K và ¬G¬H˅ L được hợp giải thành H˅¬H˅K ˅L hay thành G˅¬G˅K ˅L là những mệnh đề tương đương.

¬P là một kết quả hợp giải của các mệnh đề cụ thể ¬Q và ¬P ˅ Q(hay ¬Q và P→Q).

này thực chất là luật suy diễn modus tollens.

Trước khi định nghĩa tổng quát phép hợp giải áp dụng cho các mệnh đề không phải luôn luôn cụ thể, cần phải định nghĩa một cơ chế tạo sinh các mệnh đề. Đó là phép hợp nhất.

Khái niêm

Giả sử cho các mệnh đề ¬ G(X) ˅ H(X) và G(f(Y)). Nếu mệnh đề thứ nhất được thay thế bởi ¬G(f(Y)) ˅ H(f(Y)), thì ta có thể mở rộng phép hợp giải cho các mệnh đề cụ thể : loại bỏ các trực kiện bù nhau ¬G(f(Y)) và G(f(Y)) để nhận được mệnh đề H(f(Y)).

Biểu diễn tri thức nhờ logic vị từ bậc một hợp nhất cho phép biến đổi các mệnh đề sao cho có dạng trực kiện bù nhau bằng cách áp dụng các phép thế (substitutions).

Phép thế

Phép thế là một tập hợp hữu hạn các cặp ti size 12{t rSub { size 8{i} } } {}Vi size 12{V rSub { size 8{i} } } {}, trong đó ti là các hạng, còn Vi size 12{V rSub { size 8{i} } } {} là các biến phân biệt. Nếu I = 0, ta nói phép thế là rỗng.

Người ta nói áp dụng một phép thế s = { ti size 12{t rSub { size 8{i} } } {}Vi size 12{V rSub { size 8{i} } } {} } cho một biểu thức bất kỳ E (E là một hạng hoặc một CTC) cho trước là xác định một trường hợp của E theo s. Đó là việc thay thếtất cả các vị trí ban đầu của mỗi biến Vi trong E bởi ti size 12{t rSub { size 8{i} } } {}.

Phép tổ hợp hai phép thế s1và s2, người ta viết quy ước s1 ο size 12{ο} {}s2, là phép thế nhận được bằng cách như sau :

a) Ap dụng s2 cho các hạng của s1.

b) Loại bỏ khỏi s2 các cặp tj Vj sao cho Vj là một biến của s1 (hay sao cho ∃ size 12{ exists } {}ti với ti Vj size 12{ in } {} s1).

c) Tập hợp tất cả các cặp nhận được từ hai bước a) và b) trên đây.

Bộ hợp nhất (unifier)

Người ta nói rằng một tập hợp {Ei}i các biểu thức (hạng hay công thức) là hợp nhất được (unifiable) bởi s hay nói rằng s là bộ hợp nhất của {Ei}i nếu và chỉ nếu mọi phép thế s cho Ei,ký hiệu Eis, là giống nhau. Khi đó, ta ký hiệu biểu thức (duy nhất) sinh ra bởi bộ hợp nhất s là{Ei}s.

Có thể có nhiều bộ hợp nhất cho cùng một tập hợp các biểu thức đã cho.

Người ta gọi r là bộ hợp nhất tổng quát hơn (mgu - more general unifier) của một tập hợp các biểu thức {Ei}i sao cho với mọi bộ hợp nhất s khác của {Ei}i, tồn tại một phép thế s’sao cho s = r ° size 12{ circ } {}s’.

Người ta chứng minh được rằng với mọi tập hợp E hợp nhất được, sẽ tồn tại một mgu và, nếu r1 và r2 là hai mgu của {Ei}, thì {Ei}r1và {Ei}r2 là giống nhau cho tên các biến.

Thuật toán hợp nhất

Sau đây ta xây dựng thuật toán đệ quy UNIFY(E, ) với là phép thế rỗng. Thuật toán tạo ra một mgu cho một tập hợp hữu hạn E các biểu thức hợp nhất được. Nếu E không là hợp nhất được, thuật toán dừng và thông báo.

Thuật toán hợp nhất

Thuật toán sử dụng tập hợp các xung đột, ký hiệu D, của một tập hợp các biểu thức (hạng hay công thức). Tập hợp D này được xây dựng bằng cách quét đồng thời từ trái qua phải mọi phần tử của cho đến khi gặp ký hiệu ở vị trí đầu tiên làm xuất hiện sự sai khác giữa các phần tử này. Sau đó, bằng cách trích mỗi phần tử của một biểu thức (cần phải là hạng hay công thức ngay khi tất cả các hàm và tất cả các vị từ được viết bởi các ký hiệu phân biệt). Biểu thức này bắt đầu từ vị trí xung đột của ký hiệu. Tập hợp các biểu thức như vậy tạo thành D.

Chẳng hạn, cho = { G(X, f(a, Y), G(X, b), G(X, f(a, G(Z))) }

Một xung đột xuất hiện ở vị trí ký hiệu thứ năm. Như vậy :

D = { f(a, Y), b, f(a, g(Z)) }

Trong thuật toán hợp nhất :

- Ở bước 3 trong thuật toán hợp nhất UNIFY( , ), đòi hỏi V phải không xuất hiện trong t : phép thế t cho V sẽ trở nên phức tạp không xác định được, không có kết quả, các biểu thức vẫn luôn phải hợp nhất.

Chẳng hạn :

{ f(X), X } được áp dụng cho G(X, a) và G(f(X), a) sẽ chuyển chúng thành G(f(X), a) và G(f(f(X)), a), v.v...

- Việc kiểm tra «V có mặt trong t không ?» làm cho độ phức tạp tính toán của thuật toán trở nên đáng kể. Trong trường hợp xấu nhất, là có bậc luỹ thừa đối với số phần tử của E. Chẳng hạn :

E = { P(X1, X2,..., Xn), P(f(X0, X0), f(X1, X1), f(X2, X2),..., f(Xn－1, Xn－1)) } Với lời gọi đệ quy thứ nhất :

= { f(X0, X0) X1 }

= { P(f(X0, X0), X2,..., Xn),

P(f(X0, X0), f(f(X0, X0), f(X0, X0)), f(X2, X2),..., f(Xn－1, Xn－1)) } Với lời gọi đệ quy thứ hai :

= { f(X0, X0) X1, f(f(X0, X0), f(X0, X0)) X2 }

Với lời gọi đệ quy thứ ba, tập hợp được thêm phần tử :

f(f(f(X0, X0), f(X0, X0)), f(f(X0, X0), f(X0, X0))) X3

và cứ thế tiếp tục...

Với lời gọi đệ quy thứ n, tham đối cuối cùng của phần tử thứ hai của sẽ có 2n+1－1 xuất hiện của hàm f. Việc kiểm tra «V có mặt trong t không ?» sẽ cần vượt qua tất cả các xuất hiện của f với thới gian là O(2n).

- Tồn tại các thuật toán hợp nhất có độ phức tạp tính toán nhỏ, có thời gian tuyến tính. Tuy nhiên, những thuật toán này chỉ có ý nghĩa nếu bậc của các vị từ và của các hạng cần hợp nhất là lớn.

Hợp giải các mệnh đề bất kỳ

Giả sử cho hai mệnh đề cha G và H không có biến chung (theo bước e, mục II.1.2) và có thể tiến hành hợp giải. Khi đó, tồn tại kết quả hợp giải của G và H. Gọi G, H và kết quả hợp giải của chúng là các tập hợp các trực kiện {Gi} và {Hj}.

Giả sử tồn tại một tập hợp con {Gi’} của {Gi} (i’ nhận một số giá trị của i), và một tập hợp con { Hj’} của {Hj } sao cho tập hợp các trực kiện :

L = { Gi’} size 12{ union } {} { ¬Hj’ }

là hợp nhất được.

Giả sử r là một mgu của L, một kết quả hợp giải của G và H là một tập hợp các trực kiện được xác định như sau :

({Gi}- {Gi’}) r size 12{ union } {} ({Hj} {}-{Hj’}) r

Tuy nhiên, trước khi kết luận rằng không tồn tại kết quả hợp giải, ít ra cũng phải kiểm tra các mệnh đề đã cho có các biến phân biệt nhau. Chẳng hạn :

G(X, a) và ¬G(f(X), X)

không có kết quả hợp giải. Nếu viết lại mệnh đề thứ hai thành ¬G(f(Y), Y) thì xuất hiện một mpu { f(X) X, a Y}, từ đó có thể suy ra tồn tại một kết quả hợp giải là mệnh đề rỗng.

Như vậy, sự phân biệt các tên biến của các mệnh đề cha chỉ hợp pháp lúc gọi thuật toán hợp nhất. Việc tìm một kết quả hợp giải giữa G(X, X) và ¬G(f(X), X) đòi hỏi phải viết lại mệnh đề thứ hai thành ¬G(f(Y), Y). Lúc này, phép thế { f(X) X } dẫn đến kết quả là hai mệnh đề G(f(Y), f(Y)) và ¬ G(f(Y), Y) không hợp nhất được.

Một cách trình bày khác của phép hợp giải

còn được trình bày theo một cách khác, gọi là phép nhân tử hoá (factorisation).

Trước tiên, người ta đưa vào phép hợp giải nhị phân (binary resolution principle) như sau. Cho G và H là hai mệnh đề có các biến phân biệt, được ký hiệu bởi các tập hợp các trực kiện {Gi} và {Hj}.

Giả sử Gp và Hp là hai trực kiện của {Gi} và {Hj} một cách tương ứng sao cho Gp và ¬Hq là hợp nhất được. Giả sử r là một mgu của Gp và ¬Hq. Người ta định nghĩa kết quả hợp giải nhị phân (binary resolvent) của {Gi} và {Hj} là tập hợp các trực kiện :

({Gi}- {Gp}) r size 12{ union } {} ({Hj}- {Hq}) r

Ta thấy rằng kết quả hợp giải nhị phân là một trường hợp đặc biệt của phép hợp giải đã giới thiệu ở mục trên đây.

Bây giờ ta đưa vào một luật suy diễn thứ hai được gọi là phép nhân tử hoá. Giả sử G là một mệnh đề gồm một tập hợp các trực kiện.

Giả sử {Li}i = 1.. p là hai hay nhiều trực kiện của G hợp nhất được bởi một mgu r. Xuất phát từ G, bởi phép nhân tử hoá, người ta có thể suy ra mệnh đề nhân tử (factor) của G như sau :

(G - {Li}i = 2.. p) r

Nghĩa là ta đã cho phát sinh Gr nhưng trộn lẫn tất cả các trực kiện Lir thành một trực kiện duy nhất.

Cuối cùng, ta đưa vào phép hợp giải (không nhị phân) như là một luật suy diễn mới bằng cách tổ hợp các phép triển khai trong luật hợp giải nhị phân và trong luật nhân tử hoá. Xuất phát từ hai mệnh đề G và H, phép hợp giải cho phép phát sinh, hoặc một kết quả hợp giải nhị phân của G và H, hoặc một kết quả hợp giải nhị phân của G và một nhân tử của H, hoặc một kết quả hợp giải nhị phân của H và một nhân tử của G, hoặc một kết quả hợp giải nhị phân của một nhân tử của G và một nhân tử của H.

Các kết quả hợp giải nhận được theo định nghĩa thứ nhất cũng có thể nhận được theo định nghĩa thứ hai vừa trình bày.