Current Slide

Small screen detected. You are viewing the mobile version of SlideWiki. If you wish to edit slides you will need to use a larger device.

Description Logic - Reasoning

  • Reasoning Task are typically reduced to KB satisfiability sat(A) w.r.t. to a knowledge base A

    • Instance checking : instance(a,C, A) ⇔¬sat(A ⋃ {a: ¬ C})

    • Concept satisfiability : csat(C) ⇔ sat(A ⋃ {a: ¬ C})

    • Concept subsumption : B ⊑ A ⇔ A ⋃ {¬B ⊓ C} is not satisfiable ⇔ ¬sat(A ⋃ {¬B ⊓ C})

    • Retrieval : Instance checking for each instance in the Abox

  • Note: Reduction of reasoning tasks to one another in polynomial time only in propositionally closed logics

  • DL reasoners typically employ tableaux algorithms to check satisfiability of a knowledge base

Speaker notes:

Content Tools


There are currently no sources for this slide.