Lập trình logic ràng buộc (CLP) là một hướng mở rộng của lập trình logic, đã được nhiều người đầu tư nghiên cứu và có thể tìm thấy trong nhiều công trình [1], [2], [3], [8]. Cơ chế lập trình này đưa. | TẠP CHÍ KHOA HỌC Đại học Huế Số 53 2009 NGỮ NGHĨA THỦ TỤC CỦA CHƯƠNG TRÌNH LOGIC CÓ RÀNG BUỘC Trương Công Tuấn Trường Đại học Khoa học Đại học Huế Trần Thị Ngọc Trang Trung tâm Công nghệ thông tin Đại học Huế TÓM TẮT Lập trình logic ràng buộc CLP là một hướng tiếp cân mới trong lập trình logic được ra đời bởi sự kết hợp tính khai báo của lập trình logic với tính hiệu quả của quá trình giải quyết ràng buộc. Trong bài báo này chúng tôi tập trung trình bày ngữ nghĩa thủ tục của chương trình logic có ràng buộc thông qua các dẫn xuất và cây suy dẫn từ đích đồng thời ch ra những điều kiện trên hàm xử lý ràng buộc để đảm Mo rằng ngữ nghĩa này là độc lập với các quy tắc chọn literal trong đích. I. Mở đầu Lập trình logic ràng buộc CLP là một hướng mở rộng của lập trình logic đã được nhiều người đầu tư nghiên cứu và có thể tìm thấy trong nhiều công trình 1 2 3 8 . Cơ chế lập trình này đưa ra một khung hình thức với việc tổng quát hóa các hệ phương trình hạng thức trong lập trình logic thành các ràng buộc từ miền tính toán đã được định nghĩa trước. Việc nghiên cứu ngữ nghĩa của các ngôn ngữ CLP đã thực sự hữu dụng trong việc mô hình hóa hệ thống và giải quyết các bài toán tối ưu phức tạp trong cuộc sống. Trong bài báo này chúng tôi nghiên cứu ngữ nghĩa thủ tục của chương trình logic có ràng buộc và chỉ ra những điều kiện trên hàm xử lý ràng buộc để đảm bảo rằng ngữ nghĩa này là độc lập với các quy tắc chọn literal trong đích. II. Một số định nghĩa và khái niệm cơ sở Phần này chỉ trình bày tóm tắt một số khái niệm cơ sở của chương trình logic có ràng buộc chi tiết đầy đủ hơn cũng như một số khái niệm khác của lập trình logic có thể xem trong 10 . . Miền ràng buộc Định nghĩa . Bộ ký hiệu là một tập hữu hạn khác rỗng các ký hiệu bao gồm các ký hiệu hàm và ký hiệu vị từ. Mỗi ký hiệu có một số tự nhiên kèm theo gọi là bậc của ký hiệu. Bộ ký hiệu thường được ký hiệu là 145 Định nghĩa . Cho bộ ký hiệu Y một Y-cẳu trúc ký hiệu là D là một thể hiện của các ký hiệu trong Y bao
