LẬP TRÌNH LOGIC MODAL
ĐỖ THANH THUỶ
Bộ môn Mạng và các hệ thống thông tin
Khoa Công nghệ thông tin
Trường Đại học Giao thông Vận tải
Tóm tắt: Lập trình logic modal là một mở rộng của lập trình logic cổ điển bằng cách
thêm vào các toán tử modal (□, ◊) để suy diễn về các luật có thêm yếu tố độ tin cậy (belief), tri
thức (knowledge), thay đổi động (dynamic change)…Bài báo trình bày tổng quan về lập trình
logic modal.
Summary: Modal logic programming is extension of classical predicate logic
programming with two modal operators □ (necessary) and ◊ (possible) to deduce rules with
added factors such as belief, knowledge and dynamic change, …This paper presents overview
of modal logic programming
I. TỔNG QUAN VỀ LẬP TRÌNH LOGIC MODAL
Lập trình logic cổ điển được xây dựng từ những phần tử: hằng, biến, hạng thức, công thức;
các phép toán logic ∧ (hội), ∨ (tuyển), ¬ (phủ định), → (kéo theo) và các lượng từ ∀ (với mọi),
∃ (tồn tại) không giải quyết được các bài toán mà ngoài ngữ nghĩa logic còn có thêm các khái
niệm về không gian, thời gian (không thể biểu diễn được các khái niệm đó dựa trên những phép
toán logic, lượng từ đã có).
CNTT-CB
Lập trình logic modal là một mở rộng của lập trình logic cổ điển bằng cách thêm vào các
toán tử modal (□, ◊) để suy diễn về các luật có thêm yếu tố độ tin cậy (belief), tri thức
(knowledge), thay đổi động (dynamic change)…
Trong logic vị từ công thức ∀xP ⇔ ¬∃x¬P, cũng tương tự trong logic modal □P ⇔
¬◊¬P. Ngữ nghĩa không hình thức của các công thức có thể mô tả như sau:
+ ◊ϕ nghĩa là “Có khả năng xảy ra trường hợp ϕ đúng”;
+ □ϕ nghĩa là “Không thể có khả năng ϕ không đúng” hay nghĩa là “Nhất thiết ϕ đúng”.
Từ ngữ nghĩa đó, chúng ta có □ϕ → ◊ϕ và ϕ → ◊ϕ.
Lập trình logic modal phù hợp để xây dựng các hệ thống tác tử (agent), tác tử thông minh
(intelligent agent), đa tác tử (multiagent). Đó là các hệ thống có khả năng tự trị (autonomous),
khả năng cảm nhận môi trường xung quanh mình đang tồn tại để có những phản ứng thích hợp.
Sử dụng logic modal để biểu diễn sự tin cậy của tác tử, chúng ta viết: □iϕ nghĩa là “agent i
tin cậy ở ϕ” (ϕ là một công thức). Để biểu diễn về tri thức của tác tử, chúng ta viết: □ϕ nghĩa là
“agent hiểu biết ϕ” và như vậy ϕ đúng, …
Trong chứng minh logic, chúng ta viết □ϕ nghĩa là “có thể chứng minh được ϕ đúng”. Ở
đây, công thức □(□P →P) → □P đóng vai trò quan trọng nhất trong các chứng minh logic.
Lý thuyết các mô hình, lý thuyết điểm bất động và thuật giải SLD của lập trình logic modal
hoàn toàn dựa trên các lý thuyết tương ứng và thuật giải SLD của lập trình logic cổ điển.
Bài toán đặt ra của lập trình logic modal cũng tương tự bài toán của lập trình logic cổ điển.
Tuy nhiên, có một khác biệt là nó luôn phải được giải trong một hệ logic modal cụ thể nào đó.
II. KHUNG LÀM VIỆC CỦA LẬP TRÌNH LOGIC MODAL
Tương tự như trong lập trình logic cổ điển, lập trình logic modal cũng có những nguyên lý
cơ bản là: ngữ nghĩa mô hình, ngữ nghĩa điểm bất động và thuật giải SLD. Các nguyên lý này
được xây dựng và thừa kế từ lập trình logic cổ điển.
Tuy nhiên, khác với lập trình logic cổ điển, các mô hình, điểm bất động và thuật giải SLD
của lập trình logic modal luôn gắn cùng với một hệ logic modal cụ thể. Chỉ có một số ít khái
niệm là chung cho mọi hệ logic modal.
2.1. Logic modal cấp một
Một bộ các ký hiệu của logic modal bao gồm: biến; ký hiệu hằng; ký hiệu hàm; ký hiệu vị
từ; các toán tử: ∧, ∨, ¬, →; các toán tử modal □, ◊; các lượng từ ∀, ∃; các ký hiệu dấu ngoặc
“(, )”, dấu phẩy “,”.
CNTT-
CB
Các toán tử □, ◊ có ngữ nghĩa đa dạng, tùy thuộc vào ngữ cảnh. Tuy nhiên, lớp nghĩa phổ
biến nhất là: □ có nghĩa là “cần thiết / nhất thiết”, ◊ có nghĩa là “khả năng / có thể”.
Định nghĩa: (Công thức [4])
Một công thức trong logic modal được định nghĩa quy nạp như sau:
+ Nếu p là một ký hiệu vị từ n-ngôi và t1, t2, … tn là các hạng thức thì p(t1, t2, …, tn) là một
công thức. Và được gọi là nguyên tố cổ điển (classical atom).
+ Nếu φ và ψ là các công thức thì (¬φ), (ψ ∨ φ), (ψ∧ φ), (ψ→ φ), (□ψ), (◊φ) cũng là các
công thức.
+ Nếu φ là một công thức và x là một biến thì (∀x φ), (∃x φ) cũng là các công thức.
Phạm vi của ∀x (tương ứng là ∃x) trong công thức ∀x φ (tương ứng là ∃ x φ) là φ. Một
xuất hiện buộc (bound) của 1 biến trong một công thức là sự xuất hiện của biến đó ngay sau
lượng từ hoặc trong phạm vi của lượng từ (trường hợp cùng một lượng từ cho nhiều biến). Mọi
biến xuất hiện ở các vị trí khác là các biến tự do.
Một công thức đóng (closed formular) là một công thức không có sự xuất hiện của biến tự
do.
Một hạng thức nền là một hạng thức không có biến. Một công thức nền là một công thức
không có các lượng từ và không có biến. Vũ trụ Herbrand là tập tất cả các hạng thức nền. Cơ sở
Herbrand là tập tất cả các nguyên tố cổ điển nền (ground classical atom).
2.2. Ngôn ngữ MProlog
Định nghĩa: (Câu chương trình [4]): Một câu chương trình tổng quát là một công thức có
dạng: □s(A ← B1, …, Bn)
Trong đó: s ≥ 01, n ≥ 0, A, B1, ..., Bn là các công thức có dạng E, □E, ◊E, với E là một
nguyên tố cổ điển (classical atom). □s được gọi là ngữ cảnh modal (modal context). A là phần
đầu (head), B1, ..., Bn là phần thân của câu chương trình.
- Ví dụ: các câu sau: □(p1(X) ← p2(X)). □(□p2(X) ← ◊p3(X)). ◊p3(X) ← p4(X). là các câu
chương trình Mprolog.
Một câu đơn vị là câu chương trình không có phần thân (n=0).
- Ví dụ: p1(a). là một câu đơn vị.
Định nghĩa: Nguyên tố đích MProlog [4] (tổng quát trong mọi hệ logic modal)
Một nguyên tố đích MProlog là một công thức có dạng: □sE hoặc □sE (s 0). ◊ ≥
- Ví dụ: □p1(a), ◊p1(a) là các nguyên tố đích CNTT-CB
Chú ý: s ở đây cũng phụ thuộc vào từng hệ logic mà có miền giá trị khác nhau.
Một câu truy vấn MProlog (Q) là một công thức có dạng: x1, …, xk(B1 … Bn) ∃ ∃ ∧ ∧
(n > 0). Trong đó:
+ x1, …, xk là các biến xuất hiện trong B1, …, Bn
+ mỗi Bi là một nguyên tố đích MProlog.
Một câu đích MProlog (G) là ¬Q.
Ký hiệu: ¬∃x1, …, ∃xk(B1 ∧ … ∧ Bn) là ← B1, …, Bn.
Do đó, câu đích MProlog G = ← B1, …, BB
n (n>0).
- Ví dụ: ← □p1(a), p2(a). ← ◊p1(a). là các câu đích Mprolog
Định nghĩa: (Chương trình Mprolog [4])
Một chương trình MProlog là một tập các câu chương trình.
1 Tùy thuộc vào từng hệ logic mà s có thể có các miền giá trị khác nhau, ví dụ với hệ KD5 thì s ≤ 2, với
hệ KD45 hoặc hệ S5 thì s ≤ 1
2.3. Mô hình và khung làm việc (Model & frame)
Với một công thức φ, tính thỏa được (satisfaction) và tính xác đáng (validity) là quan trọng.
Tính thỏa được hay đúng đắn của công thức phải gắn với một mô hình nào đó còn tính xác đáng
phải gắn với một khung (frame) nào đó. Sau đây chúng ta sẽ định nghĩa mô hình và frame.
Định nghĩa: (Khung làm việc (Frame) [8])
Một frame của ngôn ngữ modal cơ bản là một cặp F = (W, R) thỏa mãn:
+ W là một tập khác rỗng
+ R là một quan hệ nhị phân trên W
Nghĩa là, frame đơn giản là một cấu trúc quan hệ bao gồm một miền giá trị khác rỗng và
một quan hệ nhị phân.
Định nghĩa: (Mô hình (Model) [8])
Một mô hình (model) của ngôn ngữ modal cơ bản là một cặp M=(F, V). Trong đó, F là một
frame, V là một hàm gán mỗi ký hiệu vị từ p trong tập công thức một tập con V(p) Φ ⊆ W.
V(p) là tập các điểm trong mô hình mà p là đúng (true). Hàm V được gọi là hàm lượng giá
(valuation). Khi đó, chúng ta nói mô hình m dựa trên frame F.
Như vậy, cả frame F và mô hình m dựa trên nó đơn giản là các mô hình quan hệ dựa trên
cùng một miền giá trị (vũ trụ), mô hình chính là frame được bổ sung thêm một tập các quan hệ
không có ngôi.
CNTT-
CB Tuy nhiên, frame & mô hình cũng có những điểm khác nhau. Đó là, frame có tính khái
quát hơn, mô hình nhấn mạnh đến các thông tin cụ thể hơn bởi hàm lượng giá V.
Trong lập trình logic, ta quan tâm đến một lớp các frame và lớp các mô hình nhỏ hơn là
Kripke frame và mô hình Kripke.
Định nghĩa: (Kripke frame [4])
Một Kripke frame là một bộ ba (W, , R). Trong đó: τ
+ W là một tập khác rỗng các phần tử.
+ là một phần tử, W. τ τ ∈
+ R là một quan hệ nhị phân trên W, được gọi là quan hệ có thể truy cập được
(accessibility relation).
Nếu R(w, u) đúng thì ta nói phần tử u có thể truy cập được từ w hay u có thể đạt được từ w.
Định nghĩa: Kripke model [4] (Mô hình Kripke với miền giá trị và các hạng thức cố định)
Mô hình Kripke là một bộ M = (D, W, , R, m). Trong đó: τ
+ D là một tập được gọi là miền.
+ (W, , R) là Kripke frame. τ
+ m là một thể hiện của các ký hiệu hằng, ký hiệu hàm, ký hiệu vị từ.
Với một ký hiệu hằng a, m(a) là một phần tử thuộc D, ký hiệu là aM .
Với một ký hiệu hàm n ngôi f, m(f) là một ánh xạ m(f): Dn D, ký hiệu fM. →
Với vị từ n ngôi p và một phần tử w ∈ W, m(w)(p) là một quan hệ n ngôi trên W, ký hiệu
là pM, w.
Định nghĩa: (Phép gán biến [4])
Gọi M là một mô hình Kripke. Phép gán biến đối với M (ký hiệu w.r.t M) là một hàm ánh
xạ mỗi biến vào một phần tử của miền D của mô hình M. Giá trị của hạng thức t trong phép gán
biến V được ký hiệu là V(t) và được định nghĩa như sau:
+ Nếu t là một ký hiệu hằng a thì V(t) = aM
+ Nếu t là một biến x thì V(t) = V(x)
+ Nếu t là một hàm f(t1, …, tn) thì V(t) = fM(V(t1), …, V(tn)).
Sau đây là các định nghĩa về tính thỏa được và tính xác đáng của một công thức trong mô
hình Kripke
Định nghĩa: (Tính thỏa được (satisfaction) của công thức [4])
Cho một mô hình Kripke M = (D, W, , R, m), một phép gán biến V và một phần tử w τ ∈
W. Khi đó, một công thức
CNTT-CB
φ là thỏa được trong mô hình M tại w với phép gán biến V (ký hiệu
M, V, w ╞ ) được định nghĩa như sau: φ
- M, V, w ╞ p(t1, …, tn) nếu và chỉ nếu pM, w(V(t1), …, V(tn))
- M, V, w ╞ ¬φ nếu và chỉ nếu M, V, w
⊭
φ
- M, V, w ╞ φ ∧ ϕ nếu và chỉ nếu M, V, w ╞ φ và M, V, w ╞ ϕ
- M, V, w ╞ φ ∨ ϕ nếu và chỉ nếu M, V, w ╞ φ hoặc M, V, w ╞ ϕ
- M, V, w ╞ φ → ϕ nếu và chỉ nếu M, V, w
⊭
φ hoặc M, V, w ╞ ϕ
- M, V, w ╞ □φ nếu và chỉ nếu với mọi v ∈ W sao cho R(w, v) thì M, V, v ╞ φ
- M, V, w ╞ ◊φ nếu và chỉ nếu tồn tại v ∈ W sao cho R(w, v) thì M, V, v ╞ φ
- M, V, w ╞ ∀xφ nếu và chỉ nếu với mọi a ∈ D sao cho M, V’, w ╞ φ. Ở đây, V’(x) = a và
V’(y) = V(y) với x ≠ y
- M, V, w ╞ ∃xφ nếu và chỉ nếu tồn tại a ∈ D sao cho M, V’, w ╞ φ. Ở đây, V’(x) = a và
V’(y) = V(y) với x ≠ y.
Nếu M, V, w ╞ φ thì ta nói φ đúng tại w trong W với phép gán biến V.
Chúng ta viết M, w╞ φ thay vì viết M, V, w╞ φ với mọi phép gán biến V.