Odvozování

Odvozování v ontologiích a znalostních bázích je jedním z důvodů, proč musí být specifikace formální. Odvozováním rozumíme vyvozování faktů, které nejsou v ontologii ani ve znalostní bázi explicitně vyjádřeny. Všechny formalismy probírané v této části byly vytvořeny s ohledem na automatické zpracování, ale kvůli svým vlastnostem, jako je rozhodnutelnost nebo výpočetní složitost, případně i kvůli samotné úrovni formálnosti, to není vždy možné. V této části budeme probírat odvozování pouze pro deskripční logiky.

Deskripční logiky vznikly se zaměřením na výpočetně zvládnutelné odvozování. Několik příkladů úloh, které se od odvozovače vyžadují, je následujících.

• Splnitelnost konceptu - určit, zda popis konceptu není rozporný, tj. zda může existovat individuum, které by bylo instancí daného konceptu.
• Subsumpce konceptů - určit, zda koncept C subsumuje koncept D, tj. zda je popis C obecnější než popis D.
• Konzistence ABox vzhledem k TBox - určit, zda individua v ABox neporušují popisy a axiomy uvedené v TBox.
• Ověření individua - ověřit, zda dané individuum je instancí konceptu
• Vyhledání individuí - nalézt všechna individua, která jsou instancemi konceptu
• Realizace individua - nalézt všechny koncepty, do nichž individuum patří, zejména ty nejspecifičtější

Tyto úlohy se po sémantické stránce příliš neliší. Například splnitelnost lze testovat jako subsumpci pomocí ⊥ - koncept je nesplnitelný, pokud nemůže existovat žádné individuum, které by bylo jeho instancí. Pro všechny úlohy postačuje umět ověřovat deduktivní důsledek nebo odvodit všechny deduktivní důsledky teorie. Odvozovač však může pro různé úlohy používat speciální optimalizované algoritmy.

Složitost vybraných DL je uvedena v tabulce níže - všechny logiky v tabulce jsou rozhodnutelné. I když se teoretická složitost může zdát nezvládnutelná, existují optimalizované odvozovače použitelné pro praktické reálné případy.

Příklady složitosti deskripčních logik [DL complexity navigator]

Algoritmy používané v implementovaných odvozovačích pro výpočet subsumpce lze rozdělit do dvou skupin - strukturální a logické. Strukturální algoritmy porovnávají normalizovanou syntaktickou strukturu dvou konceptů. Lze ukázat, že tyto algoritmy jsou korektní, mají však problémy s úplností, zejména při použití expresivnějších logik. Kvůli tomuto problému se dnes téměř výhradně používají logické algoritmy. Logické algoritmy ověřují subsumpci C⊑D ověřením, že $C⊓¬D není splnitelné. Existují různé přístupy, jak to ověřit, včetně překladu dotazu do existujícího odvozovače predikátové logiky. Nejrozšířenějším přístupem je tableau algoritmus.

Tableau algoritmus se snaží prokázat splnitelnost konceptu C tím, že konstruuje model, interpretaci I, v níž D^I není prázdné. Tableau je graf reprezentující takový model. V grafu tableau odpovídají uzly individuím a hrany odpovídají vztahům mezi individui (prvkům Δ^IxΔ^I). Algoritmus začíná s individuem splňujícím D a aplikuje rozšiřující pravidla, dokud buď nejsou možné další inference, nebo dokud není nalezen rozpor. Rozšiřující pravidla jsou specifická pro konkrétní deskripční logiku a skládají se ze dvou částí. Hlava pravidla stanovuje podmínky pro použití pravidla a tělo pravidla určuje, jak tableau rozšířit. Podrobnosti a další techniky optimalizace výkonu viz opět The Description Logic Handbook.