Take a very simple case

• Define the type Ex :

• • the terms are “classes” (A, B, …) and “individuals” (a, b, …)
  • there are two possible relationships between classes:
  • • “subclassing” i.e., A ⊑ B, B ⊑ C, etc., and
    • “equivalence”, i.e. A ≣ B
  • there is one relationship combining individuals to classes: “typing” i.e. a:A, b:A,…

• An example for a universe: the vocabulary: {a, A, B} with the axioms {a:A, A ⊑ B}

• The goal is to define a semantics so that we could infer a:B