Bài giảng Cơ sở logic đặc tả của OWL - Lê Thanh Hương

Chia sẻ: Minh Vũ | Ngày: | Loại File: PDF | Số trang:8

Thêm vào BST

Báo xấu

62
lượt xem 7
download

Download Vui lòng tải xuống để xem tài liệu đầy đủ

Bài giảng "Cơ sở logic đặc tả của OWL" cung cấp cho người học các kiến thức: ALC, cú pháp ALC, mở rộng, cơ sở tri thức, ngữ nghĩa ALC, các khái niệm tương đương, suy luận với ALC, các kiểu suy luận,... Mời các bạn cùng tham khảo.

Chủ đề:

Bình luận(0) Đăng nhập để gửi bình luận!

Lưu

Nội dung Text: Bài giảng Cơ sở logic đặc tả của OWL - Lê Thanh Hương

ALC CƠ SỞ LOGIC ĐẶC Ặ TẢ CỦA OWL Là dạng ạ g đơn giản g nhất của DL Các khái niệm sử dụng ∩ ∪ ¬ ∃ ∀ Chỉ có các vai trò đơn (vd, đảo) Ví dụ: Person all of whose children are either Doctors or have a child who is a Doctor: Person ∩ ∀hasChild.(Doctor ∪ ∃hasChild.Doctor) Hanoi University of Technology – Master 2006 2 Cú pháp ALC Mở rộng Extracts from slides of Bruijn and Franconi S – vai trò mở rộng (transitive roles) (R+) H – phân cấp vai trò (role hierarchy), vd (khái niệm đơn) Các đánh giá đơn trong ALC hasDaughter ⊆ hasChild) (khái niệm vũ trụ) O – lớp định danh/đơn (nominals/singleton (khái niệm đáy) classes), vd ∃hasChild.{mary} (phép giao) I - vai trò đảo, vd isChildOf ≡ hasChild– (phép hợp) Các tiên đề trong ALC N – giới hạn số lượng (number restrictions), vd (phủ định) ≤1hasChild (giới hạn giá trị) Q – giới ớ hạn h số ố lượng l thỏa hỏ 1 tính í h chất hấ nào à đó (lượng từ tồn tại) (qualified number restrictions), ≥1hasChild.Male S + role hierarchy (H) + nominals (O) + inverse (I) + NR (N) = SHOIN 3 4 1
Cơ sở tri thức Cơ sở tri thức TBox là tập các luật (câu), vd: Phát biểu thuật ngữ {Doctor ⊆ Person, HappyParent ≡ Person ∩ ∀hasChild.(Doctor ∪ ∃hasChild.Doctor)} {Doctor → Person, HappyParent ↔ Person ∧[hasChild](Doctor ∨〈hasChild〉Doctor} ABox là tập các sự kiện {John:HappyParent, John hasChild Mary} {John → HappyParent, Phát biểu thành viên: John → 〈hasChild〉Mary} 1 CSTT (Knowledge Base - KB) là TBox + Abox 5 6 Bài tập Bài tập Xây dựng Tbox cho các phát biểu sau: Xây dựng Tbox cho các phát biểu sau: Mammals are animals. y fish is an animal that lives in water;; Every Cats are mammals that are carnivores. Something that eats meat is a carnivore; Elephants are mammals that are herbivores. A bird is a vertebrate that has wings and legs Carnivores eat meat. and lays eggs; A vertebrate is any animal that has, amongst Every reptile is a vertebrate that lays eggs. other things, a backbone. 7 8 2
Ngữ nghĩa ALC Bài tập Phép dịch , trong đó Dịch các Tbox sau: ΔI là miền everybody whose children are all male .I là hàm dịch cho phép gắn: • Mọi khái niệm A với tập con AI của ΔKhái I niệm đơn • Mọi vai trò r với quan hệ nhị phân rI trên ΔI the class of objects interested in computer science but not Khái niệm đơn interested in philosophy Vai trò đơn Đỉnh all living beings that are not human beings Đáy Phần bù all ll students t d t nott iinterested t t d iin mathematics th ti Phần giao all students who only drink tea Phần hợp Lượng tử với mọi Lượng tử tồn tại everybody who has a child and whose children are all male 9 10 Các khái niệm tương đương Ví dụ Cho , trong đó Với mọi phép dịch I, các khái niệm C, D và vai trò r, ta có Tính 11 12 3
Ngữ nghĩa ALC Suy luận với ALC Extracts from slides of Franconi Phép dịch I thỏa mãn Định nghĩa khái niệm Phát biểu I thỏa mọi phát biểu trong T I là một mô hình của T Đánh giá khái niệm Đánh giá vai trò I thỏa mọi đánh giá trong A I là một mô hình của A Phép dịch I=(ΔΙ,.Ι) là một mô hình của CSTT ∑ nếu mọi phát biểu của ∑ đều thỏa bởi I CSTT ∑ được nói là “có thể đáp ứng được” nếu nó có mô hình tuơng ứng 13 14 Các kiểu suy luận Ví dụ về thỏa khái niệm Thỏa mãn khái niệm Kiểm ể tra C có thỏa ∑ không, nghĩa là có một mô hình I của ∑ sao cho CI ≠ ∅ Cho biết ¬woman ∩ mother có đúng không? Tập con Kiểm tra C có là tập con của D thỏa ∑ không, nghĩa là CI ⊆ DI với mọi mô hình I của ∑ Tính thỏa Kiểm tra ∑ có thỏa không, nghĩa là nó có một mô hình nào đó không Kiểm tra giá trị ¾ Không có mother nào không phải là women 15 16 4
Thuật toán Tableaux Thuật toán Tableaux Thuật toán Tableaux dùng để đánh giá sự thỏa mãn Thuật toán Tableaux hoạt động bằng cách cố Nghĩa là, cố gắng xây dựng một mô hình cây cho các gắng xây dựng 1 ví dụ (mô hình) thỏa mãn khái niệm đã cho C CSTT: Quá trình xử lý Xuất phát từ các tri thức ban đầu (ABox axioms) Ngắt cú pháp của C ở dạng kết nối {C1, C2,…} Sinh ra các câu mới dựa trên các khái niệm và Chỉ làm việc với các khái niệm ở dạng chuẩn phủ định TBox Sử dụng luật Morgan, vd, ¬∃R.C ≡ ∀R.¬C Tạo các biểu thức phức bằng cách sử dụng các Tách các khái niệm sử dụng luật tableau luật mở rộng tableaux Dừngừ g khi có xung u g đột , vd d {C1, ¬C C1,,…}, }, hoặc oặc khi Suy S diễn các ràng àng buộc b ộc ttrong ong mô hình không còn luật nào có thể áp dụng được Phát hiện các chu trình để đảm bảo thuật toán kết thúc C là bền vững nếu không có xung đột khi áp dụng thuật toán tableau 17 18 Suy diễn với Tableaux (1) Suy diễn với Tableaux (2) Vd, CSTT: {HappyParent ≡ Person ∩ ∀hasChild.(Doctor ∪ ∃hasChild.Doctor), Luật Tableau tương ứng với các hàm thiết lập trong logic (∩, ∃, etc) John:HappyParent, John hasChild Mary, Mary:¬Doctor E g John:(Person ∩ Doctor) → John:Person and John:Doctor E.g., Wendy hasChild Mary, Wendy marriedTo John} Dừng khi không còn luật nào có thể áp dụng hoặc khi xung đột xảy ra Xung đột là mâu thuẫn hiển nhiên, vd, A(x), ¬A(x) Một số luật là không tất định (nondeterministic) (vd, ∪, ≤) Trên thực tế, điều đó nghĩa là tìm kiếm (search) Cần kiểm tra chu trình (ngăn chặn) để đảm bảo tính kết thúc Person Vd, KB: Vd ∀hasChild.(Doctor ∪ ∃hasChild.Doctor) {Person ⊆ ∃hasParent.Person, John:Person} 19 20 5
Bài tập Luật Tableaux cho ALC Xét CSTT K = (T,A) với TBox T : Clownfish ∪ Surgeonfish ⊆ Fish (1) Clownfish ∩ Surgeonfish ≡ ⊥ (2) ABox A: nemo : Clownfish ∩ ∃has_colour.Orange (3) dory : Surgeonfish ∩ ∀likes.Clownfish (4) (nemo, dory) : has_friend (5) Xây Xâ dựng dự một ột mô ô hình hì h cây â cho h các á khái niệm iệ đã cho h Trả lời các câu hỏi sau: Dori có 1 người bạn màu cam không? Nemo có 1 người bạn chỉ thích Clownfish không? 21 22 Ví dụ về suy luận Tableau Bài tập Khái niệm có thỏa không Xây dựng phép dịch thỏa khái niệm trên Suy luận Tableau cho khái niệm C ≡ ¬woman ∩ mother từ từ từ và từ từ Mâu thuẫn và ⇒ Khái niệm trên không thỏa 23 24 6
Bài tập Bài tập Khái niệm có thỏa không Xây dựng phép dịch thỏa khái niệm trên Khái niệm có thỏa không Xây dựng phép dịch thỏa khái niệm trên từ từ từ và từ từ từ từ từ và từ ⇒ Khái niệm trên thỏa và thỏa mô hình từ từ Khi đó (8.1) mâu thuẫn, (8.2) không mẫu thuẫn ⇒ mô hình thỏa k/n 25 26 Mở rộng ALC cho SHOIN Sự tương ứng giữa SHOIN và FOL Extracts from slides of Bruijn 27 28 7
Ví dụ Further reading OWL Abstract Syntax and Semantics: http://www.w3.org/TR/owl-semantics/ Description Logic Handbook, edited by F. Baader, D. Calvanese, D.L. McGuinness, D. Nardi, P.F. Patel-Schneider, Cambridge University Press. Online course on Description Logics of Enrico Franconi: http://www.inf.unibz.it/~franconi/dl/course/ 29 30 Further reading Jos de Bruijn: Using Ontologies. Enabling Knowledge Sharing and Reuse on the Semantic Web. DERI Technical Report DERI-2003-10-29, 2003. http://www.deri.org/publications/techpapers/d ocuments/DERI-TR-2003-10-29.pdf OWL Guide: http://www.w3.org/TR/owl-guide/ OWL Reference: http://www.w3.org/TR/owl- ref/ OWL Abstract syntax and Semantics: http://www.w3.org/TR/owl-semantics/ 31 8