Báo cáo khoa học: "LẬP TRÌNH LOGIC MODAL"

Chia sẻ: Nguyễn Phương Hà Linh Linh | Ngày: | Loại File: PDF | Số trang:9

Thêm vào BST

Báo xấu

74
lượt xem 4
download

Download Vui lòng tải xuống để xem tài liệu đầy đủ

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.

Chủ đề:

Bình luận(0) Đăng nhập để gửi bình luận!

Lưu

Nội dung Text: Báo cáo khoa học: "LẬP TRÌNH LOGIC MODAL"

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), CNTT-CB ∃ (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ó). 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ị CNTT- CB 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 “,”. 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 ≥ 0 1 , 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 □s ◊ E (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, …, Bn (n>0). B - 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 M, w là p . Đị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 ∈ CNTT-CB W. Khi đó, một công thức φ 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.
Chúng ta nói M thỏa mãn φ (hay φ đúng trong M) và viết M ╞ φ nếu M, τ╞ φ. Với tập T các công thức, chúng ta gọi M là mô hình của T và viết M╞ T nếu M ╞ φ với ∀φ∈ T. Một hệ logic có thể định nghĩa là một tập các công thức được thiết lập đúng đắn (well formed fomulae - wwf), một lớp các thể hiện có thể chấp nhận và một quan hệ thỏa được. Trong đó, lớp các thể hiện có thể chấp nhận được của một hệ logic modal L thông thường là các Kripke frame (được chấp nhận cho L) hạn định một số điều kiện trên đó. Nếu chúng ta định nghĩa một lớp các thể hiện chấp nhận được là lớp tất cả các mô hình Kripke (không hạn định các điều kiện trên các quan hệ có thể truy cập được) thì chúng ta sẽ có được logic modal cấp một miền cố định với các hạng thức cố định gọi là hệ logic K. Hệ logic này được tiên đề hóa bởi các luật sau: Tất cả các tiên đề trong logic vị từ - Tiên đề K: □(φ→ϕ) → (□φ→□ϕ) - Tiên đề Barcan: ∀x□φ → □∀xφ - Tiên đề định nghĩa ◊:◊φ → ¬□¬φ φ, φ → ϕ - Luật Modus Ponens: ϕ φ - Luật sinh: ∀xφ CNTT- CB φ - Luật sinh modal: φ Các tiên đề trong hệ K là đúng đắn và đầy đủ với mọi hệ logic modal. Tiên đề ngược của tiên đề Barcan là □∀xφ → ∀x□φ là hệ quả của các tiên đề trên. Tiên đề này cũng là đúng đắn & đầy đủ. Các tiên đề K, Modus ponens, luật sinh modal là các luật cơ bản nhất trong chứng minh logic. Trong đó, tiên đề K là quan trọng nhất. Mọi hệ logic mà các tiên đề của nó được mở rộng từ tiên đề K được gọi là logic modal thông thường (normal modal logic). Một số tiên đề như D, T, B, 4, 5 tương ứng với các điều kiện xác định trên các quan hệ có thể truy cập được được trình bày trong bảng sau: Tiên đề Luật Điều kiện trên R □φ → ◊φ ∀w∃u R(w,u) D □φ → φ ∀w R(w,w) T φ → □◊φ ∀w, u R(w, u) → R(u, w) B □φ → □□ φ ∀w, u, v R(w, u) ∧ R(u, v)→ R(w, v) 4 ◊φ → □◊φ ∀w, u, v R(w, u) ∧ R(w, v)→ R(u, v) 5
Để chứng minh tính thỏa được của các công thức chúng ta phải dựa vào các tiên đề trong các hệ logic (ví dụ: các tiên đề trong hệ logic K). Hệ logic K là nhỏ nhất (bao gồm ít nhất các tiên đề) và cơ bản nhất (gồm các tiên đề cơ sở) trong việc áp dụng để chứng minh các công thức. Tuy nhiên, với một số trường hợp thì hệ K không đủ mạnh để áp dụng và người ta mở rộng hệ K thành các hệ logic mới bằng cách thêm vào hệ K một số tiên đề (trong bảng trên). Các hệ mới này cũng đã được chứng minh là đúng đắn & đầy đủ. Các hệ logic modal khác K sẽ phải có những hạn định nhất định trên R. Sau đây là quy ước một số ký hiệu dùng trong MProlog + T: ký hiệu hằng giá trị đúng (true). + D, E, F: các nguyên tố cổ điển hoặc T. + X, Y: biến của các nguyên tố cổ điển hoặc T, gọi tắt là biến nguyên tố. + : ◊ được gán nhãn E. + : ◊ được gán nhãn X. + ∇: □, ◊, hoặc được gọi là toán tử modal + Δ: dãy các toán tử modal + A, B: các công thức có dạng E hoặc ∇E, được gọi là các nguyên tố đơn. + α, β: công thức có dạng ΔE, được gọi là các nguyên tố. CNTT-CB + φ, ψ: công thức (có thể chứa hoặc ). Bộ sinh mô hình (Model generator) Bộ sinh mô hình - đó là một tập các thể hiện của mô hình Kripke. Gọi L là một trong những hệ logic modal: KD, T, KDB, B, KD4, S4, KD5, KD45, S5. Với mọi bộ sinh mô hình I, luôn tồn tại một mô hình được gọi là mô hình L chuẩn (standard L model) của I và đó chính là mô hình nhỏ nhất của I [4]. Định nghĩa: (Bộ sinh mô hình [4]) Một bộ sinh mô hình là một tập các nguyên tố nền không chứa ký hiệu toán tử ◊, , T. Một bộ sinh mô hình I được gọi là bộ sinh mô hình thông thường (theo L) nếu: + L ∉ {KD5, KD45, S5} hoặc + L = KD5 và I chỉ chứa các nguyên tố có dạng E, ∇E, □∇E hoặc + L ∈ {KD45, S5} và I chỉ chứa các nguyên tố có dạng E, ∇E Với mọi chương trình MProlog P và hệ logic modal L, luôn tồn tại bộ sinh mô hình nhỏ nhất cho P là IL, P sao cho P ╞ IL, P và mô hình chuẩn theo L của IL, P là mô hình nhỏ nhất theo L của P [4].
Với một bộ sinh mô hình thông thường (theo L) I, chúng ta có thể xây dựng được mô hình nhỏ nhất (theo L) cho I dựa trên các mở rộng theo L của I và mô hình chuẩn theo L của I [4]. Nếu trong lập trình logic cổ điển, với một chương trình P luôn tồn tại mô hình Herbrand nhỏ nhất của P thì trong lập trình logic modal cũng tương tự, luôn tồn tại một mô hình nhỏ nhất được sinh ra từ một bộ sinh mô hình. Với một chương trình MProlog P, hệ logic modal L, luôn tồn tại một mô hình nhỏ nhất cho P theo L, ký hiệu là ML, P. Chi tiết đặc tả về mô hình nhỏ nhất của một chương trình MProlog với hệ logic L được trình bày trong [4]. 2.4. Điểm bất động Tương tự như lập trình logic cổ điển, với một chương trình MProlog P, một hệ logic modal L luôn tồn tại một ánh xạ đơn điệu và liên tục liên kết với nó ký hiệu là TL, P. TL, P: Tập các bộ sinh mô hình → Tập các bộ sinh mô hình. [4] Luôn tồn tại điểm bất động nhỏ nhất của TL, P ký hiệu là IL, P [4]. Và IL, P đối với một chương trình MProlog cũng có vai trò quan trọng trong việc tìm lời giải cho bài toán “xác định tính không thỏa được của P ∪ {G} theo L” (G là một đích MProlog). IL, P là hệ quả logic của P theo L, ký hiệu là P ╞ L IL, P. Chứng minh trong [4]. Và IL, P cũng chính là ML, P [4]. CNTT- Với một chương trình MProlog P, một bộ sinh mô hình thông thường (theo L) I, chúng ta CB muốn áp dụng các câu trong P vào I để đạt được các bộ sinh mô hình khác và lặp lại quá trình trên với bộ sinh mô hình mới cho đến khi đạt được điểm bất động – đó chính là bộ sinh mô hình nhỏ nhất. 2.5. Thuật giải SLD Tư tưởng cơ bản của thuật giải SLD đối với một chương trình MProlog cũng tương như trong lập trình logic cổ điển. Thuật giải SLD áp dụng với một chương trình MProlog P và đích MProlog G để xác định câu trả lời đúng đắn của P ∪ {G} trong một hệ logic modal L. Trong phần này, sẽ tập trung vào các ví dụ minh họa cho thuật giải SLD. Ví dụ : Cho một chương trình MProlog P gồm các công thức sau: φ1 = ◊p1(a) ← ; φ2 = □(p2(X) ← p1(X)); φ3 = □(□p3(X) ← p1(X), p2(X)); φ4 = □p4(X) ← p3(X); φ5 = □(p5(X) ← p4(X)) Và đích G = ← □p5(X) Sau đây là thủ tục phản bác SLD của P ∪ {G} trong hệ logic KDB với câu trả lời tính toán là {X/ a}.
Đích Câu vào / luật Phép thế biến ← □p5(X) ← □p4(X1) φ5 {X / X1} ← p3(X2) φ4 {X1 / X2} rSatKDB 2 ← □p3(X2) ←p1(X4), p2(X4) φ3 {X2 / X4} ← p2(a) φ1 {X4 / a, Y / p1(a)} ← p1(a) φ2 {X5 / a} φ1 ε □ III. KẾT LUẬN Có thể thấy quá trình giải quyết một bài toán trong lập trình logic modal gồm hai giai đoạn. Giai đoạn thứ nhất là quá trình xác định và chứng minh những tiên đề nào được phép áp dụng trong miền của bài toán (dựa trên các hạn định, ràng buộc). Từ đó xây dựng hệ logic của bài toán đã cho. Giai đoạn thứ hai là việc biểu diễn bài toán bằng các luật của logic modal và chạy chương trình với một trình dịch xác định. Quá trình suy diễn để tìm ra câu trả lời cho bài toán được thực hiện dựa trên các luật của chương trình và các luật của hệ logic modal của bài toán. Sự khác biệt cơ bản giữa lập trình logic cổ điển và lập trình logic modal là trong lập trình logic cổ điển ta không cần phải xây dựng hệ logic cho bài toán. Sở dĩ có điểm khác biệt này là CNTT-CB do lập trình logic modal có thêm hai toán tử modal □ và ◊ nên trong quá trình suy diễn phải áp dụng thêm các luật trong hệ logic nào đó để biến đổi các toán tử modal này (do các luật của chương trình không biến đổi được các toán tử modal). Tài liệu tham khảo [1]. Hồ Thuần. Bài giảng Lập trình logic và Prolog. Đại học KHTN Huế. 1999. Tiếng Anh [2]. John Durkin. Expert system. Prentice Hall International Inc, 1994. [3]. J.W. Lloyd. Foundations of Logic Programming, 2nd Edition. Springer-Verlag. 1987 [4]. L.A. Nguyen. A fixpoint semantics and an SLD-resolution calculus for modal logic programs. Fundamenta Informaticae, 55(1):63–100, 2003. [5]. L.A. Nguyen. MProlog: An extension of Prolog for modal logic programming. In B. Demoen and V. Lifschitz, editors. Proceedings of ICLP 2004, LNCS 3132, Springer. 2004. [6]. L.A. Nguyen. Reasoning about Epistemic States of Agent by Modal Logic Programming. 2004 [7]. L.A. Nguyen. Source files, calculi, and examples of MProlog. Available on Internet at http://www.mimuw.edu.pl/~nguyen/mProlog, 2004. [8]. L.A. Nguyen. The modal logic programming system MProlog. In J.J. Alferes and J.A. Leite, editors. Proceedings of JELIA 2004, LNCS 3229, Springer. 2004. [9]. Patrick Blackburn. Maarten de Rijke, Yde Venema. Modal logic. PB, MdR, YV. 1998♦