Description Logics and OWL
Introduction
Headspace Sprockets’ natural language processing technology is based on a sophisticated use of lexicons and ontologies. Ontologies are curated using the Headspace Sprockets Astonish tool and are typically derived from multiple sources such as MeSH, WordNet, UMLS extracts, and OBO ontologies including GO and ChEBI. The distribution formats and presentation styles of lexicons and ontologies vary widely. Very roughly, ontologies tend to be organized as frames, semantic nets, or encoded axioms and assertions. And very roughly, framelike visualizations are most comprehensible by people while encoded axioms and assertions are most closely matched to automated reasoning mechanisms.
Description Logic engines enable the construction of many types of intelligent software agents to act on behalf of people. The most important agent behaviors are automatic classification of knowledge (particularly incrementally learned), translation of one organization of knowledge to another organization, and negotiation of protocols and services provided by different programs or data sources. A core enabling operation of many agents is the ability to create semantic metadata of documents (and other media) and combine knowledge from that metadata in ways that are meaningful to automated processes. For this to happen, ontologies play a key role as a source of precisely defined and related terms (vocabulary) that can be shared across applications (and humans). DL technology formalizes ontology construction and use by providing a decidable fragment of First Order Logic (FOL)[i]. This formality and regularity enables machine understanding for the support of agentagent communication, semanticbased searches, and provide richer service descriptions that can be interpreted by intelligent agents.
Most ontologies and lexicons when curated by hand only encode direct relationships. Indirect relationships including subsumption may be inferred from direct relationships and from assertions governing role transitivity and propagation. For example, an ontology that encodes “partof” relations may be composed of statements that are direct relationships such as “a spark plug is part of an engine” and “an engine is part of a car.” The indirect relationship formed through transitivity of “part of” is “a spark plug is part of a car.” In the course of inferring indirect relationships, a reasoning algorithm may also determine that contradictions and equivalences exist.
Reasoning using DLs may be applied to general knowledge representation and reasoning problems but may also be used for narrower “Semantic Extract, Transform, and Load” (SETL) processing. As an example, some NLP processes used by Headspace Sprockets require all relevant “broader than” relationships to be materialized. “Broader than” includes ordinary subsumption (“is a”) and possibly other relationships such as “part of” and “caused by”. The use of “broader than” instead of “is a” may create concept equivalences (i.e., equivalence classes of concepts) through definitional cycles. Headspace Sprockets uses a moderately expressive Description Logic for this processing. This DL is designated as EL++ which corresponds to a wellknown fragment of the proposed W3C OWL 2 standard.
This chapter addresses ontologylevel processing rather than lexical processing. That is, the current discussion describes inference techniques, tools, and data formats that are in common to any ontology or lexicon under management without regard to linguistic issues. Linguistic technology is addressed in later chapters.
The latest drafts of the OWL 2 proposed standard are at: http://www.w3.org/2007/OWL/wiki/Syntax.
Below is a schematic of the ontology import and inference process that has been developed by Headspace Sprockets.
OWL
OWL (http://www.w3.org/2007/OWL/wiki/OWL_Working_Group), the successor to DAML+OIL (www.daml.org), appears to be the blessed DL language of the Semantic Web (www.semanticweb.org). It extends and improves upon XMLbased schema languages such as RDFS.
OWL has evolved. OWL 1 (c. 2004) reflects DL research that is more directed to the exploration of the relative expressiveness and computational tractability of different logics than to applications. Three “species” of OWL 1 are defined OWL Full, OWL DL, and OWL Lite. However, for a variety of reasons none of these gained wide acceptance or use.
Proposals for a more expressive DL than OWL DL (but less than the undecidable OWL Full) are aimed at the needs of applications as well as the state of the art of the technology. The proposals have been called OWL 1.1, although the W3C designation will be OWL 2. OWL 2 reflects a recognition that more complex inferences involving relationships (such as propagation of one relationship through another[ii]) is necessary, along with other improvements.
An OWL 2 knowledge base is a collection of:
 Entities, naming classes (concepts), properties, and individuals;
 Expressions, providing descriptions (definitions) which characterize, for example, all of the features of individuals that must be present for membership in a class; and
 Axioms which assert domain truths, such as membership of a particular individual in a particular class.
The semantics of OWL 2 are precisely and rigorously defined which enables predictable inferences to be drawn from a properly implemented reasoning algorithm.
OWL 2 divides a domain into two disjoint parts. One part consists of the values that belong to XML Schema datatypes. These are called the concrete datatypes. The other part consists of (individual) objects that are considered to be members of classes described within OWL (or RDF). These are called the abstract datatypes.
Reasoning over concrete datatypes is essentially composed of straightforward interval or set intersections (along with some other simple settheoretic operations). OWL 2 defines a very rich set of concrete datatypes and is very appropriate for many applications. It does not attempt to support more specialized reasoning over concrete types such as constraintbased solving (for example, linear programming) or applicationspecific problem solving (for example, temporal logics for planning and scheduling). OWL 2 abstract datatypes are used for the creation of classes, properties, and individuals that describe (or define) the object domain.
Basic DL Operations
Operations that are most apparent to users of DL systems are classification and coherence checking. Classification is the generation of concept taxa. Coherence checking determines those concept names which are unsatisfiable.
The most fundamental operations applied to a knowledge base O are:
Consistency – check if knowledge is meaningful
 Is O consistent? There exists some model I of O
 Is C consistent? C^{I} ≠ ∅ in some model I of O
Subsumption – structure knowledge, compute taxonomy
 C ⊑_{O} D? C^{I} ⊆ D^{I} in all models I of O
Equivalence – check if two classes denote the same set of instances
 C ≡_{ O} D? C^{I} ⊆ D^{I} in all models I of O
Instantiation – check if individual I is an instance of class C
 i ∈_{ O} C? i ∈ C^{I} in all models I of O
Retrieval – retrieve the set of individuals that instantiate C
 i ∈_{ O} C? i ∈ C^{I} in all models I of O
In addition, other operations are supported within this framework of basic operations including “whatif” queries, explanation of reasoning justifications, and nonstandard inferences such as most specific common subsumer and match determination. Many operations may be reduced to sets of consistency (and satisfiability) tests.
The Description Logic EL++
The W3C OWL 2 proposal specifies the syntax and semantics for knowledge base representation and reasoning based on the logic SROIQ. Because this logic is as yet primarily researchoriented, has no currently available commercialquality implementations, and is more expressive than often required for applications, the standard defines several fragments of the full SROIQ. The most important and expressive of these fragments is EL++. EL++ is in the worstcase tractable  full classification is performed in polynomial time – and is very fast in practical applications.
This logic is described in the papers:
Baader, Brandt, and Lutz in the LTCSReport "Pushing the EL Envelope" and
Baader, Lutz, Suntisrivaraporn, "Is Tractable Reasoning in Extensions of the Description Logic EL Useful in Practice?"
Headspace Sprocketshas implemented the only commercialquality EL++ system to date.
Headspace Sprockets’ EL++ can be used to solve various reasoning problems using large ontologies including GO, SNOMEDCT, MeSH (to the extent it may be viewed as an ontology!) and WordNet. These ontologies include:
huge numbers of concepts,
complex descriptions and relationships,
primacy of classification and of term hierarchies,
rich interactions and propagations of role relationships, and
the ability to be applied in many ways including as the basis for semantic indexing.
Ontologies undergo frequent revisions. Some form of version control or change propagation is required for serious applications.
An example simple ontology (from Baader, Lutz, Suntisrivaraporn, cited above) illustrates the style of assertions (without the usual syntactic or model theoretic trappings). It is reproduced here:
The first assertion may be informally read[iii] as “Pericardium is a Tissue and is contained in the Heart.” The last assertion is interpreted as “if X has location Y and Y is contained in Z then X has location Z.”
From this set of assertions we can infer (with EL++ or by simple inspection) that 'Pericarditis' is classified as 'Heart_disease' and that 'Pericarditis' is related via 'hasstate' to 'NeedsTreatment'.
While the formal language used by DLs seems stilted, they provide the basis for largescale knowledge representation and reasoning.
{ N.B. The remainder of this Chapter is a brief and technical introduction to the logic conventions of Description Logics and for the approaches taken for the implementation of DLs by Headspace Sprockets. }
Basic Terms and Identities
Tarskistyle semantics are usually used to define the semantics of DL languages. In the discussion below, I assume that the reader has some familiarity with such things – the equivalent of an introductory course in formal logic suffices. Symbols and notation will generally be defined as needed. To introduce the typography used in here, a few are listed below.
Symbol 
Term 
⊤ 
“Top” or “Thing” 
⊥ 
“Bottom” 
⊓ 
“Meet” 
⊔ 
“Join” 
⊑ 
“is subsumed by”, in the DL sense; “is a specialization of” 
The reasoning algorithms used by DLs, including tableau methods, depend on determining satisfiability. Recall:
 C ⊑ D iff C ⊓ ØD is unsatisfiable (w. r. t. the controlling terminology, etc.)
C is unsatisfiable iff C ⊑ A ⊓ ØA for some concept name A. (Equivalently, iff C is not subsumed by ⊥.) Number restrictions may also cause a concept to be unsatisfiable.
Some common identities follow.
 Ø⊤ ≡ ⊥
 Ø⊥ ≡ ⊤
 ∃R.⊥ ≡ ⊥
 ∀R.⊤ ≡ ⊤
 C ⊓ D ≡ Ø(ØC ⊔ ØD)
 C ⊔ D ≡ Ø(ØC ⊓ ØD)
 Ø ØC ≡ C
 ∀R.C ≡ Ø ∃R. ØC
 ∃R.C ≡ Ø ∀R.ØC
 Ø ≤n R.C ≡ ≥(n+1 ) R.C
 Ø ≥n R.C ≡ ≤(n1) R.C if n > 0, else ⊥
The following table summarizes the most important constructors defined in description logics and having syntactic variants in OWL 2. Actual usage of OWL 2 also includes header, version, import, annotation, and other constructors and axioms and, like other XML applications, can be verbose.
Constructor 
DL Syntax 
Prolog Syntax 
Example 
IntersectionOf 
C_{1} ⊓ … ⊓ C_{n} 
[C1, C2,…,Cn] 
Human ⊓ Male 
UnionOf 
C_{1} ⊔… ⊔ C_{n} 
or([C1,…,Cn]) 
Dog ⊔ Cat 
ComplementOf 
Ø C 
not(C) 
5 Living 
OneOf 
{x_{1}, …, x_{n}} 
oneOf([C1,…,Cn]) 
{paul, jim} 
AllValuesFrom 
∀ R.C 
all(R, C) 
∀makes.Product 
SomeValuesFrom 
∃ R.C 
exists(R, C) 
∃ kid.Girl 
HasValue 
∃ R.{x} 
exists(R, oneOf([C])) 
∃ kid.{missy} 
MinCardinality 
≥n R.C 
min(N,R,C) 
≥2 kid.Girl 
MaxCardinality 
≤n R.C 
max(N,R,C) 
≤2 kid.Girl 
ExactCardinality 
=n R.C 
equ(N,R,C) 
=2 kid.Girl 
Notes:
 ‘OneOf’ and ‘HasValue’ introduce individuals (nominals) into concept definitions which increase computational and implementation complexity.
 Concrete datatype constructors are not listed above but are discussed below.
The following table summarizes the most important types of axioms defined in description logics and having syntactic variants in OWL 2.
Axiom 
DL Syntax 
Prolog Syntax 
Example 
SubClassOf 
C_{1} ⊑ C_{2} 
subC(C1,C2) 

EquivalentClasses 
C_{1} ≐ C_{2} 
equC(C1,C2) 

SubPropertyOf 
P_{1} ⊑ P_{2} 
subR(P1,P2) 

SamePropertyAs 
P_{1} ≐ P_{2} 
equR(P1,P2) 

DisjointClasses 
C_{1} ⊑ Ø C_{2} 
subC(C1,not(C2)) 

SameIndividual 
{x_{1}} ≐ {x_{2}} 


DifferentIndividuals 
{x_{1}} ⊑ Ø{x_{2}} 


inverseOf 
P_{1} ≐ P_{2}^{} 
inv(P1,P2) 

transitiveProperty 
P^{+} ⊑ P 
trans(P) 

uniqueProperty 
⊤ ⊑ ≤1P 


unambiguousProperty 
⊤ ⊑ ≤1P^{} 


OWL 2 provides a knowledge description and interchange format. It specifies semantics that apply to automated reasoning systems. It does not address the many issues concerning the operation of a knowledgebased system including indexing, knowledge revision, transaction processing, querying, and administration.
Classes of Description Logics
Many DLs have been defined and their complexity has been explored. Some of the complexity results are surprising and the proofs are quite technical. There are tradeoffs that must be evaluated in the light of the actual applications contemplated for the DL. Hybrid approaches will be more common in the future as techniques are developed to decompose problems into subproblems that require differing forms of reasoning. Headspace Sprockets already has taken steps towards this approach in its support of different reasoners and indexing mechanisms.
SROIQ^{(D)} is the designation for the particular description logic that OWL 2 proposes and that Headspace Sprockets will completely implement in the future (we have implemented fully EL++ and have a partial implementation of SROIQ^{(D)}.)
Description Logics are named on the basis of features which give them their expressiveness. In short, SROIQ^{(D)} means:
 S – Concepts are composed of intersection, universal restrictions, simple existential quantification (∃ R.C), and complex negation (which then implies union).
 R – Role hierarchies and complex role inclusion axioms (limited by certain restrictions to guarantee decidability) of the forms R ° S ⊑ R and S ° R ⊑ R. This means that role transitivity is also supported (R ° R ⊑ R).
 O – Support for nominals (oneOf and hasValue).
 I – Role inverses.
 Q – Quantified role restrictions.
 (D) – Concrete data type support.
DL Definitions and Formalities
Introduction
SROIQ^{(D)} is based on the extension of the well known DL ALC to include transitively closed primitive roles, role hierarchies and complex role inclusions (R), nominal support (O), inverse roles (I), and qualifying number restrictions (Q). For brevity, DL practitioners named ALC plus transitively closed primitive roles S after the modal logic S4_{(m)}.
Tarskistyle semantics are used to describe DLs.
Let R be a set of role names with both transitive and normal role names R_{+} ⋃ R_{P} = R, where
R_{+} ∩ R_{P} = ∅. The set of SROIQroles is R ⋃ { R ^{}  R ∈ R }. In some DLs we would also define a third disjoint set of role names: the functional role names. SROIQroles do not define functional role names.
A role inclusion axiom is of the form R ⊑ S, for two SHIQroles R and S. A role hierarchy is a set of role inclusion axioms. A complex role inclusion is of the form S ° R ⊑ S or R ° S ⊑ S, for two SROIQroles R and S. Certain restrictions are required on the set of complex role inclusions to ensure tractability. For details, refer to Horrocks, et al., The Even More Irresistible SROIQ.
An interpretation I = (Δ^{I},.^{I} ) consists of a set Δ^{I}, called the domain of I and a function .^{I} which maps every role to a subset of Δ^{I} xΔ^{I} such that, for P ∈ R and R ∈ R_{+},
<x,y> ∈ P ^{I} iff <y,x> ∈ P ^{}^{I}, and
if <x,y> ∈ R ^{I} and <y,z> ∈ R ^{I} then <x,z> ∈ R ^{I}.
An interpretation I satisfies a role hierarchy R iff R ^{I} ⊑ S ^{I} for each R ⊑ S ∈ R ; Such an interpretation is called a model of R.
We introduce some notation to make the following considerations easier.
The inverse relation on roles is symmetric, and to avoid considering roles such as R^{}, we define a function Inv which returns the inverse of a role:
Inv(R) := R ^{} if R is a role name, or S ^{} if R = S for a role name S.
Since set inclusion is transitive and R ^{I} ⊑ S ^{I} implies Inv(R ^{I}) ⊑ Inv(S ^{I}), for a role hierarchy R, we introduce ⊑∗ as the transitivereflexive closure of ⊑ on R ⋃ { Inv(R) ⊑ Inv(S)  R ⊑ S ∈ R }. We use R ≐ S as an abbreviation for R ⊑∗ S and S ⊑∗ R.
Obviously, a role R is transitive iff its inverse Inv(R) is transitive. However, in cyclic cases such as R ≐ S, S is transitive if R or Inv(R) is a transitive role name. In order to avoid these case distinctions, the function Trans returns true iff R is a transitive role – regardless whether it is a role name, the inverse of a role name, or equivalent to a transitive role name or its inverse: Trans(R) := true if, for some S with S ≐ R, S ∈ R_{+} or Inv(S) ∈ R_{+}, and false otherwise.
A role R is called simple w.r.t. R iff not Trans(S) for each S ⊑∗ R. (Similar definitions and assertions are provided for those DLs that support functional role names).
Comments.
Most implemented systems for SH logics (e.g. SHIQ) reject cycles within sets of role axioms. The more general mechanism used for role inclusion axiom and role hierarchy processing used for SRIQ and SROIQ can and reduce role definitional cycles to equivalences.
One complication persists. Clearly, a role hierarchy R and the role hierarchy R ^{} formed by the inverses of each role in R are isomorphic. Suppose that a role hierarchy is defined with axioms that are drawn from both R and R ^{} ? These must be reconciled. This is why Inv and Trans were defined the way they were.
This discussion has not yet addressed some of the implementation issues for SROIQ. Refer to the paper by Horrocks, et al. for further information.
Concrete Roles.
A simple interval system is essentially a unary datatype system. The proposal for SHOQ(D) lacks formula calculations.
Concrete role extensions based on nary predicates have been proposed by Pan (and Horrocks) and by Haarslev, et al. These seem to me to be useful (and sometimes necessary) for many realistic applications. Further, with nary predicates, there may be some ability to define interesting predicates over different kinds of concrete roles (say, text and numeric).
In any case, the formalization of domains also allows for units of measure to be incorporated and conversions to be automatically performed (say, pounds to kilograms).
There is a general notion of “admissibility” (or “conforming”) which holds iff (i) the set of predicate names is closed under negation and contains a name y _{D} for )_{D} and (ii) the satisfiability problem for an expression of the form P_{1}^{D} Ç … Ç P_{n}^{D} is decidable. Using finite state autonoma, regular expressions can be used as predicates over textual or symbolic domains.
A proposal for a restricted form of functional roles is described in “The Description Logic ALCNH_{R+} Extended with Concrete Domains: A Practically Motivated Approach” by Haarslev, Moller, and Wessel. This is much further extended in “Practical Reasoning in Racer with a Concrete Domain for Linear Inequations” by Haarslev and Moller.
This proposal uses a criterion for admissible absorptions that detects “harmful” feature chains.
Concepts.
Let N_{C} be a set of concept names. The set of SHIQ–concepts is the smallest set such that
Every concept name C ∈ N_{C} is a concept,
If C and D are concepts and R is a SHIQ–role, then ( C ⊓ D ), ( C ⊔ D ), (Ø C ), ( ∀R.C ), and
( ∃R.C ), and
If C is a concept, R is a simple SHIQ–role and n ∈ ℕ, then ( ≤nR.C ) and ( ≥nR.C ) are concepts.
A general concept inclusion (GCI) is an expression of the form C_{1} ⊑ C_{2} for SHIQ–concepts C_{1} and C_{2}. A terminology (or TBox) is a set of GCIs.
The interpretation function .^{I} of an interpretation I = (Δ^{I},.^{I} ) maps, additionally, every concept to a subset of Δ^{I} such that
 ( C ⊓ D )^{I} = C^{I} ∩ D^{I},
 ( C ⊔ D )^{I} = C^{I} ⋃ D^{I},
 (Ø C )^{I} = Δ^{I} \ C^{I},
 ( ∃R.C )^{I} = { x ∈ Δ^{I}  There is some y ∈ Δ^{I} with <x,y> ∈ R^{I} and y ∈ C^{I} },
 ( ∀R.C )^{I} = { x ∈ Δ^{I}  For all y ∈ Δ^{I} , if <x,y> ∈ R^{I} then y ∈ C^{I} },
 ( ≤nR.C )^{I} = { x ∈ Δ^{I}  #R^{I}(x,C) ≤ n},
 ( ≥nR.C )^{I} = { x ∈ Δ^{I}  #R^{I}(x,C) ≥ n},
where, for a set M, we denote the cardinality of M by #M and R^{I}(x,C) is defined as { y  <x,y> ∈ R^{I} and y ∈ C^{I} }.
A concept C is called satisfiable with respect to a role hierarchy R iff there is a model I of with C^{I} ≠ ∅. Such an interpretation is called a model of C w.r.t. R . A concept D subsumes a concept D w.r.t. R (written C ⊑_{R} D ) iff C^{I} ⊆ D^{I} holds for every model I of R. Two concepts C, D are equivalent w.r.t. R (written C ≡_{R} D ) iff they are mutually subsuming.
Let R be a role hierarchy and D a SHIQ–concept in NNF. A completion tree w.r.t. R and D is a tree T where each node x of the tree is labeled with a set L(x) ⊆ clos(D) and each edge <x,y> is labeled with a set of role names L(<x,y>) containing (possibly inverse) roles in clos(D). Additionally, we keep track of inequalities between nodes of the tree with a symmetric binary relation ≠.
Given a completion tree, ancestors, successors, etc. are defined as usual. A node y is called an R–successor of a node x if y is a successor of x and S ∈ L(<x,y>) for some S ⊑∗ R, y is called an R–neighbor of x if y is an R–successor of x, or if x is an Inv(R)successor of y.
For a role S, a concept C, and a node x in T, we define S^{T}(x,C) by S^{T}(x,C) := { y  y is S‑neighbor of x and C ∈ L(y) }.
Assertions on Individuals
Assertions take two forms x:C interpreted to mean that named individual x is subsumed by C and r(x,y) which establishes a role relationship between named individuals x and y. The formalities of such are obvious.
For DLs that are closed under negation such as SHIQ, subsumption and satisfiability can be mutually reduced.
C ⊑ D iff C ⊓ Ø D is unsatisfiable.
C is unsatisfiable iff C ⊑ A ⊓ Ø A for some concept name A
C is satisfiable iff the ABox { a:C } is consistent.
Internalization of General Concept Inclusions (GCIs) extends these operations to terminologies.
With a little care, reasoning can be extended to include ABox individuals. The ABox individuals may have arbitrary role relationships between them. Thus, the completion algorithm must operate on a forest instead of a tree; The root nodes of the trees in the forest represent individuals in the ABox.
Using the same techniques and arguments as for TBoxes, general concept inclusion axioms can be internalised for ABoxes. However, as it is not guaranteed that all root nodes will be connected, it is necessary to add the concept C_{T} ⊓ ∀U. C_{T} to the label of every root node when the completion forest is initialized. This is equivalent to adding an assertion a : (C_{T} ⊓ ∀U. C_{T}) to the ABox for every individual a occurring in it. We thus have the following theorem:
Lemma. Let C, D be concepts, A an ABox, T a terminology, and R a role hierarchy. We define
C_{T} := ⊓ ØC_{i} ⊔ D_{i} where the meet is over all C_{i} ⊑ D_{i} ∈ T.
Let U be a transitive role that does not occur in T, C, D, A, or R. We set
R_{U} := R ⋃ ( R ⊑ U, Inv(R) ⊑ U  R occurs in T, C, D, A, or R}.
Then:
 C is satisfiable w.r.t. T and R iff C ⊓ C_{T} ⊓ ∀U.C_{T} is satisfiable w.r.t. R_{U}.
 D subsumes C w.r.t. T and R iff C ⊓ 5D ⊓ C_{T} ⊓ ∀U.C_{T} is unsatisfiable w.r.t. R_{U}.
 A is consistent w.r.t. T and R iff A ⋃ {a:C_{T} ⊓ ∀U.C_{T}  a occurs in A} is consistent w.r.t. R_{U}.
A design choice is whether the unique individual assumption is made for ABox assertions; Headspace Sprockets’ implementation of EL++ makes the unique individual assumption.
Implementing DLs
The implementation of Description Logics broadly follows three different strategies.
 Structural – reasoning based inference rules that directly compare descriptions for subsumption and add assertions that match directly testable conditions
 Tableau – reasoning based on proof tree expansion rules
 Automata – reasoning based on compiled FSAs
Active Knowledge Studio employs a combination of structural and tableau reasoning.
Tableau Expansion Rules
Active Knowledge Studio uses tableau expansion rules that are compatible with the sophisticated blocking strategy for dealing with terminological cycles, nonchronological backtracking, concrete domains, and ABox axioms. These expansion rules are based on all concepts transformed to a Lexical Normal Form (LNF) which enables efficiently identification of equivalent concept subexpressions.
The expansion rules create a tree structure that branches at choice points such as those created by disjunction within descriptions. The tree structure reflects the search that is required for determination of consistency (satisfiability).
Control Strategies.
Of course, rules only make sense when embedded within a control mechanism. In the case of tableau rules, the control mechanism includes:
 Metarules that govern the order of application of rules
 Blocking strategies that close redundant expansions that are created by cyclic definitions
 Nonchronological backtracking or backjumping search strategies
Much of the control over reasoning is derived from constraint propagation methods similar to or including SAT solving and integer programming. These are topics of the chapter on Constraint Satisfaction and Optimization.
[i] It would be possible to create an undecidable description logic, but most DL researchers strive to create logics that are not only decidable but are tractable (for all or typical cases).
[ii] For example, “owns” propagates through “partof” as in, if I own something, then I own each of that thing’s parts.
[iii] A little more formally read as “An X which is an instance of Pericardium is necessarily an instance of Tissue and has a relationship ‘containedin’ which has a value Y which is an instance of Heart. (Pericardium and Heart each being concepts.)