A family of logics describing classes of individuals and relationships between individuals, with restricted constructors chosen to support reasoning.
The assumption that distinct individual names denote distinct domain elements. Standard ALC semantics does not impose it; Herbrand interpretations do treat distinct ground terms as distinct elements.
A description logic concept is satisfiable with respect to a TBox if some model of that TBox interprets the concept as a nonempty set.
A rule-oriented description logic fragment designed for translation to function-free Horn rules, allowing constraints but excluding existential witness generation in rule conclusions. In an equivalence, each direction must meet the relevant restrictions. [ref]
The description logic generated by atomic concepts, , conjunction and existential restrictions. Some conventions also allow ; that extension is distinguished here as EL with bottom. Without , every concept is satisfiable with respect to every EL TBox.
EL extended with , allowing disjointness and unsatisfiable concepts. Concept satisfiability with respect to general TBoxes is P-complete.
The description logic with atomic concepts, top and bottom, Boolean concept constructors, and existential and universal restrictions on description logic roles.
A concept satisfiability procedure that expands concept labels into a graph, branches on disjunctions, creates witnesses for existential restrictions, propagates universal restrictions along existing edges, and tests for a tableau clash. General TBoxes require global constraints and a termination device such as direct blocking in description logic.
A test that stops further witness generation at a node when an appropriate earlier ancestor already represents its required pattern of labels. The exact test depends on the logic and tableau calculus. An isolated root has no ancestor and is not directly blocked.
An explicit contradiction in a node label, such as both and , or . Opposite universal restrictions alone cause no clash when there are no successors.
A collection of terminological axioms, including general concept inclusions, constraining the meanings of description logic concepts and description logic roles.
Rewriting suitable general axioms into definitions or primitive inclusions that can be processed when an atomic label is encountered. For example, can be absorbed as .
Substitution of acyclic concept definitions into expressions to be tested. Primitive inclusions require care: can be represented using a fresh name by , but is not equivalent to .
An axiom requiring every instance of the description logic concept to be an instance of . It holds throughout the domain, not just at named individuals.
A unary description interpreted as a subset of the domain. Atomic names can be combined using the constructors of the chosen description logic.
Articles by others on the same topic
Description Logic (DL) is a family of formal knowledge representation languages that are primarily used to represent structured knowledge about the world. It is a subset of first-order logic, designed to provide a more expressive yet computationally manageable framework for reasoning about concepts (also known as classes or types) and relationships between them. ### Key Features of Description Logic: 1. **Concepts**: Represented as unary predicates, concepts define classes of objects. For example, "Person" or "Animal".