Bài báo này trình bày ngữ nghĩa điểm bất động đối với chương trình logic diễn giải. Đầu tiên, nghiên cứu ngữ nghĩa điểm bất động đối với chương trình logic dạng tuyển dương, trên cơ sở đó xây dựng các phép chuyển đổi chương trình logic, chương trình Horn diễn giải và chương trình logic diễn giải về chương trình logic dạng tuyển không chứa ký hiệu phủ định. | Điểm bất động đối với chương trình logic diễn giải Thông báo Khoa học và Công nghệ Số 1-2015 114 ĐIỂM BẤT ĐỘNG ĐỐI VỚI CHƢƠNG TRÌNH LOGIC DIỄN GIẢI ThS. Trần Thái Sơn Trung Tâm Ngoại ngữ - Tin học Trường Đại học Xây dựng Miền Trung Tóm tắt Chương trình logic diễn giải và chương trình logic dạng tuyển đều là những mở rộng của chương trình logic. Bài báo này trình bày ngữ nghĩa điểm bất động đối với chương trình logic diễn giải. Đầu tiên nghiên cứu ngữ nghĩa điểm bất động đối với chương trình logic dạng tuyển dương trên cơ sở đó xây dựng các phép chuyển đổi chương trình logic chương trình Horn diễn giải và chương trình logic diễn giải về chương trình logic dạng tuyển không chứa ký hiệu phủ định. Cuối cùng xác định ngữ nghĩa điểm bất động thông qua chương trình được chuyển đổi. Từ khóa Abductive Logic Programs Logic Programming Fixpoint Semantics Disjunctive Logic Programs. 1. Ngữ nghĩa điểm bất động đối với chương trình logic dạng tuyển dương Định nghĩa Một chương trình logic là một tập hữu hạn các mệnh đề có dạng sau p q1 . qm qm 1 . qn hoặc q1 . qm qm 1 . qn trong đó n m 0 p và qi là các nguyên tố. Trong mệnh đề vế trái của được gọi là đầu mệnh đề và vế phải của được gọi là thân mệnh đề. Mỗi mệnh đề dạng được gọi là một ràng buộc toàn vẹn với ý nghĩa không thể tất cả q1 qm là đúng và đồng thời tất cả qm 1 qn là sai. Một ràng buộc toàn vẹn còn được gọi là một mệnh đề âm nếu nó không chứa ký hiệu phủ định tức là m n Chương trình logic không chứa ký hiệu phủ định được gọi là chương trình Horn. Chương trình Horn không chứa ràng buộc toàn vẹn được gọi là chương trình logic xác định. Định nghĩa Chương trình logic dạng tuyển dương P là tập hữu hạn các mệnh đề có dạng p1 pl q1 qm l m 0 trong đó pi và qj là các nguyên tố. Thể hiện I thỏa mãn mệnh đề nền p1 pl q1 qm nếu q1 . qm I kéo theo pi I với mọi i 1 i l . I là mô hình cực tiểu của P nếu nó là thể hiện cực tiểu thỏa mãn tất cả các mệnh đề nền từ P. Định nghĩa 8 Cho P là một chương trình .
