Różnice między wybraną wersją a wersją aktualną.
|
pl:dydaktyka:krr:lab_dl_reasoning [2016/06/08 01:44] msl [4 Algorytmy wnioskowania] |
pl:dydaktyka:krr:lab_dl_reasoning [2017/07/17 10:08] |
||
|---|---|---|---|
| Linia 1: | Linia 1: | ||
| - | ====== - Wnioskowanie w logikach deskrypcyjnych ====== | ||
| - | * Logiki opisowe, dzięki formalnemu ugruntowaniu w logice, umożliwiają automatyczne wnioskowanie. | ||
| - | * Osobne __zadania wnioskowania__ definiuje się dla TBoxa i ABoxa. | ||
| - | * W logikach opisowych stosuje sią [[http://en.wikipedia.org/wiki/Open_world_assumption|Założenie o otwartości świata]]. | ||
| - | * Podstawowymi algorytmami dla DL są: | ||
| - | * algorytmy strukturalne (Structural subsumption algorithms) | ||
| - | * algorytmy tableau (Tableau algorithms) | ||
| - | * Złożoność obliczeniona poszczególnyc zadań wnioskowania zależy od siły ekspresji języka DL | ||
| - | * zobacz [[http://www.cs.man.ac.uk/~ezolin/dl/|przewodnik po językach DL]] | ||
| - | * Przykładowe wyniki dla zadania subsumcji: | ||
| - | {{ http://www.obitko.com/tutorials/ontologies-semantic-web/images/dl-complexity.gif |}} | ||
| - | |||
| - | ==== - Zadania wnioskowania dla TBoxa ==== | ||
| - | - Spełnialność (ang. //satisfiability//) | ||
| - | * Pojęcie C jest //spełnialne// względem terminologii T jeżeli istnieje model (interpretacja) I taki że <latex> C^{\mathcal{I}}</latex> jest niepusty. | ||
| - | - Subsumcja ((subsumcja (sub- + sumere ‘brać’) log. proces wynajdowania dla danego pojęcia innego pojęcia, bardziej ogólnego. Wg. "Słownik Wyrazów Obcych" Wydawnictwa Europa, pod redakcją naukową prof. Ireny Kamińskiej-Szmaj, autorzy: Mirosław Jarosz i zespół. ISBN 83-87977-08-X. Rok wydania 2001.)) (ang. //subsumption//) | ||
| - | * Pojęcie C jest włączone w pojęcie D wzg. T jeżeli <latex> C^{\mathcal{I}} \subseteq D^{\mathcal{I}}</latex> dla każdego modelu I terminologii T. | ||
| - | - Równoważność (ang. //equivalence//) | ||
| - | * Dwa pojęcia C i D są sobie //równoważne// wzg. T jeżeli <latex> C^{\mathcal{I}} = D^{\mathcal{I}}</latex> dla każdego modelu I terminologii T. | ||
| - | - Rozłączność (ang. //disjointness//) | ||
| - | * Dwa pojęcia C i D są //rozłączne// wzg. T. jeżeli <latex> C^{\mathcal{I}} \cap D^{\mathcal{I}} = \emptyset</latex> dla każdego modelu I terminologii T. | ||
| - | |||
| - | __**Ćwiczenie 6**__ | ||
| - | - Wiedząc, że: | ||
| - | * <latex>Vegetarian \equiv (\forall eats.(\neg (\exists partOf.Animal))) \sqcap (\forall eats.(\neg Animal)) \sqcap Animal</latex> | ||
| - | * <latex>Cow \sqsubseteq Vegetarian</latex> | ||
| - | * <latex>MadCow \equiv \exists eats.(\exists partOf.Sheep \sqcap Brain) \sqcap Cow </latex> \\ Odpowiedz na pytanie: | ||
| - | - Jakiemu pojęciu jest równoważne pojęcie ''MadCow''? | ||
| - | - Wykorzystując bazę wiedzy z sekcji [[#terminologia_tbox]] odpowiedz na pytanie: | ||
| - | - Czy zdanie" "Każdy kto prowadzi przedmiot musi mieć tytuł inżyniera" jest logiczną konsekwencją tej bazy wiedzy? Odpowiedź uzasadnij. | ||
| - | |||
| - | |||
| - | ==== - Zadania wnioskowania dla ABoxa ==== | ||
| - | - Sprawdzenie spójności (ang. //consistency checking//) | ||
| - | * ABox A jest //spójny// wzg. terminologii T, jeżeli istnieje nterpretacja I będąca jednocześnie modelem A i T. | ||
| - | - Sprawdzanie instancji (ang. //instance checking//) | ||
| - | * <latex> A \models \alpha</latex> iff każda interpretacja spełniająca A spełnia również α. | ||
| - | - Poszukiwanie najbardziej szegółowego pojęcia dla danej instancji (ang. //realization//). | ||
| - | - Poszukiwanie instancji danego pojęcia (ang. //retrieval//). | ||
| - | |||
| - | __Uwaga:__ | ||
| - | * wszystkie zadania TBox mogą być zredukowane do zadania subsumcji lub spełnialności | ||
| - | * C i D są rozłączne ⇔ <latex> C \sqcap D</latex> zawiera się w ⊥ | ||
| - | * np. C zawiera się D ⇔ <latex> C \sqcap \neg D </latex> nie jest spełnialne (na tej obserwacji opierają się algorytmy tableau) | ||
| - | * wszystkie zadania wnioskowania mogą być sprowadzone do sprawdzenia spójności bazy wiedzy. | ||
| - | |||
| - | __**Ćwiczenie 7**__: | ||
| - | - Wiedząc, że: | ||
| - | * <latex> OldLady \equiv Elderly \sqcap Female \sqcap Person</latex> | ||
| - | * <latex> OldLady \sqsubseteq \exists hasPet.Animal </latex><latex> \sqcap </latex><latex> \forall hasPet. Cat </latex> | ||
| - | * <latex> hasPet(Minnie,Tom)</latex>,<latex> Elderly(Minnie)</latex>,<latex> Female(Minnie)</latex> \\ Odpowiedz na pytania: | ||
| - | - Czy każda starsza pani musi mieć kota? Dlaczego? | ||
| - | - Do jakiej klasy należy obiekt Minnie? | ||
| - | - Do jakiej klasy należy obiekt Tom? | ||
| - | - Rozważ opis świata z sekcji [[#abox]] i odpowiedz na pytanie: | ||
| - | * Czy John należy do klasy: ∃friend.(Female ⊓ ∃loves.¬Female)? | ||
| - | * Podpowiedź: | ||
| - | * Zwizualizuj w postaci grafu ten ABox, zaobserwuj, do jakich klas należą poszczególne obiekty. | ||
| - | * Rozważ dwa przypadki: ''andrea : Female'' i ''andrea : ¬Female'' | ||
| - | |||
| - | |||
| - | Odpowiedzi: [[lab_dl_answers#wnioskowanie]] | ||
| - | |||
| - | ==== - Założenie o otwartości świata ==== | ||
| - | * Analogia bazy wiedzy DL i relacyjnej bazy danych: | ||
| - | * schemat bazy danych <-> TBox | ||
| - | * instancje danych <-> ABox | ||
| - | * W przeciwieństwie do relacyjnych baz danych, brak w ABox oznacza **brak wiedzy**, nie zaś negatywnąinformację | ||
| - | * ABox reprezentuje potencjalnie nieskończenie wiele interpretacji. | ||
| - | * Semantyka otwartego świata wymaga nietrywialnych mechanizmów wnioskowania, a realizaja zapytań jest bardziej skomplikowana. | ||
| - | |||
| - | **BONUS**: | ||
| - | * [[http://www.cs.man.ac.uk/~horrocks/ISWC2003/Tutorial/examples.pdf|Więcej przykładów wnioskowania...]] | ||
| - | |||
| - | ==== - Algorytmy wnioskowania ==== | ||
| - | === Strukturalne === | ||
| - | Porównują strukturę składniową pojęć. | ||
| - | Są efektywne, ale odpowiednie tylko do prostych języków, np. nie działają dla języków z negacją i dysjunkcją | ||
| - | |||
| - | === Tableau === | ||
| - | Opierają swoje działanie na obserwacji, że: <latex>C \sqsubseteq D</latex> wtw. gdy wyrażenie <latex>C \sqcap \neg D </latex> jest niespełnialne. | ||
| - | Schemat działania: | ||
| - | - Start od faktów (aksjomatów ABox) | ||
| - | - Dekompozycja składniowa z użyciem odpowiednich reguł tzw. //tableaux expansion rules// | ||
| - | * reguły odpowiadają poszczególnymkonstruktorom (<latex> \sqcap, \sqcup, ...</latex>) | ||
| - | * niektóre reguły są niedeterministyczne (np. <latex> \sqcup, \leq </latex>) (w praktyce prowadzi to do przeszukiwania) | ||
| - | - Wnioskowanie o ograniczeniach na elementach modelu | ||
| - | - Stop, kiedy nie można zastosować więcej reguł lub wystąpiła sprzeczność | ||
| - | |||
| - | __**Ćwiczenie 8**__ (dla chętnych): | ||
| - | |||
| - | Sprawdź czy poniższe pojęcia są spełnialne: | ||
| - | - A ⊓ ∃R.C ⊓ ∀R.D | ||
| - | - ∃R.C ⊓ ∀R.¬(C ⊓ D) | ||
| - | - A⊓∃R.C⊓∀R.D⊓∀R.¬(C⊓D) | ||
| - | - ∃R.(A ⊓ ∃R.C) ⊓ ∀R.¬C | ||
| - | - ∃R.(A ⊓ ∃R.C) ⊓ ∀R.∀R.¬C | ||
| - | - ¬C ⊓ ∃R.C ⊓ ∀R.(¬C ⊔ ∃R.C) | ||
| - | - A ⊓ ∀R.A ⊓ ∀R.¬∃P.A ⊓ ∃R.∃P.A | ||
| - | |||
| - | |||
| - | |||
| - | ==== - Wsparcie narzędziowe ==== | ||
| - | Istnieje wiele implementacji silników wnioskujących dla logik deskrypcyjnych. | ||
| - | Niektóre z nich są zoptymalizowane pod kątem konkretnych języków DL (np. takich na których opierają się warianty języka ontologii OWL ). | ||
| - | |||
| - | Lista dostępnych silników wnioskujących dostępna jest na stronie: [[http://www.cs.man.ac.uk/~sattler/reasoners.html|Prof. U. Sattler]]. | ||
| - | Popularne narzędzia to m.in: | ||
| - | * [[http://clarkparsia.com/pellet/download|Pellet]] | ||
| - | * [[http://www.cs.man.ac.uk/~horrocks/FaCT/|FaCT]] | ||
| - | * [[http://www.sts.tu-harburg.de/%7Er.f.moeller/racer/|Racer]] | ||
| - | * [[http://www.sts.tu-harburg.de/%7Er.f.moeller/racer/Racer-1-9-2-beta-Release-Notes/release-notes-1-9-2se3.html#x4-70003.2|RacerPorter]] GUI | ||
| - | * [[http://blipkit.wordpress.com/2010/11/27/posh-the-prolog-owl-shell/|POSH: the prolog OWL shell]] | ||
| - | * [[http://code.google.com/p/dlmodel/|DL model]] | ||
| - | * [[http://db-tom.cs.uwaterloo.ca/AssertionRetrieval/pages/kbgen.jsp|CARE]] - online | ||
| - | |||
| - | Najczęściej silniki wnioskujące zintegrowane są z innymi narzędziami, np. edytorami ontologii (pełnią one wówczas rolę pomocniczą, np. do sprawdzania spójności ontologii itp.). | ||
| - | |||
| - | __**Ćwiczenie 9**__: | ||
| - | - Pobierz silnik wnioskujący [[http://clarkparsia.com/pellet/download|Pellet]]. | ||
| - | - :!: Na borgu powinien być w ''/usr/local/pellet''. | ||
| - | - Uruchom go wpisując w konsoli ''pellet.sh help'' i zapoznaj się z dostępnymi opcjami. (''/usr/local/pellet/pellet.sh'') | ||
| - | - Uruchom ''pellet.sh consistency <ontology>'' gdzie ''<ontology>'' jest bazą wiedzy ''people+pets.owl'' umieszczoną w katalogu ''examples/data''. | ||
| - | - Jakie są rezultaty? | ||
| - | - Uruchom ''pellet.sh classify <ontology>'' dla powyższej ontologii ''peopl+pets.owl'' | ||
| - | - Jakie są rezultaty? | ||
| - | |||
| - | |||
| - | ===== Materiały ===== | ||
| - | ==== Wykłady, prezentacje ==== | ||
| - | * [[http://www.inf.unibz.it/~franconi/dl/course/|DL Course]] by Enrico Franconi | ||
| - | * **[[http://www.inf.unibz.it/~franconi/dl/course/slides/prop-DL/propositional-dl.pdf|Propositional Description Logics]]** :!: | ||
| - | * [[http://www.inf.unibz.it/~franconi/dl/course/slides/kbs/kbs.pdf|Knowledge Bases in Description Logics]] | ||
| - | * [[http://www.inf.unibz.it/~franconi/dl/course/slides/logic/fol/fol-2.pdf|DL reasoning, FOL etc.]] | ||
| - | |||
| - | * [[http://www.cse.iitd.ac.in/~kkb/DL-1.pdf|DL Tutorial]] | ||
| - | |||
| - | * [[http://www.cs.man.ac.uk/~horrocks/Slides/IJCAR-tutorial/Print/p1-introduction.pdf|Description Logics—Basics, Applications, and More]] | ||
| - | |||
| - | * [[http://www.cs.put.poznan.pl/jjozefowska/wyklady/ai/Ontologie.pdf|Ontologie, Logiki deskrypcyjne]] | ||
| - | * [[http://www.cs.man.ac.uk/~horrocks/Slides/index.html|Horrock's Presentations]] | ||
| - | * [[http://www.inf.unibz.it/~franconi/dl/course/slides/db/db.pdf|DL and DB]] | ||
| - | |||
| - | * [[http://www.obitko.com/tutorials/ontologies-semantic-web/description-logics.html|DL]] by Obitko | ||
| - | * [[http://www.obitko.com/tutorials/ontologies-semantic-web/syntax-and-semantics.html|Syntax & Semantics]] | ||
| - | * [[http://www.obitko.com/tutorials/ontologies-semantic-web/translation-to-fopl.html|Translation to FOPL]] | ||
| - | * [[http://www.obitko.com/tutorials/ontologies-semantic-web/reasoning.html|Reasoning]] | ||
| - | |||
| - | * [[http://www.inf.unibz.it/~franconi/dl/course/dlhb/dlhb-01.pdf|Introduction to DL]] (handbook) | ||
| - | |||
| - | ==== Kursy ==== | ||
| - | * [[http://www.inf.unibz.it/~franconi/dl/course/|DL Course]] by Enrico Franconi | ||
| - | * [[http://www.cs.man.ac.uk/~horrocks/Teaching/cs646/|by I.Horrocks]] | ||
| - | * Lectures: | ||
| - | * {{http://www.cs.man.ac.uk/%7Ehorrocks/Teaching/cs646/Slides/pt2-dlintro.pdf|Intro to DL}} | ||
| - | * {{http://www.cs.man.ac.uk/%7Ehorrocks/Teaching/cs646/Slides/pt3-dlreasoning.pdf|DL reasoning}} | ||
| - | * Labs: | ||
| - | * DL reasoning: [[http://www.cs.man.ac.uk/~horrocks/Teaching/cs646/Labs/dlreasoning/|HTML]], {{http://www.cs.man.ac.uk/~horrocks/Teaching/cs646/Labs/dlreasoning.pdf|PDF}} | ||
| - | * [[http://www.cs.man.ac.uk/%7Ehorrocks/Teaching/cs646/Exams/dlreasoning2/|Exam]] - zadania z DL | ||
| - | * [[http://www.cs.man.ac.uk/~rector/modules/CS646/|Rector]] | ||
| - | * Lectures: [[http://www.cs.man.ac.uk/~rector/modules/CS646/Lecture-Handouts/|Handouts]] | ||
| - | * Lab: [[http://www.cs.man.ac.uk/~rector/modules/CS646/Lab-Handouts/|Handouts]] | ||
| - | * [[http://www.dcs.bbk.ac.uk/~michael/sw/sw.html|SemWeb course in London]], 2012 | ||
| - | |||
| - | ==== Narzędzia ==== | ||
| - | * [[http://www.cs.man.ac.uk/~horrocks/FaCT/|FaCT]] | ||
| - | * [[http://www.sts.tu-harburg.de/%7Er.f.moeller/racer/|Racer]] | ||
| - | * [[http://www.sts.tu-harburg.de/%7Er.f.moeller/racer/Racer-1-9-2-beta-Release-Notes/release-notes-1-9-2se3.html#x4-70003.2|RacerPorter]] GUI | ||
| - | * [[http://blipkit.wordpress.com/2010/11/27/posh-the-prolog-owl-shell/|POSH: the prolog OWL shell]] | ||
| - | * [[http://code.google.com/p/dlmodel/|DL model]] | ||
| - | * [[http://db-tom.cs.uwaterloo.ca/AssertionRetrieval/pages/kbgen.jsp|CARE]] - online | ||
| - | * [[http://www.cs.man.ac.uk/~sattler/reasoners.html|More reasoners]] | ||
