EL Description Logic

Origin. Baader et al. (2005). Tractable description logic. Polynomial reasoning. SNOMED CT. Foundation of efficient ontology.

Models. Existential restrictions only. Polynomial subsumption. Tractable classification. Large-scale ontologies.

Formalism.

Constructors: ⊤: top concept. A: atomic concept. C ⊓ D: conjunction. ∃r.C: existential restriction. No negation, disjunction, universal.

TBox: C ⊑ D: concept inclusion. C ≡ D: equivalence. General TBoxes.

ABox: C(a): concept assertion. r(a, b): role assertion. Individual data.

Semantics: Standard DL interpretation. ∃r.C: has r-successor in C. No negation = monotonic.

Subsumption: C ⊑_T D: C subsumed by D w.r.t. TBox T. Polynomial in EL. P-complete.

Classification: Computing all subsumptions. Tractable. Completion algorithms.

EL++: Adds: ⊥, nominals {a}. Role inclusions: r ∘ s ⊑ t. Still polynomial. SNOMED CT expressible.

SNOMED CT: Medical ontology. ~300,000 concepts. EL-based. Polynomial classification essential.

Limitations vs ALC: No negation ¬C. No universal ∀r.C. No disjunction C ⊔ D. Trades expressivity for tractability.

Symbols.

Metatheory. Polynomial subsumption. Tractable TBox reasoning. Completion algorithms. Expressivity bounds.

Applies to. Biomedical ontologies. Large KBs. Efficient reasoning. SNOMED CT.

Limitations. Limited expressivity. No negation. No disjunction. Not universal.