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:
-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:
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 .