Różnice
Różnice między wybraną wersją a wersją aktualną.
Nowa wersja
|
Poprzednia wersja
|
pl:dydaktyka:krr:lab_dl_reasoning [2016/06/08 01:36] msl utworzono |
pl:dydaktyka:krr:lab_dl_reasoning [2019/06/27 15:50] (aktualna) |
Schemat działania: | Schemat działania: |
- Start od faktów (aksjomatów ABox) | - 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// | - 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 | - Wnioskowanie o ograniczeniach na elementach modelu |
- Stop, kiedy nie można zastosować więcej reguł lub wystąpiła sprzeczność | - 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): | __**Ćwiczenie 8**__ (dla chętnych): |
- ¬C ⊓ ∃R.C ⊓ ∀R.(¬C ⊔ ∃R.C) | - ¬C ⊓ ∃R.C ⊓ ∀R.(¬C ⊔ ∃R.C) |
- A ⊓ ∀R.A ⊓ ∀R.¬∃P.A ⊓ ∃R.∃P.A | - A ⊓ ∀R.A ⊓ ∀R.¬∃P.A ⊓ ∃R.∃P.A |
Przykładowe rozwiązania z użyciem algorytmu tableau: [[http://www.dcs.bbk.ac.uk/~michael/sw/slides/Sew11-8-tut.pdf|tutaj]]. | |
| |
| |