Tài liệu Tích hợp tri thức sử dụng các kỹ thuật tranh cãi

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ NGUYỄN TRẦN VÂN TÍCH HỢP TRI THỨC SỬ DỤNG CÁC KỸ THUẬT TRANH CÃI Ngành: Công nghệ thông tin Chuyên ngành: Kỹ thuật phần mềm Mã số: 62.48.01.03 LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN Người hướng dẫn khoa học: TS. Trần Trọng Hiếu Hà Nội - 2016 Mục lục Mục lục Lời cám ơn iii Lời cam đoan iv Danh mục các ký hiệu, các chữ viết tắt v Danh sách hình vẽ vii Danh sách bảng viii Mở đầu ix 1 Tổng quan về logic và tích hợp tri thức 1.1 Tổng quan về logic . . . . . . . . . . . 1.1.1 Logic cổ điển . . . . . . . . . . 1.1.2 Logic khả năng . . . . . . . . . 1.2 Tổng quan về tích hợp tri thức . . . . . 1.2.1 Biểu diễn tri thức . . . . . . . . 1.2.2 Duyệt tri thức . . . . . . . . . . 1.2.3 Tích hợp tri thức . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 . 1 . 1 . 2 . 4 . 4 . 6 . 14 2 Mô hình tranh cãi 2.1 Sự chấp nhận của tranh cãi . . . . . . . . . . . . . . . . . 2.1.1 Mô hình tranh cãi . . . . . . . . . . . . . . . . . . . 2.1.2 Ngữ nghĩa cố định và ngữ nghĩa cơ sở (hoài nghi) . 2.1.3 Điều kiện cho sự trùng giữa ngữ nghĩa khác nhau . 2.2 Tranh cãi, trò chơi n-người và bài toán hôn nhân bền vững 2.2.1 Tranh cãi trong trò chơi n-người . . . . . . . . . . . 2.2.2 Tranh cãi và bài toán hôn nhân bền vững . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 24 24 28 29 32 32 33 3 Tích hợp tri thức có ưu tiên trong mô hình logic khả năng 35 3.1 Tích hợp tri thức bằng tranh cãi trong logic khả năng . . . . . . . . . . 36 3.2 Định đề và một số tính chất . . . . . . . . . . . . . . . . . . . . . . . . 41 4 Thực nghiệm và đánh giá 43 4.1 Môi trường thực nghiệm . . . . . . . . . . . . . . . . . . . . . . . . . . 43 4.2 Quá trình thực nghiệm . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 i 4.2.1 4.2.2 4.2.3 4.2.4 4.2.5 Giới thiệu về chương trình . . . . . . . . . . . . . . . . . . . . Tập dữ liệu thực nghiệm . . . . . . . . . . . . . . . . . . . . . Kết quả thực nghiệm thu được của tập dữ liệu thứ nhất . . . Kết quả thực nghiệm thu được của tập dữ liệu thứ hai . . . . Đánh giá kết quả thực nghiệm và hướng nghiên cứu tiếp theo . . . . . 43 45 45 48 48 Kết luận 50 Tài liệu tham khảo 51 ii LỜI CÁM ƠN Lời đầu tiên, tôi xin gửi lời cám ơn sâu sắc nhất đến TS. Trần Trọng Hiếu đã tận tình hướng dẫn tôi trong suốt quá trình thực hiện Luận văn. Tôi cũng xin gửi lời cám ơn và lòng biết ơn sâu sắc tới PGS.TS Hà Quang Thuỵ cùng anh chị em phòng thí nghiệm DS&KTLab đã nhiệt tình động viên và giúp đỡ tôi hoàn thành Luận văn. Tôi chân thành cảm ơn các thầy, cô đã tạo điều kiện thuận lợi cho tôi được học tập và nghiên cứu tại Trường Đại học Công Nghệ. Tôi xin cảm ơn các bạn trong lớp cao học K20 và các đồng nghiệp tại công ty AI Việt Nam đã ủng hộ, khuyến khích và tạo điều kiện cho tôi trong suốt quá trình học tập tại trường. Cuối cùng nhưng không kém phần quan trọng, tôi muốn gửi lời cảm ơn vô hạn tới gia đình, bạn bè, những người thân yêu luôn bên cạnh, động viên và giúp đỡ tôi không chỉ trong quá trình thực hiện Luận văn mà còn trong suốt cuộc đời này. Hà Nội, ngày 19 tháng 9 năm 2016 Học viên Nguyễn Trần Vân iii LỜI CAM ĐOAN Tôi xin cam đoan luận văn “Tích hợp tri thức sử dụng các kỹ thuật tranh cãi" là công trình nghiên cứu của riêng tôi. Các số liệu, kết quả được trình bày trong luận văn là hoàn toàn trung thực. Tôi đã trích dẫn đầy đủ các tài liệu tham khảo, công trình nghiên cứu liên quan. Ngoại trừ các tài liệu tham khảo này, luận văn hoàn toàn là công việc của riêng tôi. Luận văn được hoàn thành trong thời gian tôi là học viên tại Khoa Công nghệ Thông tin, Trường Đại học Công nghệ, Đại học Quốc gia Hà Nội. Hà Nội, ngày 19 tháng 9 năm 2016 Học viên Nguyễn Trần Vân iv DANH MỤC CÁC CHỮ VIẾT TẮT ANO BMA CLO CON COO IC IDN MAJ PKB SMP SYM UNA : : : : : : : : : : : : Anonymity Belief Merging by Argumentation Closure Consistency Cooperativity Integrity Constraints Identity Majority Possibilistic Knowledge Base Stable Marriage Problem Symmetry Unanimity v DANH MỤC CÁC THUẬT NGỮ Tiếng Anh Acceptable Admissible Arbitration operator Belief base Belief contraction Belief Merging Belief profile Belief Revision Characteristic function Complete Extension Conflict-free Epistemic Entrenchment Grounded Extension Harper Identity Integrity Constraints Levi Identity Majority operator Necessity degree Possibilistic formula Possibilistic Knowledge Base Possibilistic logic Possibility degree Possibility distribution Possible world Preferred Extension Principle of minimal change Responsibility attribution Revision function Selection Function Stable Extension System of Spheres Tiếng Việt Có thể chấp nhận Bao đóng có thể chấp nhận Toán tử trọng tài Cơ sở tri thức Loại bỏ tri thức Tích hợp tri thức Hồ sơ tri thức Duyệt tri thức Hàm đặc trưng Phần mở rộng đầy đủ Không chứa các xung đột Cố thủ tri thức Phần mở rộng cơ sở Đồng nhất Harper Ràng buộc toàn vẹn Đồng nhất Levi Toán tử đa số Độ chắc chắn Công thức khả năng Cơ sở tri thức khả năng Logic khả năng Độ có thể Phân phối khả năng Thế giới có thể Phần mở rộng ưu tiên Nguyên tắc thay đổi tối thiểu Chỉ định trách nhiệm Hàm duyệt Hàm lựa chọn Phần mở rộng ổn định Hệ thống các khối cầu tri thức vi Trang 26 26 17 1 7 4 2 4 28 29 26 11 28 9 15 9 17 2 2 1 1 2 1 13 26 6 23 7 9 27 12 Danh sách hình vẽ 1.1 1.2 Một khối cầu tri thức . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 Mô hình AGM . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.1 2.2 2.3 2.4 2.5 Mô hình tranh cãi . . . . . . . . . . . . . . . . . Quan hệ tấn công trong mô hình tranh cãi . . . Mô hình tranh cãi không chứa xung đột . . . . Có thể chấp nhận trong mô hình tranh cãi . . . Bao đóng có thể chấp nhận trong mô hình tranh . . . . . . . . cãi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 25 26 26 26 4.1 4.2 4.3 4.4 4.5 4.6 4.7 Giao diện chương trình . . . . Tạo cơ sở tri thức . . . . . . . Kết quả của hàm hợp . . . . . Các lập luận . . . . . . . . . . Quan hệ Undercut . . . . . . Kết quả của toán tử BMA . . Biểu đồ thời gian thực nghiêm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 44 46 46 47 47 48 . . . . . . . . . . . . . . . . . . (đơn vii . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . vị giây) . . . . . . . . . . . . . . . . . . . . . Danh sách bảng 1.1 Toán tử tích hợp dựa vào khoảng cách thông thường . . . . . . . . . . 20 3.1 3.2 Ảnh hưởng của lập luận . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Danh sách các lập luận . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 4.1 4.2 Kết quả quá trình tích hợp . . . . . . . . . . . . . . . . . . . . . . . . . 48 Thời gian thực nghiệm chương trình (đơn vị phút) . . . . . . . . . . . . 48 viii Mở đầu Ngày nay tích hợp tri thức là một trong các vấn đề nghiên cứu với các ứng dụng quan trọng trong Khoa học máy tính. Mục tiêu chính của tích hợp tri thức là nhằm đạt được các tri thức chung từ các nguồn tri thức riêng lẻ. Vấn đề này được ứng dụng rộng rãi trong nhiều lĩnh vực của khoa học máy tính như tích hợp dữ liệu [1], khôi phục thông tin [2], gộp dữ liệu cảm biến [3], các hệ đa tác tử [4] và các hệ thống đa phương tiện (Multimedia) [5, 6]. Vấn đề tích hợp tri thức bắt đầu được quan tâm, nghiên cứu, phát triển và áp dụng cho một số lĩnh vực trong đời sống, xã hội, kinh tế, an ninh quốc phòng,. . . Một trong các ví dụ thực tế đó là hiện nay đã có một số hệ thống dự báo kinh tế của Việt Nam như hệ thống của CIA1 , hệ thống của WordBank2 . . . , mỗi hệ thống đưa ra một bộ các chỉ số phát triển của nền kinh tế nước ta. Tuy nhiên bộ Kế hoạch đầu tư không thể lấy ngay kết quả của dự báo từ một trong các hệ thống này để báo cáo lên Chính phủ hay Quốc hội được. Thay vào đó Trung tâm Thông tin và Dự báo kinh tế - xã hội quốc gia của bộ Kế hoạch và đầu tư phải tổng hợp thông tin từ các nguồn đó thành một thông tin duy nhất mà phản ánh được thực trạng kinh tế của Việt Nam rồi sau đó mới báo cáo kết quả này lên Chính phủ hay Quốc hội. Hiện nay có nhiều cách tiếp cận để tích hợp tri thức khác nhau như [7, 8]. Tuy nhiên tất cả các cách tiếp cận này đều dựa trên giả thuyết là các bên tham gia đều có tính cộng tác, tức là để các bên đạt được thỏa thuận chung khi mà mỗi bên đều có một số đòi hỏi và các đòi hỏi này mâu thuẫn nhau thì các bên cần thỏa thuận với nhau để mỗi bên hy sinh đi một số đòi hỏi của mình nhằm đạt được sự đồng thuận. Các tiếp cận này chưa phản ánh được đúng cách làm việc trong thực tế. Chẳng hạn như bên A có các đòi hỏi là hoàn toàn hợp lý và có đầy đủ bằng chứng, lập luận để bảo vệ ý kiến của mình còn bên B các đòi hỏi hoàn toàn vô lý và không có bằng chứng lập luận gì cả. Nếu theo các tiếp cận truyền thống, hai bên sẽ cùng bớt đi một số đòi hỏi nào đó của mình để đạt được một thỏa thuận chung, điều này là vô lý vì bên B sẽ được hưởng lợi mặc dù mọi đòi hỏi đều không hợp lý và bên A sẽ bị mất một phần quyền lợi chính đáng của mình. Trong luận văn này tôi đề ra một cách tiếp cận mới cho việc tích hợp tri thức nhằm khắc phục những hạn chế của các tiếp cận hiện có. Ý tưởng chính của tiếp cận này như sau: Để đạt được thỏa thuận giữa các bên, ta sẽ để cho các bên tranh cãi với nhau, tức là các bên sẽ dùng lý lẽ, lập luận để bảo vệ cho các đòi hỏi của mình đồng thời phản bác lại các đòi hỏi của đối phương, bên nào có nhiều chứng cứ, lập luận tốt hơn thì bên đó sẽ giành được nhiều lợi ích hơn. Để làm được điều này, một mô hình tích hợp cơ sở tri thức khả năng được đề xuất dựa trên một mô hình tranh cãi nổi tiếng được đề xuất bởi GS. Phạm Minh Dũng [25]. Bên cạnh đó, một tập các tiên đề cho tích hợp tri thức bằng tranh cãi cũng được giới thiệu và các tính chất logic của nó cũng được đem ra thảo luận. Một chương trình thực nghiệm tích hợp tri thức dựa trên mô hình đã đề xuất và các đánh giá về nó được tiến hành. Nội dung chính của luận văn bao gồm các phần: 1 https://www.cia.gov/library/publications/the-world-factbook/geos/vm.html. 2 http://www.worldbank.org/en/country/vietnam. ix Chương 1. Tổng quan về logic và tích hợp tri thức. Chương này trình bày các kiến thức cơ sở về logic và tích hợp tri thức bao gồm: logic cổ điển, logic khả năng, biểu diễn tri thức, duyệt tri thức và tích hợp tri thức. Chương 2. Mô hình tranh cãi. Chương này trình bày về mô hình tranh cãi của GS. Phạm Minh Dũng cùng với các ngữ nghĩa của mô hình này. Chương 3. Các mô hình tích hợp tri thức bằng tranh cãi. Chương này là nội dung chính của luận văn, trong đó trình bày cách tiếp cận để giải quyết thông tin mâu thuẫn bằng tích hợp tri thức có ưu tiên trong mô hình logic khả năng. Chương 4. Thực nghiệm và đánh giá. Trong chương này tôi tiến hành cài đặt một chương trình tích hợp tri thức như trong mô hình đề xuất và đánh giá các kết quả đạt được. Phần kết luận. Tóm lược những kết quả đã đạt được của luận văn và đưa ra định hướng nghiên cứu trong tương lai. x Chương 1 Tổng quan về logic và tích hợp tri thức 1.1 Tổng quan về logic Phương pháp tích hợp dựa trên logic đã nhận được rất nhiều sự chú ý trong nhiều lĩnh vực của khoa học máy tính, chẳng hạn như các hệ thống thông tin có cộng tác, cơ sở dữ liệu phân tán, hệ thống đa tác tử và các hệ thống chuyên gia phân tán. Trong mô hình logic, mỗi nguồn thông tin thường được coi như là một cơ sở tri thức và được biểu diễn là một tập hợp của các công thức logic. Một trong những vấn đề quan trọng của tích hợp nhiều cơ sở tri thức là đối phó với vấn đề không nhất quán. Mặc dù có thể mỗi cơ sở tri thức là nhất quán, tuy nhiên khi ta đặt chúng với nhau thì chúng có thể làm phát sinh những mâu thuẫn. Trong logic mệnh đề vấn đề không nhất quán thường được giải quyết bằng tích hợp tri thức. Phương pháp tích hợp bằng logic mệnh đề được chia làm hai loại: Tích hợp ở mức cú pháp (công thức logic) và tích hợp ở mức ngữ nghĩa (mô hình). Loại thứ nhất dựa trên việc lựa chọn một vài tập con nhất quán có được khi hợp nhất các cơ sở tri thức ban đầu còn loại thứ hai thì được xác định bởi mối quan hệ nhị phân trên tập các diễn giải. Các thông tin được ưu tiên đóng một vai trò quan trọng trong việc giải quyết vấn đề không nhất quán khi các cơ sở tri thức được tích hợp. Logic khả năng [28] đã cung cấp một mô hình linh hoạt để biểu diễn các thông tin được ưu tiên và đối phó với vấn đề không nhất quán. Ở mức độ cú pháp, thông tin được biểu diễn là một công thức logic có gắn trọng số, trọng số này được hiểu là mức độ chắc chắn của công thức này. Một cơ sở tri thức khả năng (Possibilistic Knowledge Base (PKB)) là một tập các công thức có trọng số. Ở mức độ ngữ nghĩa, nó dựa trên khái niệm của hàm phân phối khả năng, đó là một ánh xạ từ tập các diễn giải Ω vào r0, 1s để đại diện cho thông tin có sẵn. 1.1.1 Logic cổ điển Chúng ta xem xét một ngôn ngữ mệnh đề L được xác định từ một tập hữu hạn các biến mệnh đề P và các hằng số tJ, Ku. Ký hiệu W dùng để ký hiệu tập của các thế giới có thể, trong đó mỗi thế giới có thể là một hàm từ P vào tJ, Ku. Một mô hình của công thức φ là một thế giới có thể ω làm cho φ đúng, ký hiệu là ω ( φ. Với Φ là một tập của các công thức, rΦs biểu diễn tập các mô hình của Φ, nghĩa là rΦs “ tω P W |@φ P Φpω ( φqu. Chúng ta sử dụng ký hiệu rφs để thay thế cho rtφus. Chúng ta cũng sử dụng ký hiệu $ để biểu diễn cho mối quan hệ hệ quả, ví dụ 1 tφ, ψ u $ θ nghĩa là θ là hệ quả logic của {φ, ψ}. Một cơ sở tri thức (phẳng) K là tập hữu hạn các công thức, nó có thể xem là tương đương về logic với công thức φ khi nó là kết hợp của tất cả các công thức của K. Cho K1 , . . . , Kn là n cơ sở tri thức và một số trong số chúng có thể tương đương logic với nhau, một hồ sơ tri thức E của n cơ sở tri thức là một đa tập (multiset)1 E “ tK1 , . . . , Kn u. Giả sử K “ tφ1 , . . . , φm u, chúng ta ký hiệu ^K “ ^m 1 φi và i“ ^E “ ^n 1 p^Ki q. K là nhất quán khi và chỉ khi ω |ù K đối với ít nhất một thế giới i“ có thể ω. Hai cơ sở tri thức K và K 1 là tương đương, ký hiệu K ” K 1 , khi và chỉ khi 1 1 @φ P K, K 1 $ φ và ngược lại. Một tập tri thức E 1 “ tK1 , . . . , Kn u là tương đương logic với một tập tri thức E “ tK1 , . . . , Kn u, ký hiệu E ” E 1 , khi và chỉ khi tồn tại một 1 hoán vị σ trên tập {1,. . . ,n} sao cho Ki ” Kσpiq với mọi i “ 1, . . . , n. Hợp của hai tập 1 1 tri thức E và E 1 cũng là một tập tri thức E \ E 1 “ tK1 , . . . , Kn , K1 , . . . , Kn u. 1.1.2 Logic khả năng Ở mức độ ngữ nghĩa logic khả năng dựa trên khái niệm của một hàm phân phối khả năng (possibility distribution) ký hiệu bằng π, là một ánh xạ từ tập các diễn giải Ω vào r0, 1s để đại diện cho thông tin có sẵn. π pω q thể hiện mức độ phù hợp của diễn giải ω đối với những tri thức sẵn có. Quy ước, π pω q “ 1 có nghĩa là chúng ta hoàn toàn có thể cho ω là một thế giới thực (hoặc ω thỏa mãn hoàn toàn), 1 ą π pω q ą 0 có nghĩa ω chỉ thỏa mãn được một phần, trong khi π pω q “ 0 có nghĩa ω chắc chắn không phải là một thế giới thực (hoặc không đáp ứng tất cả). Từ một hàm phân bố khả năng π ta có thể xác định được độ có thể (possibility degree) của công thức φ ký hiệu là Πpφq “ maxtπ pω q|ω P Ω, ω |ù φu. Đó là mức độ đòi hỏi của công thức φ đối với với những tri thức có sẵn và độ chắc chắn (necessity degree) của mỗi công thức φ : N pφq “ 1 ´ Πp φq đối với các thông tin có sẵn, N pφq “ 1 có nghĩa φ là phần thông tin hoàn toàn chắc chắn hoặc một mục tiêu bắt buộc, trong khi N pφq “ 0 thể hiện sự không có thông tin đối với φ nhưng không có nghĩa là φ sai. Ở mức độ cú pháp, một công thức được gọi là một công thức khả năng được xác định bằng một cặp pφ, aq trong đó φ là một công thức mệnh đề và a P r0, 1s. Cặp pφ, aq có nghĩa là mức độ chắc chắn của φ ít nhất bằng apN pφq ě aq. Một PKB là một tập hữu hạn các công thức khả năng có dạng B “ tpφi , ai q : i “ 1, ..., nu. Chúng ta ký hiệu B ˚ là cơ sở tri thức phẳng liên kết với B, cụ thể là các cơ sở tri thức thu được từ B bằng cách loại bỏ đi các trọng số của công thức pB ˚ “ tφi |pφi , ai q P B uq. Một PKB B là nhất quán khi và chỉ khi B ˚ là nhất quán. Cho một PKB B, hàm phân phối khả năng của B ký hiệu là πB được xác định như sau [27]: Định nghĩa 1.1.1. @ω P Ω " πB pω q “ 1 Đa 1 nếu @pφi , ai q P B, ω |ù φi 1 ´ maxtai : pφi , ai q P B và ω * φi u ngược lại tập là tập hợp mà các phần tử của nó có thể giống nhau 2 Ví dụ 1.1.1. (Xem Ví dụ 1.2.1 tại trang 5) Cho B “ tp c; 0.9q, pa, 0.8q, p b _ a, 0.6q, pc; 0.5q, p c _ b; 0.4qu là một cơ sở tri thức. Từ Định nghĩa 1.1.1, ta có thể xác định được phân phối khả năng của B như sau: - πB pa b cq “ πB pab cq “ 0.5, - πB p ab cq “ πB p a b cq “ 0.2, - πB pabcq “ πB pa bcq “ πB p abcq “ πB p a bcq “ 0.1 Định nghĩa 1.1.2. [27] Cho B là PKB và a P r0, 1s. Chúng ta gọi a-cut (tương ứng, strict a-cut) của B, ký hiệu là Běa (tương ứng, Bąa ) là tập của các công thức mệnh đề trong B có mức độ chắc chắn ít nhất bằng a pBěa “ tφ P B ˚ |pφ, bq P B, b ě auq (tương ứng, lớn hơn a pBąa “ tφ P B ˚ |pφ, bq P B, b ą auq). Định nghĩa 1.1.3. [27] Cho B1 và B2 là hai PKB. B1 và B2 được gọi là tương đương ký hiệu là B1 ” B2 nếu πB1 “ πB2 . Sự tương đương của hai PKB cũng có thể xác định như sau: B1 ” B2 nếu pB1 qěa ” pB2 qěa . Định nghĩa 1.1.4. [27] Độ không nhất quán của PKB B được xác định như sau: IncpB q “ maxtai : Běai là không nhất quánu Độ không nhất quán của B là trọng số lớn nhất ai sao cho ai ´ cut của B là không nhất quán. Với IncpB q “ 0 thì B là nhất quán Định nghĩa 1.1.5. [27] Cho pφ, aq là một công thức trong B. pφ, aq được gọi là ngưỡng trong B nếu: pB ´ pφ, aqqěa $ φ Vàpφ, aq được gọi là ngưỡng chặt trong B nếu Bąa $ φ. Công thức ngưỡng trong một vài trường hợp cần thiết được chỉ ra trong các bổ đề sau: Bổ đề 1.1.2. Cho pφ, aq là một công thức ngưỡng trong B. Thì B và B 1 “ B ´ pφ, aq là tương đương. Định nghĩa 1.1.6. [27] Cho B là một PKB. Công thức φ được gọi là kết luận hợp lý của B nếu: BąIncpB q $ φ Định nghĩa 1.1.7. [27] Cho B là một PKB. Công thức pφ, aq là một kết luận khả năng của B, ký hiệu B $π pφ, aq, nếu: - BąIncpB q $ φ - a ą IncpB q và @b ą a, Bąb & φ Suy luận khả năng yêu cầu trọng số của công thức mệnh đề phải lớn hơn độ không nhất quán của B bởi vì với mỗi công thức mệnh đề pφ, aq. Nếu a ď IncpB q thì Běa $ φ. Nghĩa là pφ, aq có thể được suy ra từ B. 3 Với mỗi PKB B không nhất quán, các công thức có mức độ chắc chắn mà không lớn hơn IncpB q thì sẽ không được sử dụng trong suy diễn. Tiếp tục Ví dụ 1.1.1, rõ ràng B tương đương với B 1 “ tpa, 0.8q, p c; 0.7q, p b _ a, 0.6q, pc; 0.5qu bởi vì IncpB q “ 0.5 do đó p c _ b; 0.4q không được sử dụng trong suy luận khả năng. Ta có ngưỡng pB q “ t b _ a, c _ bu, kết luận hợp lý pB q = tpaq, p cq, p b _ aq, p c _ bqu và kết luận khả năng pB q = tp b _ a, 0.6qu. 1.2 1.2.1 Tổng quan về tích hợp tri thức Biểu diễn tri thức Ngày nay việc giải quyết sự không nhất quán là một trong các lĩnh vực nghiên cứu chính trong trí tuệ nhân tạo. Không nhất quán thể hiện sự thiếu (hoặc thừa) thông tin cho quá trình suy luận. Do đó, việc giải quyết sự không nhất quán của tri thức là một nhiệm vụ quan trọng trong việc quản lý tri thức. Sự không nhất quán thường xảy ra do các thông tin thường đến từ các nguồn khác nhau và từ đó nảy sinh sự mâu thuẫn. Tích hợp tri thức là một trong những cách phổ biến nhất để giải quyết mâu thuẫn. Tuy nhiên, tích hợp tri thức là một công việc khó khăn bởi vì việc xác định sự không nhất quán của tri thức không dễ dàng, do đó việc giải quyết các mâu thuẫn cũng là một vấn đề vô cùng phức tạp. Tích hợp tri thức là một khái niệm chung. Trong các vấn đề kinh tế - xã hội, tích hợp tri thức liên quan đến vấn đề nghiên cứu của các lĩnh vực: kinh tế, chính trị, văn hóa, giáo dục... Trong trí tuệ nhân tạo, khái niệm về tri thức đôi khi được hiểu với khái niệm về niềm tin và tích hợp tri thức được hiểu là quá trình duyệt tri thức hay tích hợp niềm tin [11]. Duyệt tri thức (Mục 1.2.2) nghiên cứu về quá trình thay đổi tri thức: khi một đối tượng phải đối mặt với thông tin mới mà thông tin này lại mâu thuẫn với tri thức hiện tại của nó, đối tượng này sẽ phải loại bỏ một số tri thức cũ để có thể phù hợp với thông tin mới. Mối quan tâm chính ở đây là làm thế nào để đưa ra quyết định hợp lý hay công bằng khi loại bỏ những tri thức cũ. Có rất nhiều công trình nghiên cứu về vấn đề này, trong đó có [11, 12]. Tích hợp tri thức (Mục 1.2.3) nghiên cứu phương pháp để tổng hợp các cơ sở tri thức của các đối tượng thành một tri thức chung [13, 14]. Duyệt tri thức có thể xem như là một trường hợp đặc biệt của tích hợp tri thức bởi vì trong quá trình duyệt tri thức, thông tin mới có được luôn được coi là tin cậy hơn so với thông tin ban đầu. Trong trí tuệ nhân tạo, để khắc phục vấn đề mâu thuẫn đến từ nhiều nguồn khác nhau. Hai cách tiếp cận chính để đối phó với các thông tin mâu thuẫn đã được phân biệt: - Cách tiếp cận thứ nhất bao gồm việc tích hợp các thông tin và xây dựng một tập thông tin nhất quán có thể biểu diễn cho kết quả của việc tích hợp. Nói cách khác, bắt đầu từ các cơ sở tri thức B1, ..., Bn có thể mâu thuẫn với nhau. Kết quả của cách tiếp cận này sẽ trả về một cơ sở nhất quán duy nhất. Logic khả năng (Mục 1.1.2) là một mô hình phù hợp để mô hình hóa các thông tin được ưu tiên. Nó cho phép mô hình hóa thông tin được ưu tiên bằng các công thức mệnh đề có trọng số. - Cách tiếp cận thứ hai đó là "sống chung" với mâu thuẫn bằng cách sử dụng các 4 paraconsistent logics [30, 31]. Trong đó, chúng ta loại bỏ bớt một số công thức suy luận của logic cổ điển để có thể lập luận với mâu thuẫn. Một số hệ paraconsistent logic phổ biến hiện nay như logic logic thích nghi (Adaptive Logics), logic đa trị (Many-Valued Logics), logic giống với logic cổ điển (Quasi-classical logic),. . . Trong luận văn này tôi tập trung vào cách tiếp cận thứ nhất. Đó là giải quyết mâu thuẫn bằng kỹ thuật tích hợp tri thức. Một cách tổng quát, bài toán tích hợp tri thức dựa trên cấu trúc logic được phát biểu như sau: Cho một tập các cơ sở tri thức, mỗi cơ sở tri thức được biểu diễn bằng một tập các công thức lôgic. Hãy xác định một cơ sở tri thức chung là đại diện tốt nhất cho tập các cơ sở tri thức đã cho. Các cấu trúc logic đã được nghiên cứu trong lĩnh vực này gồm có logic mệnh đề, logic mờ, logic vị từ, logic mô tả và logic khả năng. Để tiện cho việc diễn đạt và giải thích, luận văn sử dụng ví dụ như sau: Ví dụ 1.2.1. Vừa qua, một cuộc khủng hoảng môi trường nghiêm trọng đã gây ra hiện tượng cá chết paq hàng loạt tại các tỉnh ven biển miền Trung Việt Nam. Có một số chuỗi ý kiến về nguyên nhân của hiện tượng này như sau: - Công chúng và các nhà khoa học: Cá chết paq hàng loạt là do vấn đề nước xả thải ô nhiễm của nhà máy gang thép pbq: pb Ñ aq - Nhà máy gang thép: Nhà máy đã đầu tư một hệ thống xử lý nước thải hiện đại pcq, do đó nước đã được xử lý trước khi thải ra biển: pc, c Ñ bq - Cơ quan truyền thông: Nhà máy đã nhập hàng trăm tấn hóa chất độc hại pdq đồng thời hệ thống xử lý nước thải đặt ống xả thải ngầm sai quy định pf q: pd, f q - Công chúng và các nhà khoa học: Một thợ lặn tham gia xây dựng nhà máy đã chết pg q do nước biển quanh khu vực nhà máy bị nhiễm độc pbq:pg, b Ñ g q - Nhà máy: Chúng tôi nhập khẩu chất hóa học pdq để tẩy rửa đường ống, tuy nhiên nước thải đã được xử lý trước khi xả ra biển p pd Ñ bqq. Ống xả thải ngầm đã được cấp phép xây dựng nhưng chưa được hoàn thành, do đó không thể xả thải tại thời điểm hiện tại p f q. - Nhà chức trách: Có hai nguyên nhân dẫn đến hiện tượng cá chết hàng loạt. Nó có thể do chất độc hóa học pdq hoặc do hiện tượng tảo nở hoa peq : pd Ñ aq _ pe Ñ aq. Ngoài ra chưa thấy có bất kỳ mối quan hệ nào giữa nhà máy với hiện tượng cá chết. - Công chúng và các nhà khoa học: Cá chết không thể do hiện tượng tảo nở hoa bởi vì không có dấu hiệu của hiện tượng này như là tảo dạt vào bờ gây ô nhiễm, tảo nở dày đặc gây đổi màu nước và cá chết ở dưới đáy p eq. Từ tiến triển của các sự kiện trên, chúng ta có các tập tri thức như sau: - B1 “ tb Ñ a, g, b Ñ g, eu, - B2 “ tc, c Ñ b, pd Ñ bq, f u, - B3 “ td, f u, - B4 “ tpd Ñ aq _ pe Ñ aqu. Ví dụ này sẽ được sử dụng để minh họa cho các công việc được đề cập trong suốt luận văn này. 5 1.2.2 Duyệt tri thức Nghiên cứu quá trình duyệt tri thức là một lĩnh vực nghiên cứu thú vị và được bắt đầu từ những năm 1980. Các bài viết được phổ biến đánh dấu sự ra đời của lĩnh vực này là các chuyên đề, các hội thảo, các báo cáo của Gardenfors, Alchourron và Makinson [15]. Mô hình được phát triển từ [15] được gọi là mô hình AGM (là tên viết tắt của ba người sáng lập) và ngày nay mô hình này chiếm ưu thế trong duyệt tri thức. Mô hình này sử dụng ngôn ngữ L và mối quan hệ hệ quả (consequence relation) $. L là đóng bởi các toán tử logic. Cho một tập các câu Γ của L, CnpΓq biểu diễn tất cả hệ quả logic(logical consequences) của Γ, nghĩa là CnpΓq “ tϕ P L : Γ $ ϕu. Một lý thuyết K của L là tập các câu của L được bao đóng bởi $, nghĩa là K “ CnpK q. Chúng ta ký hiệu tập tất cả các lý thuyết của L bằng KL . Một lý thuyết K của L là đầy đủ (hoàn toàn) khi mỗi câu ϕ P L, ϕ P K hoặc ϕ P K. ML biểu diễn tập tất cả các lý thuyết đầy đủ nhất quán của L. Với một tập các câu Γ của L. rΓs biểu diễn tập tất cả lý thuyết đầy đủ nhất quán của L có chứa Γ. Chúng ta sẽ sử dụng ký hiệu rϕs cho câu ϕ P L. Cho một lý thuyết K và một tập các câu Γ của L, chúng ta ký hiệu K ` Γ là bao đóng đối với $ của K Y Γ, nghĩa là K ` Γ “ CnpK Y Γq. Với mỗi câu ϕ P L chúng ta thường viết K ` ϕ (thay cho K ` tϕu). Cuối cùng chúng ta sử dụng J và K để biểu diễn cho công thức hằng đúng và công thức hằng sai của L tương ứng. 1.2.2.1 Mô hình AGM Trong mô hình AGM, tri thức được biểu diễn như là một câu của L và một bộ tri thức là một lý thuyết của L. Quá trình duyệt tri thức được mô phỏng là một hàm ˚ ánh xạ một lý thuyết K và một câu ϕ đến một lý thuyết mới K ˚ ϕ. Tất nhiên cũng có những ràng buộc nhất định được đặt ra đối với ˚ để duyệt tri thức một cách chính xác nhất. Một trong số những ràng buộc đó là nguyên tắc thay đổi tối thiểu, tức là một tác nhân phải thay đổi tri thức của mình càng ít càng tốt để phù hợp với thông tin mới K ˚ ϕ. 1.2.2.1.1 Bộ định đề AGM cho duyệt tri thức Gardenfors [16] đã thành công trong việc xây dựng một bộ gồm 8 định đề được gọi là bộ định đề AGM cho duyệt tri thức2 . Ngày nay mô hình này đã chiếm phần lớn bản chất của duyệt tri thức. Cho K là một lý thuyết của L và ϕ P L. Hàm ˚ là một hàm duyệt tri thức nếu nó thỏa mãn các định đề sau: (K*1) K ˚ ϕ là lý thuyết của L. (K*2) ϕ P K ˚ ϕ. (K*3) K ˚ ϕ Ď K ` ϕ. (K*4) Nếu ϕ R K thì K ` ϕ Ď K ˚ ϕ. 2 Ban đầu, các định đề được đề xuất bởi một mình Gardenfors, nhưng sau đó ông đã hợp tác nghiên cứu cùng với Alchourron và Makinson. Do đó bộ định đề được mang tên của cả ba người. 6 (K*5) Nếu ϕ là nhất quán thì K ˚ ϕ cũng nhất quán. (K*6) Nếu $ ϕ Ø ψ thì K ˚ ϕ “ K ˚ ψ. (K*7) K ˚ pϕ ^ ψ q Ď pK ˚ ϕq ` ψ (K*8) Nếu ψ R K thì pK ˚ ϕq ` ψ Ď K ˚ pϕ ^ ψ q. Với bất kỳ một hàm ˚ : K ˆ L ÞÑ KL đáp ứng các định đề AGM cho duyệt tri thức pK ˚ 1q ´ pK ˚ 8q được gọi là hàm duyệt AGM . Sáu định đề đầu tiên pK ˚ 1q ´ pK ˚ 6q được gọi là định đề AGM cơ bản (cho duyệt tri thức). Trong khi pK ˚ 7q ´ pK ˚ 8q được gọi là định đề AGM bổ sung. Định đề pK ˚ 1q chỉ ra rằng kết quả của phép duyệt giữa lý thuyết K và một câu ϕ cũng là một lý thuyết của L. Định đề pK ˚ 2q chỉ ra rằng thông tin mới ϕ luôn nằm trong tập tri thức mới. Mệnh đề pK ˚ 3q và pK ˚ 4q cùng chỉ ra rằng nếu một thông tin mới ϕ mà không mâu thuẫn với tập tri thức K thì không có lý do gì để loại bỏ nó khỏi tri thức ban đầu. Thông tin mới K ˚ ϕ sẽ bao gồm toàn bộ K, thông tin mới ϕ và bao đóng (logical closure) của K và ϕ. Về cơ bản pK ˚ 3q và pK ˚ 4q cho ta thấy ý tưởng của thay đổi tối thiểu trong trường hợp thông tin mới không mâu thuẫn với tri thức ban đầu. Mục đích của việc duyệt tri thức là để tạo ra một tập tri thức mới nhất quán, pK ˚ 5q phát biểu rằng nếu thông tin mới ϕ là nhất quán thì kết quả của phép duyệt K ˚ ϕ tạo ra một thông tin mới cũng nhất quán.pK ˚ 6q là nguyên tắc không phụ thuộc cú pháp, tức là cú pháp của thông tin mới sẽ không ảnh hưởng đến quá trình duyệt và tất cả vấn đề là ở nội dung của nó (tức là các mệnh đề mà nó biểu diễn). Do đó lý thuyết K được duyệt bởi hai câu tương đương logic ϕ và ψ sẽ cho các kết quả tương đương logic với nhau. Cuối cùng, định đề pK ˚ 7q và pK ˚ 8q phát biểu rằng: cho hai câu ϕ và ψ. Nếu kết quả của phép duyệt của lý thuyết ban đầu K bởi ϕ mà tạo ra một lý thuyết mới K ˚ ϕ nhất quán với ψ, thì để tạo ra K ˚ pϕ ^ ψ q việc chúng ta cần làm là mở rộng kết quả K ˚ ϕ với ψ. Động lực để có các định đề pK ˚ 7q và pK ˚ 8q một lần nữa lại xuất phát từ nguyên tắc thay đổi tối thiểu: K ˚ ϕ là thay đổi tối thiểu của K để bao hàm ϕ, do đó không có cách nào để tạo ra K ˚ pϕ ^ ψ q từ K với thay đổi "ít hơn". Thực tế, bởi vì K ˚ pϕ ^ ψ q cũng bao gồm cả ψ nên có thể thực hiện các thay đổi thêm để loại bỏ những thứ cần thiết để bao gồm cả ϕ. Nếu ψ là nhất quán với K ˚ ϕ thì những thay đổi này có thể giới hạn bằng cách thêm ψ vào K ˚ ϕ. 1.2.2.1.2 Bộ định đề AGM cho loại bỏ tri thức Ngoài duyệt tri thức AlChourron, Gardenfor và Makinson còn nghiên cứu thêm một lĩnh vực thay đổi khác đó là loại bỏ tri thức (hoặc đơn giản là loại bỏ). Đây là quá trình loại bỏ từ một bộ tri thức K một số tri thức ϕ nhất định nào đó. Loại bỏ thường xảy ra khi một đối tượng mất niềm tin vào ϕ và quyết định loại bỏ nó, đơn giản chỉ là đưa ϕ ra khỏi K. Tuy nhiên việc loại bỏ sẽ không đáp ứng được nếu các câu khác đang có trong K có thể lại sinh ra ϕ thông qua tính bao đóng. Ví dụ: giả sử cho K “ Cnptp Ñ q, p, q uq và chúng ta muốn lọai bỏ p khỏi K . Để loại bỏ được, chúng ta không phải chỉ loại bỏ duy nhất p từ K mà chúng ta cũng cần phải loại bỏ (ít nhất) p Ñ q hoặc p. Nếu không q sẽ lại được sinh ra thông qua tính đóng. 7 . Giống như duyệt tri thức, loại bỏ tri thức cũng là một hàm ´ ánh xạ một lý thuyết . K và một câu ϕ đến một lý thuyết mới K ´ ϕ. Một lần nữa một bộ tám định đề được đề xuất theo nguyên tắc thay đổi tối thiểu. . Cho K là một lý thuyết của L và ϕ P L. Hàm ´ là một hàm loại bỏ tri thức nếu nó thỏa mãn các định đề sau: . . (K´ 1) K ´ ϕ là lý thuyết. . . (K´ 2) K ´ ϕ Ď K. . . (K´ 3) Nếu ϕ R K thì K ´ ϕ “ K . . (K´ 4) Nếu & ϕ thì ϕ R K ´ ϕ . . (K´ 5) Nếu ϕ P K thì K Ď pK ´ ϕq ` ϕ . . . (K´ 6) Nếu $ ϕ Ø ψ thì K ´ ϕ “ K ´ ψ . . . . (K´ 7) pK ´ ϕq X pK ´ ψ q Ď K ´ pϕ ^ ψ q . . . . (K´ 8) ϕ R K ´ pϕ ^ ψ q thì K ´ pϕ ^ ψ q Ď K ´ ϕ . . . Bất kỳ hàm ´ : K ˆ L ÞÑ KL đáp ứng pK ´ 1q ´ pK ´ 8q được gọi là một hàm loại bỏ . . AGM. Giống như những định đề duyệt tri thức, pK ´ 1q ´ pK ´ 8q được chia thành 2 . . nhóm. Nhóm đầu 6 định đề pK ´ 1q ´ pK ´ 6q được gọi là định đề AGM cơ bản cho . 7q ´ pK ´ 8q được gọi là định đề AGM bổ sung cho . loại bỏ tri thức, trong khi pK ´ loại bỏ tri thức. . Định đề pK ´ 1q chỉ ra rằng kết quả của việc loại bỏ giữa lý thuyết K và một câu . ϕ cũng là một lý thuyết. Định đề pK ´ 2q phát biểu rằng quá trình loại bỏ sẽ tạo ra . một tri thức mới nhỏ hơn tri thức ban đầu. Định đề pK ´ 3q phát biểu rằng nếu thông tin ϕ mà không thuộc tri thức ban đầu thì quá trình loại bỏ sẽ không làm thay đổi . bất cứ điều gì. Định đề pK ´ 4q phát biểu rằng nếu một thông tin ϕ mà không phải là chân lý thì kết quả của quá trình loại bỏ sẽ không bao gồm thông tin đó. Định đề . pK ´ 5q được gọi là định đề phục hồi và nó chỉ ra rằng từ kết quả thu được sau quá trình loại ϕ chúng ta tiếp tục mở rộng với ϕ thì chúng ta sẽ thu được lý thuyết ban . đầu K. Định đề pK ´ 6q phát biểu rằng kết quả của việc loại bỏ các câu tương đương logic nhau thì cho kết quả giống nhau. Hai định đề cuối cùng liên quan đến việc loại bỏ hai câu ϕ và ψ riêng biệt và loại bỏ bởi kết hợp của chúng (ϕ ^ ψ). Đầu tiên, để loại bỏ K bởi ϕ ^ ψ chúng ta cần loại bỏ ϕ hoặc ψ hoặc cả hai. Bây giờ chúng ta xem xét một tri thức χ P K thu được sau khi loại bỏ bởi ϕ cũng như loại bỏ bởi ψ (nghĩa . . là χ P K ´ ϕ và χ P K ´ ψ). Điều này có nghĩa là trong ngữ cảnh của K, χ không liên . quan đến ϕ, ψ cũng như kết hợp của chúng. Do đó, định đề pK ´ 7q theo nguyên tắc thay đổi tối thiểu χ không bị ảnh hưởng bởi loại bỏ K bởi ϕ ^ ψ. Cuối cùng, định đề . . . pK ´ 8q giả sử rằng ϕ R K ´ pϕ ^ ψ q. Vì K ´ ϕ là thay đổi nhỏ nhất của K để loại bỏ . . ϕ, từ đó suy ra K ´ pϕ ^ ψ q không thể lớn hơn K ´ ϕ. Có một mối quan hệ giữa mô hình duyệt tri thức và loại bỏ tri thức, nó đã được đề xuất vởi Isaac Levi trước khi Alchourron, Gardenfors, và Makinson xây dựng định đề của họ. Nói chính xác hơn, Levi cho rằng ta nên tuân theo nguyên tắc được xác định quá trình duyệt tri thức liên quan đến loại bỏ tri thức như sau: để duyệt K bởi 8 ϕ, đầu tiên ta loại bỏ ϕ khỏi K (khi đó ta có thể loại bỏ bất kỳ thông tin nào có thể mâu thuẫn với thông tin mới) và sau đó mở rộng kết quả lý thuyết với ϕ. Nguyên tắc đó được gọi là đồng nhất Levi: . K ˚ ϕ “ pK ´ ϕq ` ϕ . Định lý 1.2.2. (Alchourron, Gardenfors, và Makinson [15]) cho ´ là hàm bất kỳ từ . . K ˆ L đến KL đáp ứng được các định đề pK ´ 1q ´ pK ´ 8q. Thì các hàm ˚ tạo ra từ . ´ bằng đồng nhất Levi thỏa mãn các định đề pK ˚ 1q ´ pK ˚ 8q. Trên thực tế AGM cho hàm duyệt và hàm loại bỏ có liên quan đến các tiên đoán của Levi, là dẫn chứng chính đầu tiên để cung cấp, hỗ trợ cho các định lý AGM để loại bỏ và duyệt tri thức. Một quy trình xác định loại bỏ trong giới hạn của duyệt cũng đó được chỉ ra. Nó được biết đến với tên gọi là đồng nhất Harper: . K ´ ϕ “ pK ˚ ϕq X K Giống như đồng nhất Levi, đồng nhất Harper là đúng và đầy đủ để xây dựng các . hàm loại bỏ. Tức là, hàm ´ được tạo ra từ một hàm duyệt AGM bằng đồng nhất . . Happer thỏa mãn pK ´ 1q ´ pK ´ 8q và ngược lại. Mỗi một hàm loại bỏ AGM có thể được tạo ra từ một hàm duyệt bằng đồng nhất Harper. Trên thực tế, bằng cách kết hợp đồng nhất Levi và đồng nhất Harper đã tạo thành một vòng tròn đầy đủ. Nếu . chúng ta bắt đầu với một hàm loại bỏ AGM ´ và sử dụng đồng nhất Levi để tạo ra một hàm duyệt ˚ lần lượt được sử dụng để tạo ra một hàm loại bỏ bằng đồng nhất . Harper. Kết quả chúng ta đạt được tương tự hàm loại bỏ ´ mà chúng ta đã bắt đầu. 1.2.2.2 Hàm lựa chọn Xét một lý thuyết K, cho ϕ là câu không phải định lý mà chúng ta muốn loại bỏ khỏi K. Vì quá trình loại bỏ của ta cần phải tuân thủ theo nguyên tắc thay đổi tối thiểu, điều đầu tiên nghĩ đến là xác định một tập con lớn nhất của K mà không dẫn xuất ra ϕ và chỉ định đó là kết quả của sự loại bỏ ϕ khỏi K. Thật không may, có nhiều hơn một tập con như vậy, tất cả chúng không phải là rõ ràng và làm thế nào để có thể lựa chọn được giữa chúng3 . Bất kỳ một tập con lớn nhất nào của K mà không dẫn xuất ra ϕ thì được gọi là một ϕ-remainder4 và tập hợp tất cả ϕ-remainder được ký hiệu là K K ϕ5 . K Như đã đề cập, mỗi ϕ-remainder không phải là rõ ràng và làm thế nào để lựa chọn giữa các ϕ-remainder vì tất cả chúng đều tốt theo quan điểm logic. Trong mô hình AGM , việc này được thực hiện thông qua hàm lựa chọn. Một hàm lựa chọn cho một lý thuyết K là một hàm γ bất kỳ mà ánh xạ từ một tập khác rỗng X của các tập con của K tới một tập hợp khác rỗng γ pX q của X. Nghĩa là:H ‰ γ pX q Ď X. Một hàm lựa chọn được sử dụng để nhận biết ϕ-remainder “tốt nhất”. Nghĩa là các phần tử của 3 Xem xét lý thuyết K “ Cnptp, quq, trong đó p, q là hai biểu thức mệnh đề, giả sử chúng ta muốn loại bỏ K bởi p ^ q. Có nhiều hơn một tập con của K không dẫn xuất ra p ^ q, một trong số đó có chứa p nhưng không chứa q và tập còn lại chứa p nhưng không chứa q. 4 Một ϕ-remainder là một tập con K’ của K sao cho (i) K 1 & ϕ, (ii) với mỗi K 2 Ď K, nếu K 1 Ă K” thì K 2 $ ϕ 5 Trong một số trường hợp khi ϕ lặp lại thì K K ϕ được xác định là tKu K 9