Description Logic

A Formal System for talking about collections of objects and their relations. It is at least as expressive as Propositional Logic with set-theoretic semantics, and it offers

• individuals
• relations

It has the following components.

• a formal language $\mathcal{L}$ with logical constants $\sqcap ,\bar{\circ },\bigsqcup ,⊑,\equiv$
• a set-theoretic semantics $⟨\mathcal{D},[[\circ ]]⟩$
  • we get this for free when we can translate into First-Order Predicate Logic
• Translation into First-Order Predicate Logic that is compatible with the set-theoretic semantics
• a Calculus for $\mathcal{L}$ that includes a decision procedure for $\mathcal{L}$ satisfiability
  • to verify we are still in the decidable region of logics

ABox

Closed World Assumption vs. Open World Assumption

TBoxes

TBox Concept Definition