====== - 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 C^{\mathcal{I}} 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 C^{\mathcal{I}} \subseteq D^{\mathcal{I}} 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 C^{\mathcal{I}} = D^{\mathcal{I}} dla każdego modelu I terminologii T.
- Rozłączność (ang. //disjointness//)
* Dwa pojęcia C i D są //rozłączne// wzg. T. jeżeli C^{\mathcal{I}} \cap D^{\mathcal{I}} = \emptyset dla każdego modelu I terminologii T.
__**Ćwiczenie 6**__
- Wiedząc, że:
* Vegetarian \equiv (\forall eats.(\neg (\exists partOf.Animal))) \sqcap (\forall eats.(\neg Animal)) \sqcap Animal
* Cow \sqsubseteq Vegetarian
* MadCow \equiv \exists eats.(\exists partOf.Sheep \sqcap Brain) \sqcap Cow \\ 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//)
* A \models \alpha 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 ⇔ C \sqcap D zawiera się w ⊥
* np. C zawiera się D ⇔ C \sqcap \neg D 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:
* OldLady \equiv Elderly \sqcap Female \sqcap Person
* OldLady \sqsubseteq \exists hasPet.Animal \sqcap \forall hasPet. Cat
* hasPet(Minnie,Tom), Elderly(Minnie), Female(Minnie) \\ 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: C \sqsubseteq D wtw. gdy wyrażenie C \sqcap \neg D jest niespełnialne.
Schemat działania:
- Start od faktów (aksjomatów ABox)
- Doprowadzenie do normalnej formy negacyjnej (NNF). Jest to forma, w której negacja występuje tylko przd nazwami klas.
- Dekompozycja składniowa z użyciem odpowiednich reguł tzw. //tableaux expansion rules//
- Wnioskowanie o ograniczeniach na elementach modelu
- Stop, kiedy nie można zastosować więcej reguł lub wystąpiła sprzeczność
Proszę zapoznać się szczegółowo z trzema przykładami z ze [[http://www.dcs.bbk.ac.uk/~michael/sw/slides/SW-8.pdf|slajdów]]. Proszę przeczytać strony 22-30.
__**Ć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 '' gdzie '''' jest bazą wiedzy ''people+pets.owl'' umieszczoną w katalogu ''examples/data''.
- Jakie są rezultaty?
- Uruchom ''pellet.sh classify '' 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]]