Tài liệu Nguyen thi gia bao

BỘ GIÁO DỤC VÀ ĐÀO TẠO ĐẠI HỌC HUẾ TRƢỜNG ĐẠI HỌC KHOA HỌC NGUYỄN THỊ GIA BẢO TÌM HIỂU VỀ LẬP LUẬN SUY DIỄN ĐỐI VỚI CHƢƠNG TRÌNH LOGIC PHỎNG ĐOÁN CÓ CHỨA RÀNG BUỘC CHUYÊN NGÀNH: KHOA HỌC MÁY TÍNH MÃ SỐ: 60 48 01 01 LUẬN VĂN THẠC SĨ KHOA HỌC ĐỊNH HƢỚNG NGHIÊN CỨU NGƢỜI HƢỚNG DẪN KHOA HỌC PGS.TS. TRƢƠNG CÔNG TUẤN Thừa Thiên Huế, 2016 LỜI CAM ĐOAN Tôi cam đoan các kết quả nghiên cứu đƣa ra trong luận văn này dựa trên các kết quả thu đƣợc trong quá trình nghiên cứu của riêng tôi, không sao chép bất kỳ kết quả nghiên cứu nào của các tác giả khác. Nội dung của luận văn có tham khảo và sử dụng một số thông tin, tài liệu từ các nguồn sách, tạp chí đƣợc liệt kê trong danh mục các tài liệu tham khảo. Học viên Nguyễn Thị Gia Bảo LỜI CẢM ƠN Lời đầu tiên, tôi xin chân thành cảm ơn Thầy Trƣơng Công Tuấn đã hƣớng dẫn, định hƣớng và luôn động viên để tôi hoàn thành tốt luận văn này. Xin cảm ơn Quý Thầy, Cô giáo Khoa Công nghệ thông tin Trƣờng Đại học Khoa học – Đại học Huế đã truyền đạt nhiều kiến thức sâu sắc, quý báu về các môn học trong quá trình giảng dạy và các nội dung hoàn thiện luận văn. Xin cảm ơn các bạn học viên lớp cao học Khoa học máy tính khóa 2014– 2016 và các đồng nghiệp đã luôn bên cạnh, động viên tôi trong suốt thời gian học tập và thực hiện luận văn. Cuối cùng, tôi xin đƣợc bày tỏ lòng biết ơn sâu sắc tới toàn thể gia đình, bạn bè đã luôn động viên, khích lệ tinh thần để tôi có đủ nghị lực hoàn thành luận văn này. Xin chân thành cảm ơn tất cả! Huế, tháng 7 năm 2016 MỤC LỤC Trang Lời cam đoan ............................................................................................................... Lời cảm ơn ................................................................................................................... Mục lục ......................................................................................................................... Danh mục các hình ...................................................................................................... Danh mục các chữ viết tắt .......................................................................................... Danh mục các thuật ngữ ............................................................................................. PHẦN MỞ ĐẦU ........................................................................................................1 Chƣơng 1. TỔNG QUAN VỀ CHƢƠNG TRÌNH LOGIC ...................................3 1.1. CÁC KHÁI NIỆM CƠ SỞ ..............................................................................3 1.2. CHƢƠNG TRÌNH LOGIC ..............................................................................4 1.2.1. Chƣơng trình logic xác định ..................................................................... 4 1.2.2. Chƣơng trình logic thông thƣờng ........................................................... 10 1.3 TIỂU KẾT CHƢƠNG 1 .................................................................................12 Chƣơng 2. CHƢƠNG TRÌNH LOGIC PHỎNG ĐOÁN CÓ CHỨA RÀNG BUỘC ..13 2.1. GIỚI THIỆU VỀ LẬP LUẬN PHỎNG ĐOÁN TRONG LẬP TRÌNH LOGIC ..................................................................................................................13 2.2. CHƢƠNG TRÌNH LOGIC PHỎNG ĐOÁN VÀ CÂU TRẢ LỜI PHỎNG ĐOÁN ...................................................................................................................14 2.2.1. Chƣơng trình logic phỏng đoán .............................................................. 14 2.2.2. Câu trả lời phỏng đoán ........................................................................... 15 2.3. CHƢƠNG TRÌNH LOGIC PHỎNG ĐOÁN CÓ CHỨA RÀNG BUỘC ....17 2.3.1. Chƣơng trình logic có chứa ràng buộc ................................................... 17 2.3.2. Chƣơng trình logic phỏng đoán có chứa ràng buộc ............................... 18 2.4. TIỂU KẾT CHƢƠNG 2 ................................................................................20 Chƣơng 3. THỦ TỤC CHỨNG MINH CIFF ĐỐI VỚI CHƢƠNG TRÌNH LOGIC PHỎNG ĐOÁN CÓ CHỨA RÀNG BUỘC ...........................................21 3.1. TÍNH ĐẦY ĐỦ CỦA CHƢƠNG TRÌNH LOGIC PHỎNG ĐOÁN CÓ CHỨA RÀNG BUỘC ..........................................................................................21 3.2. THỦ TỤC CHỨNG MINH CIFF..................................................................23 3.2.1. Một số định nghĩa ................................................................................... 23 3.2.2. Các quy tắc CIFF .................................................................................... 24 3.2.3. Dẫn xuất CIFF và trích xuất câu trả lời .................................................. 32 3.3. CÀI ĐẶT VÀ THỰC THI MỘT SỐ BÀI TOÁN BẰNG HỆ THỐNG CIFF TRÊN SWI-PROLOG ..........................................................................................38 3.3.1. Giới thiệu SWI-Prolog ........................................................................... 38 3.3.2. Thực thi truy vấn trong SWI-Prolog ...................................................... 40 3.3.3. Giới thiệu hệ thống CIFF ....................................................................... 40 3.3.4. Cài đặt và thực thi các bài toán minh họa .............................................. 41 3.4. TIỂU KẾT CHƢƠNG 3 ................................................................................49 KẾT LUẬN ..............................................................................................................50 TÀI LI U THAM KHẢO ......................................................................................51 DANH MỤC CÁC HÌNH Trang Hình 3.1. Cửa sổ làm việc của SWI-Prolog. ............................................................ 39 Hình 3.2. Kết quả thực thi bài toán 1 bằng hệ thống CIFF. .....................................42 Hình 3.3. Kết quả thực thi bài toán 2 bằng hệ thống CIFF. .....................................45 Hình 3.4. Kết quả thực thi bài toán 3 bằng hệ thống CIFF. .....................................47 Hình 3.5. Kết quả thực thi bài toán 4 bằng hệ thống CIFF. .....................................49 DANH MỤC CÁC CHỮ VIẾT TẮT ALP Abductive Logic Programming ALPC Abductive Logic Programming with Constraints CLP Constraint Logic Programming DANH MỤC CÁC THUẬT NGỮ Câu trả lời phỏng đoán Abductive answer Câu trả lời phỏng đoán với ràng buộc Abductive answer with constrains Chƣơng trình logic Logic program Chƣơng trình logic nền Ground logic program Cơ sở Herbrand Herbrand base Lập trình logic Logic programming Literal âm Negative literal Mô hình bền vững Stable model Mô hình nhỏ nhất Least model Ngữ nghĩa mô hình bền vững Stable model semantics Nguyên tố Atom Quy tắc Rule Vị từ Predicate Vũ trụ Herbrand Herbrand universe PHẦN MỞ ĐẦU Trong suốt những thập kỷ qua, đã có nhiều nghiên cứu về các vấn đề lập luận suy diễn đối với chƣơng trình logic. Lập trình logic chủ yếu dựa trên ý tƣởng lập trình khai báo, ở đó các chƣơng trình logic không đƣợc tạo ra từ các câu lệnh cũng nhƣ từ các hàm mà đƣợc tạo ra chủ yếu dựa trên tập các vị từ. Tuy nhiên, hiện nay lập trình logic đã bộc lộ những hạn chế nhất định và không thể giải quyết đối với các bài toán phức tạp trong thực tế. Đã có nhiều công trình nghiên cứu nhằm mở rộng lập trình logic, trong số đó – Lập trình logic phỏng đoán (ALP - Abductive Logic Programming) là một hƣớng nghiên cứu đƣợc nhiều nhà khoa học quan tâm. ALP đƣợc bắt nguồn từ sự phỏng đoán, phỏng đoán là một hình thức suy luận để giải thích cho các quan sát, xuất phát từ một cơ sở tri thức T và một quan sát Q để tìm các giải thích có thể cho Q dựa theo một tập vị từ đặc biệt đƣợc gọi là các vị từ phỏng đoán (abducible predicate). Trong ALP hình thành nên một cú pháp mới của chƣơng trình logic, đƣợc định nghĩa bởi một bộ ba P, A, IC , trong đó P là một chƣơng trình logic thông thƣờng, A là một tập hợp các vị từ và đƣợc gọi là các vị từ phỏng đoán, và IC là một tập các ràng buộc toàn vẹn. ALP là một khuôn khổ biểu diễn tri thức cấp cao, cho phép giải quyết các bài toán dựa trên lập luận phỏng đoán. Hiện nay, xuất phát từ các nhu cầu của thực tiễn, ALP đã đƣợc nghiên cứu mở rộng để cho phép các mệnh đề của chƣơng trình logic trong ALP có thể có các ràng buộc (ALPC – Abductive Logic Programming with Constraints). ALPC thƣờng đƣợc ứng dụng để giải quyết các bài toán trong Chuẩn đoán, Lập kế hoạch, Xử lý ngôn ngữ tự nhiên, Học máy,… Luận văn nghiên cứu về lập luận suy diễn đối với chƣơng trình logic phỏng đoán có chứa ràng buộc. Những nội dung nghiên cứu của luận văn có ý nghĩa khoa học về mặt lý thuyết cũng nhƣ ứng dụng trong thực tiễn. Cấu trúc luận văn gồm phần mở đầu, ba chƣơng nội dung, phần kết luận và tài liệu tham khảo. 1 Chƣơng 1 trình bày về ngôn ngữ logic bậc nhất, cú pháp và ngữ nghĩa của chƣơng trình logic. Trên cơ sở đó trình bày lập luận suy diễn trong lập trình logic. Chƣơng 2 trình bày về cú pháp, câu trả lời phỏng đoán của chƣơng trình logic phỏng đoán và chƣơng trình logic phỏng đoán có chứa ràng buộc. Chƣơng 3 trình bày thủ tục chứng minh CIFF – là một phƣơng pháp để trả lời câu truy vấn đối với các chƣơng trình logic phỏng đoán có chứa ràng buộc. Chƣơng 3 cũng trình bày tổng quan về hệ thống CIFF, tiến hành việc cài đặt một số bài toán minh họa bằng hệ thống CIFF và thực thi bằng phần mềm SWI-Prolog. Phần kết luận nêu những kết quả đã đạt đƣợc và hƣớng phát triển của luận văn. Do thời gian có hạn và bản thân chỉ mới bƣớc đầu nghiên cứu về lĩnh vực này nên không thể tránh khỏi những thiếu sót, kính mong sự giúp đỡ và góp ý thêm của quý Thầy, Cô và các bạn. 2 Chƣơng 1. TỔNG QUAN VỀ CHƢƠNG TRÌNH LOGIC Chƣơng 1 trình bày về cú pháp và ngữ nghĩa của chƣơng trình logic. Đây là những kiến thức cơ sở làm tiền đề cho các nghiên cứu ở các chƣơng tiếp theo. 1.1. CÁC KHÁI NI M CƠ SỞ Phần này trình bày một số khái niệm thƣờng đƣợc dùng trong logic bậc nhất, khái niệm đầu tiên là bộ ký tự, đƣợc định nghĩa nhƣ sau: Định nghĩa 1.1 (Bộ ký tự) Bộ ký tự bao gồm 8 lớp ký hiệu sau: 1. Hằng, thƣờng ký hiệu là các chữ cái thƣờng a, b, c,... 2. Biến, thƣờng ký hiệu bởi các chữ cái in hoa X, Y, Z,... 3. Các ký hiệu hàm, thƣờng ký hiệu bởi f, g, h,... 4. Các ký hiệu vị từ, thƣờng ký hiệu bởi p, q, r,... 5. Các hằng vị từ: true, false. 6. Các ký hiệu kết nối:  (phủ định), ∨ (tuyển), ∧ (hội),  (suy ra),  (tƣơng đƣơng). 7. Các ký hiệu lƣợng từ:  (với mọi),  (tồn tại). 8. Dấu ngoặc đơn trái (, dấu ngoặc đơn phải ), dấu phẩy ,. Mỗi ký hiệu hàm hoặc ký hiệu vị từ thƣờng có kèm theo một số tự nhiên để chỉ số các đối số tham gia cùng với ký hiệu hàm hoặc ký hiệu vị từ đó, gọi là ngôi của chúng. Định nghĩa 1.2 (Hạng thức) Gọi A là bộ ký tự. Hạng thức đƣợc định nghĩa đệ qui nhƣ sau: (i) Mỗi hằng c trong A là một hạng thức, (ii) Mỗi biến V trong A là một hạng thức, (iii) Nếu f là ký hiệu hàm n ngôi trong A và t1,..,tn là các hạng thức thì f(t1,...,tn) là một hạng thức, 3 (iv) Hạng thức chỉ đƣợc sinh ra bởi các quy tắc trên. Một hằng đƣợc xem là ký hiệu hàm 0-ngôi. Hạng thức nền là hạng thức không chứa biến. Định nghĩa 1.3 (Nguyên tố) Một nguyên tố có dạng p(t1,…,tn), trong đó p là ký hiệu vị từ n-ngôi (ký hiệu p/n) và các đối t1,...,tn là các hạng thức. Nguyên tố nền là nguyên tố không chứa biến. Ví dụ 1.1 Xét nguyên tố father(Hung,Dung), trong đó vị từ father là vị từ 2-ngôi chỉ mối quan hệ bố con, hạng thức Hung, Dung là các hằng. Nguyên tố này có ý nghĩa là Hoa là bố của Dung và là nguyên tố nền. Định nghĩa 1.4 (Literal) Literal là một nguyên tố (gọi là literal dương) hoặc phủ định của nguyên tố (literal âm). Với p là một nguyên tố, literal âm của p đƣợc ký hiệu  p. Vídụ 1.2 Xét nguyên tố father(Hung,Dung) ở ví dụ 1.1, father(Hung,Dung) là literal dƣơng và father(Hung,Dung) là literal âm. 1.2. CHƢƠNG TRÌNH LOGIC Trong phần này sẽ xem xét cú pháp và ngữ nghĩa của hai lớp chƣơng trình logic: chƣơng trình logic xác định và chƣơng trình logic thông thƣờng. 1.2.1. Chƣơng trình logic xác định 1.2.1.1. Cú pháp Định nghĩa 1.5 (Mệnh đề xác định) Mệnh đề xác định là công thức có dạng: X1...Xk ( p  q1,..., qn ) (1) trong đó n  0, p, qi là các nguyên tố, p đƣợc gọi là đầu và q1, ..., qn đƣợc gọi là thân của mệnh đề, dấu phẩy ký hiệu thay cho phép hội (), X1... Xk là các biến xuất hiện trong p, q1, ..., qn. Ta thƣờng viết mệnh đề (1) dƣới dạng: p  q1,..., qn 4 (2) Trong mệnh đề (1), nếu n = 0 thì đƣợc gọi là mệnh đề đơn vị, nghĩa là mệnh đề có dạng: p  , đó là mệnh đề với thân rỗng, ký hiệu  có thể bỏ qua. Ngữ nghĩa của mệnh đề đơn vị là với mọi phép thay thế các biến của p bởi các hằng thì p luôn luôn đúng. Định nghĩa 1.6 (Chƣơng trình logic xác định) Chương trình logic xác định là một tập hữu hạn khác rỗng các mệnh đề xác định. Ví dụ 1.5 Cho chƣơng trình logic xác định P gồm các mệnh đề: r1 : even(0)  r2 : even(s(s(X)))  even(X) Trong chƣơng trình này thì s là một hàm 1-ngôi, đƣợc xác định bởi s(X) = X +1 với X  N, nguyên tố even(X) để chỉ X là một số chẵn. Mệnh đề đơn vị r1 even(0) có ý nghĩa là 0 một số chẵn và r2 là mệnh đề với ý nghĩa là nếu X là số chẵn thì s(s(X)) cũng là số chẵn. Định nghĩa 1.7 (Vũ trụ/Cơ sở Herbrand) Cho P là chƣơng trình logic xác định.  Vũ trụ Herbrand của P, ký hiệu UP, là tập các hạng thức nền đƣợc xây dựng từ các hằng và các ký hiệu hàm trong P.  Cơ sở Herbrand của P, ký hiệu BP, là tập các nguyên tố nền đƣợc xây dựng từ các ký hiệu vị từ trong P có đối là các hạng thức nền lấy từ vũ trụ Herbrand UP. Vũ trụ Herbrand, cơ sở Herbrand của chƣơng trình logic xác định P luôn luôn là những tập vô hạn nếu P có chứa ký hiệu hàm. Ví dụ 1.6 Xét chƣơng trình logic xác định P ở ví dụ 1.5: Vũ trụ Herbrand của P là: UP = {0, s(0), s(s(0)), s(s(s(0))),...} Cơ sở Herbrand của P là: BP = {even(0), even(s(s(0)), even(s(s(s(0))),...} Trong trƣờng hợp chƣơng trình logic xác định không chứa ký hiệu hàm thì 5 vũ trụ Herbrand, cơ sở Herbrand đều là những tập hữu hạn. 1.2.1.2. Ngữ nghĩa chương trình logic xác định Định nghĩa 1.8 (Thể hiện Herbrand, mô hình Herbrand) Cho P là chƣơng trình logic xác định.  Một thể hiện Herbrand của P là một tập con tùy ý của cơ sở Herbrand BP của P.  Một mô hình Herbrand của P là một thể hiện Herbrand I của P sao cho mọi mệnh đề của P đều đúng trong thể hiện I.  Mô hình Herbrand của P đƣợc gọi là mô hình nhỏ nhất nếu nó đƣợc bao hàm trong mọi mô hình của P. Ví dụ 1.8 Xét trở lại chƣơng trình logic xác định P ở ví dụ 1.5: r1 : even(0)  r2 : even(s(s(X)))  even(X) Xét các thể hiện Herbrand: I1 = {even(0)} I2 = {even(0), even(s(0))} I3 = {even(sn(0)) | n  {0, 2, 4,…}} I 4 = BP Thể hiện I1 không phải là mô hình của P vì mặc dù I1 là mô hình của mệnh đề even(0) nhƣng I1 không phải là mô hình của mệnh đề r2 vì tồn tại mệnh đề nền even(s(s(0)))  even(0) của r2 mà I1 không phải là mô hình của mệnh đề nền này. Tƣơng tự, I2 cũng không phải là mô hình của P vì mệnh đề tồn tại mệnh đề nền: even(s(s(s(0))))  even(s(0)) của r2 mà I2 không phải là mô hình của nó. Tuy nhiên, I3 là mô hình của P. Ta có I3 là mô hình của r1. I3 cũng là mô hình của r2. Thật vậy, xét mệnh đề: 6 even(s(s(t))))  even(t) là một hiện hành nền nào đó của mệnh đề r2, trong đó tUP. Rõ ràng mệnh đề even(s(s(t)))  even(t) đúng vì even(t) và even(s(s(t)))) đều thuộc I3. Vậy I3 là mô hình của P. Ta cũng có ngay I4 là mô hình của P. Ví dụ1.9 Cho chƣơng trình logic xác định P gồm các mệnh đề: r1 : happy(X)  parent(X,Y) , newborn(Y) r2 : parent(X,Y)  father(X,Y) r3 : parent(X,Y)  mother(X,Y) r4 : father(Khoa,Mai)  r5 : newborn(Mai)  Xét một số thể hiện Herbrand của P: I1 ={newborn(Khoa), happy(Khoa)} I2= {newborn(Mai), happy(Mai), parent(Khoa,Mai)} I3= {newborn(Mai), father(Khoa,Mai), mother(Khoa,Mai), parent(Khoa,Mai), happy(Khoa)} I1 và I2 đều không phải là mô hình của P vì tồn tại mệnh đề father(Khoa,Mai) của r4 không đúng trong I1 và I2. Tuy nhiên, I3 là mô hình của P vì mọi mệnh đề của P đều đúng trong I3. Định nghĩa 1.9 (Ngữ nghĩa chƣơng trình logic xác định) Cho P là chƣơng trình logic xác định, ngữ nghĩa của P là mô hình nhỏ nhất của P, ký hiệu MP. Mô hình nhỏ nhất MP có thể xây dựng bằng cách dùng toán tử hệ quả trực tiếp. Ta có định nghĩa sau: Định nghĩa 1.10 (Toán tử hệ quả trực tiếp) Cho P là chƣơng trình logic xác định. Ánh xạ TP: 2 BP 2 BP đƣợc xác định nhƣ sau: Với mỗi I  2 7 BP , TP(I) = { A  BP |  mệnh đề nền A  A1,…, An của P và {A1,…, An}  I } trong đó 2 BP là ký hiệu tập các tập con của cơ sở Herbrand BP. TP đƣợc gọi là toán tử hệ quả trực tiếp trên 2 BP . Định lý 1.1 [2] Toán tử TP đơn điệu theo quan hệ bao hàm và có điểm bất động nhỏ nhất. Hơn nữa, điểm bất động nhỏ nhất đó cũng chính là mô hình nhỏ nhất của chƣơng trình logic xác định P. Định lý 1.2 [2] Cho P là chƣơng trình logic xác định. Mô hình nhỏ nhất của P là giới hạn của dãy TPn, n  N, ký hiệu TP, trong đó: TP 0 = , TP (i + 1) = TP(TPi) Ví dụ 1.10 Xét chƣơng trình logic P ở Ví dụ 1.5: r1 : even(0)  r2 : even(s(s(X)))  even(X) Áp dụng Định lý 1.2 ở trên ta tính đƣợc: Ta có: TP 0 =  TP 1 = {even(0)} TP 2 = {even((s(s(0))))} … TP = {even(sn(0)) | n {0, 2, 4,…}} Ví dụ 1.11 Xét chƣơng trình logic sau: path(X,Y)  edge(X,Y) path(X,Y)  edge(X,Z) , path(Z,Y) edge(1,2), edge(2,3), edge(3,4), edge(4,5) Mô hình nhỏ nhất (MP) của P đƣợc tìm qua các bƣớc lặp sau: 8 I1 =  I2 = Tp(I1) = {edge(1,2), edge(2,3), edge(3,4), edge(4,5)} I3 = Tp(I2) = I2 {path(1,2), path(2,3), path(3,4), path(4,5)} I4 = Tp(I3) = I3 {path(1,3), path(2,4), path(3,5)} I5 = Tp(I4) = I4 {path(1,4), path(2,5)} I6 = Tp (I5) = I5 {path(1,5)} I7 =Tp(I6) =I6   = I6 Vậy mô hình nhỏ nhất của P chính là MP = . 1.2.1.3. Lập luận suy diễn trong chương trình logic xác định Vấn đề ta quan tâm là làm thế nào xác định đƣợc các nguyên tố nền là hệ quả logic (nghĩa là đƣợc suy diễn logic) từ các quy tắc của chƣơng trình logic xác định đã cho. Điều này đƣợc thể hiện qua kết quả sau: Định lý 1.3 [2] Mô hình nhỏ nhất MP của chƣơng trình logic xác định P là tập các nguyên tố nền mà là hệ quả logic của P. Nghĩa là: MP = {A  BP | P A} Đối với chƣơng trình logic xác định, ta thƣờng dùng giả thiết thế giới đóng (CWA – Closed World Assumption) sau đây: nếu một nguyên tố nền A không thể suy diễn logic từ chương trình logic xác định P thì A là đúng. Vì vậy, từ định lý trên ta có thể kết luận về giá trị chân lý của nguyên tố nền: nếu A  MP thì A đƣợc xem là đúng, ngoài ra A là sai. Điều này có thể biểu diễn bởi quy tắc suy diễn sau: P A A (CWA) Ví dụ 1.12 Xét chƣơng trình logic ở ví dụ 1.11, tất cả các nguyên tố nền không thuộc mô hình nhỏ nhất MP = {edge(1,2), edge(2,3), edge(3,4), edge(4,5), path(1,2), path(2,3), path(3,4), path(4,5), path(1,3), path(2,4), path(3,5), path(1,4), path(2,5)} đều đƣợc xem là sai, chẳng hạn path(2,1) là sai. 9 1.2.2. Chƣơng trình logic thông thƣờng Các chƣơng trình logic xác định biểu diễn tri thức dƣơng, các mệnh đề trong chƣơng trình mô tả các đối tƣợng xác định và mối quan hệ giữa chúng. Các quan hệ này đƣợc thể hiện rõ trong mô hình nhỏ nhất - chứa các nguyên tố nền là hệ quả logic của chƣơng trình. Đối với chƣơng trình logic thông thƣờng, khi các mệnh đề có chứa phủ định ở thân thì ngữ nghĩa của nó trở nên phức tạp hơn nhiều. Lúc này chƣơng trình có thể không có mô hình nhỏ nhất nhƣng tồn tại nhiều mô hình cực tiểu. Ví dụ 1.13 Chẳng hạn, xét chƣơng trình logic P gồm các mệnh đề sau: p(X)  r(X) , q(X) q(X)  r(X) , p(X) r(1)  Chƣơng trình này chỉ có hai mô hình cực tiểu là S1 = {q(1), r(1)}, S2 = {p(1), r(1)} và không có mô hình nhỏ nhất vì S1 ⊄ S2 và S2 ⊄ S1. 1.2.2.1. Cú pháp và ngữ nghĩa Định nghĩa 1.11 (Chƣơng trình logic thông thƣờng) Chương trình logic thông thường là một tập hữu hạn khác rỗng các mệnh đề có dạng: p  q1, ..., qn (1) trong đó n  0, p là nguyên tố, qi là các literal. Từ đây về sau ta gọi chƣơng trình logic thông thƣờng là chƣơng trình logic. Để giải quyết vấn đề ngữ nghĩa của chƣơng trình logic thông thƣờng (có chứa phủ định), đã có nhiều tiếp cận khác nhau, trong đó thƣờng sử dụng tiếp cận ngữ nghĩa mô hình bền vững [3]. Việc xác định mô hình bền vững sẽ đƣợc thực hiện nhờ vào một phép biến đổi, đƣợc gọi là phép biến đổi Gelfond – Lifschitz. Ta có định nghĩa sau: Định nghĩa 1.12 (Phép biến đổi Gelfond - Lifschitz) [3] Gọi ground(P) là chƣơng trình nhận đƣợc từ chƣơng trình logic P bằng cách thay thế các biến trong mọi mệnh đề của P bởi các hằng trong P. Đối với mọi thể hiện M của ground(P), ký hiệu PM là chƣơng trình nhận đƣợc từ ground(P) bằng cách loại bỏ: 10 1. Các quy tắc có literal âm B trong thân của nó, với B  M. 2. Tất cả literal âm trong thân của các quy tắc còn lại. Rõ ràng PM là chƣơng trình không có phủ định, nó là chƣơng trình logic xác định, vì vậy PM có mô hình nhỏ nhất. Ví dụ 1.14 Cho P là chƣơng trình logic: a  b b  a c  a , b Bây giờ, P có hai mô hình bền vững: M1 = {a, c} và M2 = {b}. Thu gọn P M1 là tập các quy tắc: a  c a và mô hình nhỏ nhất của nó chính là {a,c}. Thu gọn P M 2 là tập quy tắc: b  và mô hình nhỏ nhất của nó chính là {b}. Tập M3 = {a, b, c} là một mô hình của P theo nghĩa thông thƣờng, nhƣng nó không bền vững vì mô hình nhỏ nhất của P M 3 là tập rỗng. Định nghĩa 1.13 (Mô hình bền vững) Tập M các nguyên tố đƣợc gọi là mô hình bền vững của chƣơng trình logic P nếu M là mô hình nhỏ nhất của PM. Định lý 1.4 [3] Cho P là chƣơng trình logic. Mọi mô hình bền vững của P đều là mô hình cực tiểu của P. Các mô hình bền vững là sự tổng quát hóa ngữ nghĩa của chƣơng trình logic xác định, điều này đƣợc thể hiện bởi kết quả sau: 11 Định lý 1.5 [3] Đối với chƣơng trình logic xác định thì mô hình bền vững chính là mô hình nhỏ nhất của nó. 1.2.2.2. Lập luận suy diễn trong chương trình logic thông thường Bởi vì một chƣơng trình logic có thể có một hoặc nhiều hoặc không có mô hình bền vững. Vấn đề đặt ra là cách thức suy luận từ P sẽ đƣợc xác định nhƣ thế nào. Đối với một mô hình bền vững cụ thể, một nguyên tố nền a đƣợc xem là đúng nếu a  M và sai nếu a  M. Điều này thƣờng đƣợc mở rộng để suy luận từ tất cả mô hình bền vững của P theo hai dạng đối ngẫu nhau sau đây:  Lập luận bất chấp (Brave Reasoning): Một nguyên tố nền a là hệ quả bất chấp (brave consequence) của P, ký hiệu ⊨b nếu a thuộc vào một mô hình bền vững M nào đó của P.  Lập luận thận trọng (Cautious Reasoning): Một nguyên tố nền a là hệ quả thận trọng (brave consequence) của P, ký hiệu ⊨c nếu a thuộc mọi mô hình bền vững M của P. Ví dụ 1.16 Xem chƣơng trình logic P: p(a)  r(X)  p(X), q(X) P có 2 mô hình cực tiểu là M1 = {p(a), r(a)} và M2 = {p(a), q(a)} và chỉ có M1 là mô hình bền vững của P. Lúc đó P ⊨b r(a) và P ⊨c r(a) vì r(a) đúng trong mọi mô hình bền vững. Tuy nhiên với P’ = P  {q(a)} thì cả hai P’ ⊨b r(a) và P’ ⊨c r(a) đều không thỏa mãn vì r(a) là sai trong mô hình bền vững duy nhất của {p(a), q(a)} của P’. 1.3. TIỂU KẾT CHƢƠNG 1 Chƣơng một đã trình bày tổng quan về chƣơng trình logic gồm cú pháp và ngữ nghĩa của chƣơng trình logic. Các ví dụ minh họa chi tiết nhằm làm rõ các khái niệm. Trong chƣơng hai sẽ trình bày chi tiết về cú pháp và câu trả lời phỏng đoán của chƣơng trình logic phỏng đoán có chứa ràng buộc. 12