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) |
||
|---|---|---|---|
| Linia 83: | Linia 83: | ||
| 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): | ||
| Linia 99: | Linia 100: | ||
| - ¬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]]. | + | |
