Ngôn ngữ vị từ bậc một
Cú pháp của ngôn ngữ vị từ bậc một Trong ngôn ngữ vị từ bậc một (first-order predicate language), bằng cách sử dụng một bảng ký hiệu đặc biệt, người ta đưa vào các khái niệm hạng (term), nguyên tử (atom), trực kiện ...
Cú pháp của ngôn ngữ vị từ bậc một
Trong ngôn ngữ vị từ bậc một (first-order predicate language), bằng cách sử dụng một bảng ký hiệu đặc biệt, người ta đưa vào các khái niệm hạng (term), nguyên tử (atom), trực kiện (literal) và công thức chỉnh (well-formed formula) để xây dựng các biểu thức đúng (correct expressions).
Bảng ký hiệu
Bảng ký hiệu để xây dựng các biểu thức đúng gồm :
- Các dấu phân cách (separator signs) là dấu phẩy ( , ), dấu mở ngoặc ( ( ) và dấu đóng ngoặc ( ) ).
- Các hằng (constant) có dạng chuỗi sử dụng các chữ cái in thường a..z.
a, block.
- Các biến (variable) có dạng chuỗi sử dụng các chữ cái in hoa A..Z.
X, NAME.
- Các vị từ (predicate) được viết tương tự các biến, là các chuỗi sử dụng các chữ cái in hoa A..Z.
ISRAINING, ON(table), P(X, blue), BETWEEN(X, Y, Z).
Khi cần thao tác trên một vị từ nào đó, cần phải ghi rõ bậc (arite) hay số các đối (argument) của vị từ đó. Bậc là một số nguyên dương. Ví dụ, trong một ứng dụng nào đó, bậc của các vị tự ISRAINING, ON, P và BETWEEN lần lượt là 0, 1, 2 và 3. Khi bậc có giá trị cố định là 0, vị từ còn được gọi là mệnh đề (proposition). Chẳng hạn ISRAINING, EMPTY là các mệnh đề.
- Các hàm (function), có cách viết tương tự các hằng, sử dụng các chữ in thường a..z. Mỗi hàm cũng có bậc (hay số lượng các đối) cố định, là một số nguyên dương.
f(X), weight(elephan), successor(M, N) là các hàm có bậc lần lượt là 1, 1, và 2. Người ta quy ước rằng các hằng là những hàm bậc không (nil).
a, elephan, block là các hằng.
- Các phép nối logic (logical connector) là ¬,˅,˄,→ và ↔ tương ứng với các phép phủ định, và, hoặc, kéo theo và kéo theo lẫn nhau.
- Dấu ∃ size 12{ exists } {}là lượng tử tồn tại (existential quantifier) và ∀ size 12{ forall } {} là lượng tử toàn thể (universal quantifier).
Hạng (term)
Hạng được tạo thành từ hai luật sau :
- Các hằng và các biến là các hạng.
- Nếu f là một hàm có bậc n size 12{ >= {}} {} 1 và nếu t1,..., tn đều là các hạng, thì hàm f (t1,..., tn) cũng là một hạng.
Các hàm successor(X, Y) hay weight(b) hay successor(b, wight(Z)) đều là các hạng, nhưng P(X, blue) không phải là hạng vì P là một vị từ hay weight (P(b)) cũng không phải là hạng vì P(b) không phải là một hạng (không thể làm đối cho một hàm).
Nguyên tử (atom)
Nguyên tử được tạo thành từ hai luật sau :
- Các mệnh đề (vị từ bậc 0) là các nguyên tử.
- Nếu P là một vị từ bậc n (n size 12{ >= {}} {} 1) và nếu t1,..., tn đều là các hạng, thì P(t1,..., tn) cũng là một nguyên tử.
P(X, blue), EMPTY, BETWEEN(table, X, sill(window)) là các nguyên tử. Còn successor (X, Y), sill (window) ây thì không phải nguyên tử.
Các công thức chỉnh
Các công thức chỉnh (viết tắt CTC) được tạo thành từ ba luật sau :
- Các nguyên tử là các CTC.
- Nếu G và H biểu diễn các CTC,
thì (¬G), (G ˅H), (G ˄H), (G → H) và (G ↔ H) cũng là các CTC do được tạo thành từ các phép nối lôgich giữa G và H.
- Nếu G là một CTC và X là một biến,thì ( ∃ size 12{ exists } {}X)G và ( ∀ size 12{ forall } {}X)G cũng là các CTC.
( ∃ size 12{ exists } {}X)G được đọc là tồn tại một biến X sao cho G được thoả mãn.
( ∀ size 12{ forall } {}X)G được đọc là với mọi biến X thì G đều được thoả mãn.
Các công thức sau đây là chỉnh :
( ∃ size 12{ exists } {}X) ( ∀ size 12{ forall } {}Y) ((P(X, Y) Q(X, Y) → R(X))
((¬ (P(a) → P(b))) → ¬P(b))
còn (¬f(a)) : phủ định của một hàm,
và f (P(a)) : hàm có đối là một vị tư, đều không phải là CTC.
- Một CTC được gọi là một trực kiện (literal) hay một trị đúng nếu nó là một nguyên tử hay có dạng (¬G), với G là một nguyên tử.
- Trong một CTC, trước hoặc sau các ký tự nối, ký tự phân cách, các hằng, các biến, các hàm, các vị từ, người ta có thể đặt tùy ý các dấu cách (space hay blank).
Từ nay về sau ta quy ước rằng, trong một công thức, nếu có một biến được lượng tử hóa, tức là biến xuất hiện ngay theo sau ký hiệu ∀ size 12{ forall } {} hay ∃ size 12{ exists } {} thì từ đó trở đi, tất cả các vị trí đứng sau của cùng biến này cũng được lượng tử hóa.
Một CTC có thể chứa các biến không được lượng tử hóa, chúng được gọi là những biến tự do (free variable).
P(X) và ( ∃ size 12{ exists } {}Y) Q(X, Y) là các CTC có chứa biến tự do X.
- Logic vị từ được gọi là «bậc một» (first-order) vì trong định nghĩa các CTC không chứa các lượng tử cho vị từ hay cho hàm.
( ∀ size 12{ forall } {}P)P(a) và ( ∀ size 12{ forall } {}f) ( ∀ size 12{ forall } {}f) ( ∀ size 12{ forall } {}X) P(f (X), b)
không phải là những CTC logic vị từ bậc một, mà có bậc cao hơn (higher-order).
Các luật suy diễn (inference rule)
Một luật suy diễn là cách biểu diễn sao cho từ một hoặc nhiều CTC, có thể suy dẫn(derive) thành các CTC khác. Chẳng hạn các luật suy diễn sau đây :
- Luật suy diễn modus ponens : Từ hai CTC lần lượt là G và (G →H), có thể suy dẫn ra CTC H (ở đây vẫn quy ước rằng các tên như G, H phải được thay thế bởi các CTC mà chúng biểu diễn).
- Luật suy diễn modus tollens : Từ các CTC là (¬H) và (G → H), ta suy dẫn ra được
(¬G). Người ta viết quy ước hai luật suy diễn trên như sau :
- Luật suy diễn chuyên dụng (universal specialization), nếu từ một CTC có dạng : ( ∀ size 12{ forall } {}X) G(X) và từ một hằng bất kỳ, chẳng hạn «a», có thể suy dẫn thành CTC :
G(a) nghĩa là mọi vị trí X trong G được thay thế bởi a.
Cho trước một tập hợp cố định các luật suy diễn, người ta có thể xem xét họ các bài toán sau : Từ một tập hợp các CTC đã chọn, bằng cách áp dụng một số hữu hạn lần nào đó các luật suy diễn, có thể nhận được một CTC đã cho trước hay không ?
Các CTC được chọn lúc đầu được gọi là các tiên đề (axiom). Các CTC nhận được bằng cách áp dụng các luật suy diễn được gọi là các định lý (theorem). Một dãy các áp dụng các luật suy diễn từ các tiên đề dẫn đến định lý là một phép chứng minh (proving) của định lý.
Một số kỹ thuật hợp giải vấn đề (problem resolution) thuộc lĩnh vực «Trí tuệ nhân tạo» như tìm kiếm trong không gian các trạng thái, có thể được xem như việc tìm kiếm một chứng minh cho một định lý đã cho. Theo nghĩa không gian các trạng thái, tập hợp các tiên đề có thể xem là một trạng thái đầu, các luật suy diễn đóng vai trò là các phép chuyển trạng thái, các trạng thái đích sẽ là tập hợp các CTC trong đó có chứa định lý cần chứng minh.
Ngữ nghĩa của ngôn ngữ vị từ bậc một
Sau đây, ta sẽ nghiên cứu cách sử dụng các CTC để biểu diễn và suy luận trên các giá trị chân (truth value) của các tri thức đã có để tìm được giá trị chân của các tri thức khác.
Diễn giải (Interpretation)
Một diễn giải của một CTC G, ký hiệu I, được xác định từ năm bước sau đây :
- Chọn một miền diễn giải (interpretation domaim) ký hiệu là D với D size 12{ <> } {} Ø, nghĩa là một tập hợp khác rỗng các phần tử.
- Gán (assignation) cho mỗi hằng của G một phần tử của D.
- Gán cho mỗi mệnh đề (hay vị từ có bậc 0) một phần tử của tập hợp giá trị {true, false}.
Để đơn giản ta ký hiệu F là trị false và T là trị true.
- Gán cho mỗi vị từ bậc n (n size 12{ >= {}} {} 1) một ánh xạ từ Dn size 12{D rSup { size 8{n} } } {} lên { T, F } : P( X1,... Xn ) : {}Dn size 12{D rSup { size 8{n} } } {} → { T, F }
- Gán cho mỗi hàm bậc n (n size 12{ >= {}} {} 1) một ánh xạ từ Dn size 12{D rSup { size 8{n} } } {} lên D : P( X1,... Xn ) : Dn size 12{D rSup { size 8{n} } } {} →D.
Người ta nói rằng đã có một diễn giải I từ G lên D :
Cho các miền diễn giải D1, D2, D3 và các CTC
G1 : ( ∀ size 12{ forall } {}X) P(X)
G2 : ( ∀ size 12{ forall } {}X) ( ∃ size 12{ exists } {}Y) Q(X, Y)
G3 : ( ∀ size 12{ forall } {}X) (R(X) → T (f (X), a))
Ta xây dựng các diễn giải Ii của Gi lên Di, i = 1.. 3, như sau :
Đôi khi, người ta nói một diễn giải là không đầy đủ nếu trong đó, các phép gán cần thiết chỉ được đặc tả từng phần.
Giá trị một công thức theo diễn giải
Cho một diễn giải I của một miền D cho một công thức G.
- Nếu G là một mệnh đề, khi đó, giá trị gán cho G do định nghĩa của I được gọi là giá trịcủa G theo I.
- Nếu G là một trực kiện mà không phải là một mệnh đề, khi đó, với mỗi phép lựa chọn C các giá trị trong D cho các biến của G (nếu tồn tại), ta nhận được một giá trị true hay false theo cách định nghĩa I. Giá trị này được gọi là giá trị của G theo I đối với lựa chọn C các giá trị của các biến.
Chẳng hạn, trong công thức G3 ở trên được diễn giải theo I3, nguyên tử T(f(X), a) nhận giá trị T nếu X được gán phần tử 4 của D3, và cũng nhận giá trị T nếu X nhận một giá trị khác (giả sử 5) của D3.
- Nếu G có dạng ( ∀ size 12{ forall } {}X)G’, ta định nghĩa giá trị của G theo I là T (true) nếu giá trị của G’ theo I cho mọi giá trị của biến X (trong D) là T, nếu không là F (false). Chẳng hạn, giá trị của G1 được diễn giải theo I là F.
- Nếu G có dạng ( ∃ size 12{ exists } {}X)G’, ta định nghĩa giá trị của G theo I là T (true) nếu giá trị của G’ theo I đối với ít nhất một giá trị của biến X (trong D) là T, nếu không là F (false).
Chẳng hạn, giá trị của Q(X, Y) được diễn giải theo I2 là T khi gán 1 cho X và 3 cho Y. Từ đó suy ra rằng giá trị của ( ∃ size 12{ exists } {}Y)Q(X, Y) theo I2, khi X nhận giá trị 1, là T. Ngược lại, giá trị của G2 theo I2 là F.
- Nếu G có dạng (¬G’), người ta định nghĩa giá trị của ¬ G’ theo I, khi giá trị này của G’ theo I được định nghĩa, căn cứ theo bảng sau :
| Giá trị của G’ theo I | Giá trị của (¬G’) theo I (giả sử G) |
| T | F |
| F | T |
- Nếu G có dạng (G’ ˅ G’’), hoặc (G’ ˄G’’), hoặc (G’ → G’’), hoặc (G’ ↔ G’’), người ta định nghĩa giá trị của G theo I, khi các giá trị của G’ và G’’ theo I được định nghĩa, căn cứ theo các bảng chân lý (truth table) tương ứng sau :
Chẳng hạn, giá trị của G3 theo I3 là T.
Khi một công thức G là T theo một diễn giải I, người ta nói rằng diễn giải I là một mô hình của G.
Giá trị của một công thức theo một diễn giải đã cho được định nghĩa theo cách qua lại tương hỗ ngay khi tất cả các biến được lượng tử hoá.Tính hợp thức / không hợp thức, tính nhất quán / không nhất quán
Một công thức được gọi là hợp thức (valid) nếu và chỉ nếu mọi diễn giải đều cho giá trị T. Nếu không, nó được gọi là không hợp thức (non - valid).
Một công thức được gọi là không nhất quán (inconsistent) nếu và chỉ nếu với mọi diễn giải đều cho giá trị F. Nếu không, nó được gọi là nhất quán (inconsistent).
Công thức G1 là nhất quán vì diễn giải I’1 sau đây trả về cho nó giá trị T :
I’1 : D = {1} P(1) T Q(1) T
Tuy nhiên, nó là không hợp thức vì diễn giải I’’1 sau đây trả về giá trị F :
I’’1 : D = {1} P(1) F Q(1) T
Công thức G2 là hợp thức vì nếu không, giả sử I là một diễn giải thuộc miền D làm sai G2, khi đó tồn tại một giá trị «a» của X, lấy trong D, sao cho (P(a) ˅ (¬P(a))) là F, mà điềunày không thể xảy ra do cách định nghĩa các phép ˄ và ˅. Như vậy, G2 phải là hợp thức.
Công thức G3 là không hợp thức vì nếu không, giả sử I là một mô hình của G, I phải làm thoả mãn ( ∃ size 12{ exists } {}Y) (¬P(Y)), khi đó tồn tại một giá trị «a» trong D, sao cho P(a) có giá trị F, nhưng ( ∀ size 12{ forall } {}X) (P(X) không thể thoả mãn trên D. Như vậy, G3 phải là không hợp thức.
- Một số tác giả gọi các công thức hợp thức là các hằng đúng (tautology) và các công thức không nhất quán là các mâu thuẫn (contradiction).
- X) → (MAN(X) → MORTAL(X)). gợi ý rằng « tất cả mọi người đều chết » và công thức là hợp thức. Thực tế, công thức này là nhất quán, nhưng không hợp thức, vì giá trị trả về của công thức phụ thuộc vào diễn giải theo biến X.
Tính không quyết định được và tính nửa quyết định được
Khi một công thức không chứa các biến, người ta có thể sử dụng các bảng chân lý để tiến hành một số hữu hạn các phép toán nhằm xác định một công thức đó là hợp thức hay không,có nhất quán hay không. Vấn đề trở nên vô cùng phức tạp khi các công thức có chứa biến vàcác dấu lượng tử.
Người ta đã chỉ ra rằng trong logic vị từ bậc một, không thể tìm được một thuật toán tổng quát để quyết định xem với chỉ một số hữu hạn phép toán, một công thức bất kỳ nào đó đã cho có là hợp thức hay không. Do vậy, người ta gọi logic vị từ bậc một là không quyết định được (indecidability) (theo định lý về tính không quyết định được của A. Church xây dựng năm 1936).
Tuy nhiên, người ta có thể xây dựng các thuật toán tổng quát để quyết định tính hợp thức của một số họ các CTC. Đặc biệt, tồn tại các thuật toán đảm bảo tính hợp thức ngay từ đầu khi ứng dụng một CTC hợp thức nào đó, bằng cách dừng lại sau khi áp dụng một số hữu hạn (nhưng không bị chặn trên) các phép toán để kết luận rằng công thức đã cho là hợp thức. Một thuật toán như vậy khi áp dụng cho một công thức không hợp thức có thể không bao giờ dừng. Chính vì vậy mà người ta nói logic vị từ bậc một là nửa quyết định được (half - decidability).
Công thức tương đương
Hai CTC G và H được gọi là tương đương nếu và chỉ nếu chúng có cùng giá trị (T hoặc F) cho mọi diễn giải. Người ta viết : với mọi diễn giải I, I(G) = I(H).
(P(a) → Q(b)) và ((¬P(a) ˅ Q(b)) là tương đương. Có thể kiểm tra lại kết quả bằng bảng chân lý.
- G, H, K là các CTC bất kỳ,
- G(X), H(X) là các CTC với X là biến tự do,
biểu diễn một CTC hợp thức,
biểu diễn một CTC không nhất quán.
Bảng các công thức tương đương
Hậu quả logic
Công thức G được gọi là hậu quả logic từ các công thức H1,..., Hn nếu và chỉ nếu mọi mô hình của H1,..., Hn là một mô hình của G.
P(a) là hậu quả logic của ( ∀ size 12{ forall } {}X) P(X)
( ∀ size 12{ forall } {}X) Q(X) là hậu quả logic của ( ∀ size 12{ forall } {}X) ((¬P(X)) ˅ Q(X)) và ( ∀ size 12{ forall } {}X) P(X)
Dễ dàng chỉ ra rằng G là hậu quả logic của H1,..., Hn nếu và chỉ nếu :
((H1 ˄... ˄ Hn) → G) là hợp thức, hay nếu và chỉ nếu (H1 ˄... ˄ Hn) ˅ (¬G)) là không nhất quán.
Ta thấy rằng việc định nghĩa các luật suy diễn, rồi đưa ra các định lý và chứng minh là độc lập với các khái niệm diễn giải (đưa vào các giá trị true và false), tương đương và hậu quả logic.
Nhóm các luật suy diễn «đúng đắn» (sound)
Khi các định lý, nhận được bằng cách áp dụng một nhóm các luật suy diễn đã cho, là hậu quả logic một cách hệ thống từ một tập hợp các tiên đề bất kỳ nào đó, người ta nói rằng nhóm các luật suy diễn này là đúng đắn.
Dễ dàng chỉ ra rằng các luật suy diễn modus ponens và chuyên dụng đã nói trước đây là đúng đắn.
Nhóm các luật suy diễn «đầy đủ»
Một nhóm các luật suy diễn đã cho là đầy đủ đối với phép suy diễn (deduction complete) nếu với bất kỳ một tập hợp các CTC, mọi hậu quả logic của chúng đều được dẫn đến từ chúng như những định lý, nghĩa là bởi áp dụng một số hữu hạn lần các luật suy diễn của nhóm.
Nhóm các luật suy diễn chỉ được rút ra từ luật modus ponens sẽ không là đầy đủ đối với phép suy diễn, ( ∀ size 12{ forall } {}X) (G(X) ˅H(X)) là một CTC hậu quả logic của hai CTC ( ∀ size 12{ forall } {}X) G(X) và ( ∀ size 12{ forall } {}X) H(X). Nhưng công thức đầu tiên chỉ có thể được suy diễn từ hai công thức này bởi modus ponens mà thôi.
Vì sao cần «đúng đắn» hay «đầy đủ» ?
Trong hệ thống hợp giải càc bài toán, logic vị từ bậc một thường dùng để biểu diễn những khẳng định là đúng hay sai trong những miền ứng dụng chuyên biệt. Người ta quan tâm đến phép suy diễn các CTC.
Nếu ta lấy các luật suy diễn trong những hệ thống này, thì một cách tự nhiên, chúng phải tạo thành nhóm «đúng đắn».
Rõ ràng người ta mong muốn nhóm các luật phải đầy đủ. Nghĩa là mọi hậu quả logic của các tiên đề phải là một định lý và do vậy phải được làm rõ bởi dẫn xuất các luật suy diễn. Tuy nhiên trong thực tế, không phải luôn luôn như vậy.
Sau đây ta sẽ chỉ ra một luật suy diễn quan trọng là phép hợp giải (principle of resolution), hay nói gọn là hợp giải (resolution).
