Definition (Concept Satisfiability). Given concept C and knowledge base K as input, a decision procedure for concept satisfiability with reference to knowledge base K returns “C is satisfiable with reference to K” if there is an interpretation I = (ΔI, ·I) and an element d ∈ I such that I ⊨ K and d ∈ CI, otherwise it returns “C is unsatisfiable with reference to K.”