Definition (Concept Subsumption). Given C and D concepts and K knowledge base as input, a decision procedure for concept subsumption with reference to a knowledge base returns “D subsumes C with reference to K” if there is no interpretation I = (ΔI, ·I) such that I ⊨ K and there is an element d ∈ ΔI, d ∈ CI, and d ∈ (¬D)I, otherwise it returns “D does not subsume C with reference to K.”