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 □...
Nội dung trích xuất từ tài liệu:
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ụ ...