As has been shown by Plotkin, the general subsumption problem for Horn clauses is undecidable. Essentially, this negative result is due to the fact that subsumption can be reduced to logical implication. -subsumption is one approximation of the `logical' subsumption that is based on instantiations of Herbrand terms and set inclusion. In principle, there are two ways how to get a decidable rule ordering:

- One can restrict the expressiveness of the underlying knowledge
representation language such that logical implication becomes
decidable, e.g. Buntine's
*generalized subsumption*with restriction to DATALOG. - Alternatively, the rule ordering can be defined using only a
weak approximation of logical implication. For example,
the subset test used for
*-subsumption*is such a sound but incomplete operationalization of logical implication.

-subsumption relies on the instantiation ordering of Herbrand
terms which implies additional deficits:
There are ``too many'' terms that are
incomparable w.r.t. the instantiation ordering of Herbrand terms
(e.g., are all incomparable). The
weakness is also indicated by the fact that there are *linear*
decision procedures for the instantiation problem of Herbrand terms.

These deficits are somehow inherent to the underlying Horn logic. As an alternative, [\protect\citeauthoryearHanschke and Meyer1992] propose a rule-formalism based on terminological logics (TL). This enables us to define a rule ordering much like -subsumption, but which is based on terminological inferences instead of instantiating Herbrand terms. As terminological reasoning formalisms are tuned to be similarly expressive while remaining tractable or at least decidable, we gain a more fine-grained rule-ordering. In particular, more rules will become comparable. Moreover, we obtain a more intuitive knowledge representation.

We will first briefly introduce the *assertional* formalism
(A-box) and the *terminological* formalism (T-box) of the concept
language as a prototypical representative for the family of
terminological formalisms (e.g. [\protect\citeauthoryearBorgida *et al.*1989])
that originated with KL-ONE [\protect\citeauthoryearBrachman and
Schmolze1985].
A *terminology* of the T-box consists of a set of
*concept definitions* where
is the newly introduced concept name and is a concept term
constructed from concept names, roles, and attributes using the following
concept forming operators:
(),
(),
*negation* (),
*value-restriction*
(), and
*exists-in restriction*
(). In an *A-box* (assertional box) concepts, roles, and attributes
can be instantiated by individuals.
Formally, an A-box is a *finite* set of
role assertions (),
membership assertions (), and equalities (),
where and are individual names, is a role or attribute name,
and is a concept term.
The subsumption problem for A-boxes of can be effectively
decided [\protect\citeauthoryearHanschke and Meyer1992].

Two individuals and are *directly linked* in an A-box iff
the A-box contains a role assertion of the form or .
*Linked* is the transitive reflexive closure of directly linked.
An A-box is called *rooted* by (individuals) ,
, iff every individual in the A-box is linked to at least one of
the and all occur in the A-box.

The rule language is now based on the terminological formalism. Its operational semantics can be based on a CLP scheme [\protect\citeauthoryearJaffar and Lassez1987][\protect\citeauthoryearSmolka1989].

A *rule* takes the form
where the are predicate symbols with arities , the
are tuples of individuals ,
and is an A-box rooted by the
individuals in the .
It is interpreted as a logical formula in the obvious way.

The idea behind the rule ordering is essentially the same as for
-subsumption. The only difference is that instead of searching
for a substitution that acts as a witness for the
instantiation relation, we now employ the A-box subsumption of the
terminological formalism. The resulting rule ordering is called
*TL-subsumption*.

Assume that two rules
over disjoint sets of variables are given.
The -rule is more general than the -rule
w.r.t. *TL-subsumption* iff there is a substitution
such that the following holds:

- and are equal,
- , and
- the A-box subsumes w.r.t. .

As the terminological formalism provides attributes and a complement operator it is possible to map Herbrand terms into the set of A-boxes that are rooted by one individual such that two Herbrand terms and are unifiable iff is satisfiable, where and are the images under the mapping from concept terms into first-order formulas as defined in [\protect\citeauthoryearHanschke and Meyer1992]. This embedding naturally extends to a mapping from Horn rules to the rule formalism. It has been shown in [\protect\citeauthoryearHanschke and Meyer1992] that TL-subsumption is at least as powerful as -subsumption, i.e. given two Horn rules and , is more general than w.r.t. -subsumption iff .