Description Logics and OWL

Originally published on Thu, 04/04/2013 - 11:31 Latest Revision: Tue, 12/24/19 - 10:19

Introduction

Headspace Sprockets' natural language processing technology is in part 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, FrameNet, 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, frame-like 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 enable machine understanding for the support of agent-agent communication, semantic-based 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 "part-of" 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 well-known fragment of the W3C OWL 2 standard.

This chapter addresses ontology-level 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 standard are at: https://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 XML-based 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 set-theoretic 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 constraint-based solving (for example, linear programming) or application-specific 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? $\qquad\qquad$ There exists some model $I$ of $O$.
  • Is $C$ consistent? $\qquad\qquad$ $C^I \ne \text{\o}$ in some model $I$ of $O$.

• Subsumption – structure knowledge, compute taxonomy

  • $C \sqsubseteq_O D$? $\qquad\qquad\qquad$ $C^I \subseteq D^I$ in all models $I$ of $O$.

• Equivalence – check if two classes denote the same set of instances

  • $C \equiv_O D$? $\qquad\qquad\qquad$ $C^I \subseteq D^I$ in all models $I$ of $O$.

• Instantiation – check if individual $I$ is an instance of class $C$

  • $i \in_O C$? $\qquad\qquad\qquad\quad$ $i \in C^I$ in all models $I$ of $O$.

• Retrieval – retrieve the set of individuals that instantiate $C$

  • $i \in_O C$? $\qquad\qquad\qquad\quad$ $i \in C^I$ in all models $I$ of $O$.

In addition,  other operations are supported within this framework of basic operations including "what-if" queries, explanation of reasoning justifications, and non-standard 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 research-oriented, has no currently available commercial-quality 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 worst-case 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 LTCS-Report "Pushing the EL Envelope" and

Baader, Lutz, Suntisrivaraporn, "Is Tractable Reasoning in Extensions of the Description Logic EL Useful in Practice?"

Headspace Sprockets has implemented the only commercial-quality EL++ system to date.

Headspace Sprockets' EL++ can be used to solve various reasoning problems using large ontologies including GO, SNOMED-CT, 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 'has-state' to 'NeedsTreatment'.

While the formal language used by DLs seems stilted, they provide the basis for large-scale knowledge representation and reasoning.

Basic Terms and Identities

Tarski-style 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 here, a few are listed below.

The reasoning algorithms used by DLs, including tableau methods, depend on determining satisfiability.  Recall:

• $C \sqsubseteq D \iff C \sqcap \lnot D$ is unsatisfiable (w. r. t. the controlling terminology, etc.)

• $C$ is unsatisfiable $\iff C \sqsubseteq A \sqcap \lnot A$ for some concept name $A$. (Equivalently, $C$ is satisfiable $\iff C$ is not subsumed by $\bot$.)

• Number restrictions may also cause a concept to be unsatisfiable.

Some common identities follow.

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.

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.

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 knowledge-based 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 trade-offs 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 sub-problems that require differing forms of reasoning.  Headspace Sprockets already has taken steps towards this approach in its support of different reasoners and indexing mechanisms.

$\small \bold{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 $\small SROIQ^{(D)}$.

Description Logics are named on the basis of features which give them their expressiveness.  In short, $\small SROIQ^{(D)}$ means:

• S – Concepts are composed of intersection, universal restrictions, simple existential quantification (\exists 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 \sqsubseteq R and S ° R \sqsubseteq R.  This means that role transitivity is also supported (R ° R \sqsubseteq R).
• O – Support for nominals (oneOf and hasValue).
• I – Role inverses.
• H – Role hierarchy.
• Q – Quantified role restrictions.
• (D) – Concrete data type support.

DL Definitions and Formalities

Introduction

$\small 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 $\bold{S4_{(m)}}$.

Tarski-style semantics are used to describe DLs.

Let $\bold{R}$ be a set of role names with both transitive and normal role names $\bold{R_+} \sqcup \bold{R}_P = \bold{R}$, where $\bold{R}_+ \cap \bold{R}_P = \text{\o}$. The set of SROIQ-roles is $\bold{R} \sqcup \text{\textbraceleft} R^- \text{\textbar} R \in \bold{R} \text{\textbraceright}$.  In some DLs we would also define a third disjoint set of role names: the functional role names. SROIQ-roles do not define functional role names.

A role inclusion axiom is of the form $R \sqsubseteq S$, for two SHIQ-roles $R$ and $S$.  A role hierarchy is a set of role inclusion axioms. A complex role inclusion is of the form $S \circ R \sqsubseteq S$ or $R \circ S \sqsubseteq S$,  for two SROIQ-roles $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$ = ($\Delta^{I}, \bullet^{I}$) consists of a set $\Delta^{I}$, called the domain of $I$ and a function $\bullet^{I}$ which maps every role to a subset of $\Delta^{I} \times \Delta^{I}$ such that, for $p \in \bold{R}$ and $R \in \bold{R_+}$,

$\quad <x, y> \in P^I$ iff $<y, x> \in P^{-I}$, and

$\quad$ if $\space <x, y> \in R^I$ and $<y, z> \in R^I$ then $<x, z> \in R^I$.

An interpretation $\bold{I}$ satisfies a role hierarchy $\bold{R}$  iff $R^I \sqsubseteq S^I$ for each $R \sqsubseteq S \in \bold{R}$ ; Such an interpretation is called a model of $\bold{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:

$\quad$ 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 \sqsubseteq S^I$ implies Inv($R^I$) \sqsubseteq Inv($S^I$), for a role hierarchy $\bold{R}$, we introduce \sqsubseteq\ast as the transitive-reflexive closure of \sqsubseteq on $\bold{R} \sqcup \text{\textbraceleft} \bold{Inv}(R) \sqsubseteq \bold{Inv}(S) | R \sqsubseteq S \in \bold{R} \text{\textbraceright}$.  We use $R \doteq S$ as an abbreviation for $R$ \sqsubseteq\ast $S$ and $S$ \sqsubseteq\ast $R$.

Obviously, a role $R$ is transitive iff its inverse $\bold{Inv}(R)$ is transitive. However, in cyclic cases such as $R \doteq S$, $S$ is transitive if $R$ or $\bold{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 \doteq R$, $S \in \bold{R_+}$ or $\bold{Inv}(S) \in \bold{R_+}$, and false otherwise.

A role $R$ is called simple w.r.t. $\bold{R}$  iff not Trans($S$) for each $S \sqsubseteq\ast 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 $\bold{R}$  and the role hierarchy $\bold{R^-}$ formed by the inverses of each role in $\bold{R}$  are isomorphic. Suppose that a role hierarchy is defined with axioms that are drawn from both $\bold{R}$ and $\bold{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 $\small SROIQ^{(D)}$. 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 $\small SROIQ^{(D)}$ lacks formula calculations.

Concrete role extensions based on n-ary 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 n-ary 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).

An admissible concrete domain $D$ is equipped with a decision procedure for checking satisfiability of finite conjunctions over concrete predicates. Satisfiability checking of admissible concrete domains is performed in concert with DL inferencing for non-concrete domains.  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 $\small 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 $\small SHIQ$–concepts is the smallest set such that

Every concept name $C \in N_C$ is a concept,

If $C$ and $D$ are concepts and $R$ is a $\small SHIQ$–role, then ( $C \sqcap D$ ), ( $C \sqcup D$ ), ($\lnot C$ ), ($\forall R.C$ ), and ( $\exists R.C$ ), and

If $C$  is a concept, $R$  is a simple $\small SHIQ$–role and $n is a natural number, then ($\le nR.C$) and ($\ge nR.C``) are concepts.

A general concept inclusion (GCI) is an expression of the form $C_1 \sqsubseteq C_2$ for SHIQ–concepts $C_1$ and $C_2$.

A terminology (or TBox) is a set of GCIs.

The interpretation function $\bullet^{I}$ of an interpretation $I$ = ($\Delta^{I}, \bullet^{I}$) maps, additionally, every concept to a subset of $\Delta^{I}$ such that

• $( C \sqcap D )^I = C^I \sqcap D^I$,

• $( C \sqcup D )^I = C^I \sqcup D^I$,

• $(\lnot C )^I = \Delta^I \backslash C^I$,

• $( \exists R.C )^I = \text{\textbraceleft} x \in \Delta^I$ | There is some $y \in \Delta^I$ with $<x, y> \in \bold{R^I}$ and $y \in \bold{C^I}\text{\textbraceright}$,

• $( \forall R.C )^I = \text{\textbraceleft} x \in \Delta^I$ | For all $y \in \Delta^I$ , if $<x, y> \in \bold{R^I}$ then $y \in \bold{C^I} \text{\textbraceright}$,

• $( \leq nR.C )^I = \text{\textbraceleft} x \in \Delta^I | \#R^I(x,C) \leq n \text{\textbraceright}$,

• $( \geq nR.C )^I = \text{\textbraceleft} x \in \Delta^I | \#R^I(x,C) \geq n \text{\textbraceright}$,

where, for a set $M$, we denote the cardinality of $M$ by $\#M$ and $R^I(x,C)$ is defined as $\text{\textbraceleft} y | <x, y> \in \bold{R^I}$ and $y \in \bold{C^I} \text{\textbraceright}$.

A concept C is called satisfiable with respect to a role hierarchy $\bold{R}$  iff there is a model $\bold{I}$ of  with $C^I \ne \text{\o}$. Such an interpretation is called a model of $\bold{C}$  w.r.t. $\bold{R}$. A concept $D$subsumes a concept $C$ w.r.t. $R$  (written $C \sqsubseteq_R D$) iff $C^I \subseteq D^I$ holds for every model $I$ of $R$. Two concepts $C$, $D$ are equivalent w.r.t. $R$  (written $C \equiv_R D$) iff they are mutually subsuming.

Let $\bold{R}$ be a role hierarchy and $D$ a $\small SHIQ$–concept in Negation Normal Form (NNF). A completion tree w.r.t. $\bold{R}$  and $D$ is a tree $\bold{T}$ where each node $x$ of the tree is labeled with a set $L(x)$ \subseteq 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 $\ne$.

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 \in L(<x,y>)$ for some $S$ \sqsubseteq\ast $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 $\bold{T}$, we define $S^T(x,C)$ by $S^T(x,C) := \text{\textbraceleft} y | y$ is a $S$–neighbor of $x$ and $C \in L(y) \text{\textbraceright}$.

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 \sqsubseteq D$ iff $C \sqcap \lnot D$ is unsatisfiable.

• $C$ is unsatisfiable iff $C \sqsubseteq A \sqcap \lnot A$ for some concept name $A$.

• $C$ is satisfiable iff the ABox $\text{\textbraceleft} a:C \text{\textbraceright}$ 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 \sqcap \forall 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 \sqcap \forall 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, $\bold{A}$ an ABox, $\bold{T}$ a terminology, and $\bold{R}$ a role hierarchy. We define

$\qquad C_T := \sqcap (\lnot C_i) \sqcup D_i$ where the meet is over all $C_i \sqsubseteq D_i \in \bold{T}$.

Let $U$ be a transitive role that does not occur in $\bold{T}$, $C$, $D$, $\bold{A}$, or $\bold{R}$. We set

$\qquad \bold{R_U} := R \cup \text{\textbraceleft} R \sqsubseteq U, Inv(R) \sqsubseteq U | R$ occurs in $\bold{T}$, $C$, $D$, $\bold{A}$, or $\bold{R} \text{\textbraceright}$.

Then:

• $C$ is satisfiable w.r.t. $\bold{T}$ and $\bold{R}$ iff $C \sqcap C_T \sqcap \forall U.C_T$ is satisfiable w.r.t. $\bold{R_U}$.

• $D$ subsumes $C$  w.r.t. $\bold{T}$ and $\bold{R}$ iff $C \sqcap \lnot D \sqcap C_T \sqcap \forall U.C_T$ is unsatisfiable w.r.t. $\bold{R_U}$.

• $\bold{A}$ is consistent w.r.t. $\bold{T}$ and $\bold{R}$ iff $\bold{A} \cup \text{\textbraceleft} a:C_T \sqcap \forall U.C_T$ | $a$ occurs in $\bold{A}\text{\textbraceright}$} is consistent w.r.t. $\bold{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, non-chronological 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:

• Meta-rules that govern the order of application of rules

• Blocking strategies that close redundant expansions that are created by cyclic definitions

• Non-chronological 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.