184 Foundations of Semantic Web Technologies
• Subsumption. K |= C v D if and only if K ∪ {(C u ¬D)(a)} is unsatis-
fiable, where a is a new individual not occurring in K.
• Class equivalence. K |= C ≡ D if and only if we have K |= C v D and
K |= D v C.
• Class disjointness. K |= C u D v ⊥ if and only if K ∪ {(C u D)(a)} is
unsatisfiable, where a is a new individual not occurring in K.
• Global consistency. K is globally consistent if it has a mo del.
• Class consistency. K |= C v ⊥ if and only if K ∪{C(a)} is unsatisfiable,
where a is a new individual not occurring in K.
• Instance checking. K |= C(a) if and only if K ∪ {¬C(a)} is unsatisfiable
• Instance retrieval. To find all individuals belonging to a class C, we
have to check for all individuals a whether ...