Description logic

DL foundations, triple mapping, reasoning tasks, TBox/ABox — and deriver.app scope

This chapter follows the structure of the canonical TAoKE text (see also the older Logic / DL entry point). The focus is how Description Logic (DL) strength can be combined with ontology-centric production rules and triple stores: (1) how DL-style knowledge maps to triples and quadruples, and (2) which reasoning-like services are suggested in connection with an ontological query language (OQL on taoke.de). Database-backed storage offers multi-user, transactional, distributed access and avoids the in-memory limits of many classical DL implementations [BaNu2003]; OWL-oriented practice is summarised in [AlHe2020].

deriver.app is not a full DL reasoner: it provides explicit triple storage and a rule engine with JSON APIs. Use this chapter to align vocabulary and expectations when you integrate or export to external OWL/DL tools.

1. Reasoning — subsumption, satisfiability, implementation approaches
2. Kinships — DL expressions and triple encoding (examples from [BaNu2003])
3. Defining DL axioms with reification
4. Using reification to represent DL expressions
5. Predicate logic and TBox
6. ABox
7. Concept expressions and GCI
8. Attribute implications and FCA
9. Further mirror pages: DL related work, DL discussion (OWA/CWA), DL axioms (Body-of-Water examples)

If concept D is more general than concept C, one writes C ⊑ D (subsumption): C is the subsumee, D the subsumer. A basic task is to decide subsumption between concept expressions. Concept satisfiability asks whether a concept can denote a non-empty set. Structural comparison via labelled graphs can suggest generality, but a “false” structural answer need not match logical entailment when the algorithm is incomplete.

A recurring theme is the expressiveness vs. tractability trade-off: richer DL fragments typically make standard reasoning tasks harder. Implementations often fall into: (1) limited + complete — restrict constructs so subsumption stays efficient (e.g. CLASSIC-style systems); (2) expressive + incomplete — expressive languages with incomplete algorithms (e.g. historical LOOM/BACK); (3) expressive + complete — tableau and related methods for expressive DLs (e.g. early FACT, modern OWL DL reasoners). Usability requires intuitive syntax and clear intended semantics [BaNu2003].

The canonical text rewrites a small kinship-style conceptual model (cf. Fig. “DL CM01” on taoke.de) with name substitutions such as Person → ^Human, hasChild → ◊Child, etc. Typical concept expressions include intersection (⊓), negation (¬), existential (∃R.C), and universal (∀R.C) restrictions, e.g.:

1. Person ⊓ Female
2. Person ⊓ ¬Female
3. Person ⊓ ∃hasChild.⊤
4. Person ⊓ ∀hasChild.Female — what if a person has no children? (open-world nuance)
5. Person ⊓ ∀hasChild.⊥

Unary predicates (concept assertions) and binary predicates (role assertions) translate to triples, e.g. Father(PETER) ↔ (>Peter, ◊isi, ^Father), hasChild(MARY, PETER) ↔ (>Mary, ◊Child, >Peter), with inverse roles where needed. See [NaBr2003] for terminology (concepts, terminology, network-based representations).

Concept definitions such as Woman ≡ Person ⊓ Female, Mother ≡ Woman ⊓ ∃hasChild.Person, etc. can be stored using reification: ternary patterns that attach subject/relation/object to a reified node (figures “dl-man1”, “dl-man2” on taoke.de). A definition like Man ≡ Male ⊓ Human can be decomposed into triples over a reified axiom node; more complex expressions may use a reduced binary-tree style encoding so that every DL expression can also be mapped to a discrete encoding (as in the original treatise).

Arbitrary DL expressions are not stored “raw” in the graph: they are reified. Quantified roles (∃, ∀) can be wrapped with dedicated reificators (canonical notation uses symbols such as ≡∃Child, ≡∀Child with τ-mappings). Number restrictions on roles (≤, ≥) appear in axioms such as “at most one child or at least three children with a female child” — the mirror on taoke.de spells out the expanded normal forms.

A TBox collects concept definitions and inclusions. Equivalence definitions fix the meaning of concept names; cyclic definitions require fixed-point or descriptive semantics in expressive DLs. General concept inclusions (GCIs) C ⊑ D generalise “definition” by allowing arbitrary concept expressions on both sides (with syntactic restrictions depending on the profile). Only one definition per concept name is typical in acyclic TBoxes; expansion and cyclic dependencies are treated carefully in the literature [BaNu2003].

The canonical page discusses “who is female?” using domain/range constraints on roles and data attributes (e.g. .Gender=female) alongside class-level axioms.

The ABox stores assertional facts: concept assertions C(a) and role assertions r(a,b) (without complex role expressions in assertions in the basic setting). From Female ⊓ Person on an individual and a definition of Woman, one may infer membership in Woman. Triples such as (>MARY, ◊isi, ^Person) play the same role.

Core reasoning tasks include instance checking, consistency of the knowledge base, realisation (most specific concept for an individual), and retrieval (instances of a concept). On taoke.de these are related to OQL-style queries over the ontology store.

Concept expressions are built from concept names, ⊤, ⊥, nominals {a₁,…,aₙ}, Boolean combinations (¬, ⊓, ⊔), existential/universal restrictions ∃r.C, ∀r.C, self restrictions ∃r.Self, and cardinality constraints ≥n r.C, ≤n r.C for simple roles r [Rudo2011].

A general concept inclusion (GCI) has the form C ⊑ D and is also read as a subsumption axiom. These statements populate practical OWL ontologies together with role axioms; see [AlHe2020] for the OWL alignment.

Material on attribute implications and concept lattices in TAoKE relates to Formal Concept Analysis; see [GaWi2024] and the TAoKE page on Attribute implications.