Description Logics are a family of knowledge representation formalisms well-suited for intensional reasoning about conceptual models of databases/data warehouses. We extend Description Logics with concrete domains (such as integers and rational numbers) that include aggregation functions over these domains (such as min, max, count, and sum) which are usually available in database systems.<br> We show that the presence of aggregation functions may easily lead to undecidability of (intensional) inference problems such as satisfiability and subsumption. However, there are also extensions for which satisfiability and subsumption are decidable, and we present decision procedures for the relevant inference problems.

@article{ BaaderSattlerIS-02,
  author = {F. {Baader} and U. {Sattler}},
  journal = {Information Systems},
  number = {8},
  pages = {979--1004},
  title = {Description Logics with Aggregates and Concrete Domains},
  volume = {28},
  year = {2003},
}

The main contribution of this article is a new method for combining decision procedures for the word problem in equational theories. In contrast to previous methods, it is based on transformation rules, and also applies to theories sharing "constructors."

@article{ BaaderTinelliIC02,
  author = {F. {Baader} and C. {Tinelli}},
  journal = {Information and Computation},
  number = {2},
  pages = {346--390},
  title = {Deciding the Word Problem in the Union of Equational Theories},
  volume = {178},
  year = {2002},
}

Unification of concept terms is a new kind of inference problem for Description Logics, which extends the equivalence problem by allowing to replace certain concept names by concept terms before testing for equivalence. We show that this inference problem is of interest for applications, and present first decidability and complexity results for a small concept description language.

@article{ Baader-Narendran-JSC-00,
  author = {F. {Baader} and P. {Narendran}},
  journal = {J. Symbolic Computation},
  number = {3},
  pages = {277--305},
  title = {Unification of Concepts Terms in Description Logics},
  volume = {31},
  year = {2001},
}

This is the final version of a chapter on unification theory to appear in the Handbook of Automated Reasoning. The chapter is not intended to give a complete coverage of all the results. Instead we try to cover a number of significant topics in more detail. This should give a feeling for unification research and its methodology, provide the most important references, and enable the reader to study recent research papers on the topic.

@incollection{ BaaderSnyderHandbook00,
  author = {F. {Baader} and W. {Snyder}},
  booktitle = {Handbook of Automated Reasoning},
  editor = {J.A. {Robinson} and A. {Voronkov}},
  note = {See the handbook Web pages of Andrei Voronkov (http://www.cs.man.ac.uk/~voronkov/handbook-ar/index.html) and Elsevier (http://www.elsevier.nl/locate/isbn/0444829490).},
  pages = {447--533},
  publisher = {Elsevier Science Publishers},
  title = {Unification Theory},
  volume = {I},
  year = {2001},
}

We present a PSPACE algorithm that decides satisfiability of the graded modal logic Gr(K_R) - a natural extension of propositional modal logic K_R by counting expressions - which plays an important role in the area of knowledge representation. The algorithm employs a tableaux approach and is the first known algorithm which meets the lower bound for the complexity of the problem. Thus, we exactly fix the complexity of the problem and refute a EXPTIME-hardness conjecture. We extend the results to the logic Gr(K_R\cap^-1), which augments Gr(K_R) with inverse relations and intersection of accessibility relations. This establishes a kind of ``theoretical benchmark'' that all algorithmic approaches can be measured against.

@article{ Tobies-JLC-2001,
  author = {Stephan {Tobies}},
  journal = {Journal of Logic and Computation},
  number = {1},
  pages = {85--106},
  title = {{PSPACE} Reasoning for Graded Modal Logics},
  volume = {11},
  year = {2001},
}

Matching concepts against patterns (concepts with variables) is a relatively new operation that has been introduced in the context of concept description languages (description logics). The original goal was to help filter out unimportant aspects of complicated concepts appearing in large industrial knowledge bases. We propose a new approach to performing matching, based on a ``concept-centered'' normal form, rather than the more standard ``structural subsumption'' normal form for concepts. As a result, matching can be performed (in polynomial time) using arbitrary concept patterns of the description language ALN, thus removing restrictions from previous work. The paper also addresses the question of matching problems with additional ``side conditions'', which were motivated by practical needs.

@article{ BaadKuestBorgMcGuinn-JLC-99,
  author = {F. {Baader} and R. {K{\"u}sters} and A. {Borgida} and D. {McGuinness}},
  journal = {Journal of Logic and Computation},
  number = {3},
  pages = {411--447},
  title = {Matching in Description Logics},
  volume = {9},
  year = {1999},
}

Number restrictions are concept constructors that are available in almost all implemented Description Logic systems. However, they are mostly available only in a rather weak form, which considerably restricts their expressive power. On the one hand, the roles that may occur in number restrictions are usually of a very restricted type, namely atomic roles or complex roles built using either intersection or inversion. In the present paper, we increase the expressive power of Description Logics by allowing for more complex roles in number restrictions. As role constructors, we consider composition of roles (which will be present in all our logics) and intersection, union, and inversion of roles in different combinations. We will present two decidability results (for the basic logic that extends ALC by number restrictions on roles with composition, and for one extension of this logic), and three undecidability results for three other extensions of the basic logic. On the other hand, with the rather weak form of number restrictions available in implemented systems, the number of role successors of an individual can only be restricted by a fixed non-negative integer. To overcome this lack of expressiveness, we allow for variables ranging over the non-negative integers in place of the fixed numbers in number restrictions. The expressive power of this constructor is increased even further by introducing explicit quantifiers for the numerical variables. The Description Logic obtained this way turns out to have an undecidable satisfiability problem. For a restricted logic we show that concept satisfiability is decidable.

@article{ BaaderSattler-JLC-99,
  author = {F. {Baader} and U. {Sattler}},
  journal = {Journal of Logic and Computation},
  number = {3},
  pages = {319--350},
  title = {Expressive Number Restrictions in Description Logics},
  volume = {9},
  year = {1999},
}

This article presents the description logic ALCRP(D) with concrete domains and a role-forming predicate operator as its prominent aspects. We demonstrate the feasibility of ALCRP(D) for reasoning about spatial objects and their qualitative spatial relationships and provide an appropriate concrete domain for spatial objects. The general significance of ALCRP(D) is demonstrated by adding temporal reasoning to spatial and terminological reasoning using a combined concrete domain. The theory is motivated as a basis for knowledge representation and query processing in the domain of geographic information systems. In contrast to existing work in this domain, which mainly focuses either on conceptual reasoning or on reasoning about qualitative spatial relations, we integrate reasoning about spatial information with terminological reasoning.

@article{ Haarslev-Lutz+-JLC-1999,
  author = {V. {Haarslev} and C. {Lutz} and R. {M{\"o}ller}},
  journal = {Journal of Logic and Computation},
  number = {3},
  pages = {351--384},
  title = {A Description Logic with Concrete Domains and Role-forming Predicates},
  volume = {9},
  year = {1999},
}

The combination of transitive and inverse roles is important in a range of applications, and is crucial for the adequate representation of aggregated objects, allowing the simultaneous description of parts by means of the whole to which they belong and of wholes by means of their constituent parts. In this paper we present tableaux algorithms for deciding concept satisfiability and subsumption in Description Logics that extend with both transitive and inverse roles, a role hierarchy, and functional restrictions. In contrast to earlier algorithms for similar logics, those presented here are well-suited for implementation purposes: using transitive roles and role hierarchies in place of the transitive closure of roles enables sophisticated blocking techniques to be used in place of the cut rule, a rule whose high degree of non-determinism strongly discourages its use in an implementation. As well as promising superior computational behaviour, this new approach is shown to be sufficiently powerful to allow subsumption and satisfiability with respect to a (possibly cyclic) knowledge base to be reduced to concept subsumption and satisfiability, and to support reasoning in a Description Logic that no longer has the finite model property.

@article{ HorrSat-JLC-99,
  author = {I. {Horrocks} and U. {Sattler}},
  journal = {Journal of Logic and Computation},
  number = {3},
  pages = {385--410},
  title = {A Description Logic with Transitive and Inverse Roles and Role Hierarchies},
  volume = {9},
  year = {1999},
}

When combining languages for symbolic constraints, one is typically faced with the problem of how to treat ``mixed'' constraints. The two main problems are (1) how to define a combined solution structure over which these constraints are to be solved, and (2) how to combine the constraint solving methods for pure constraints into one for mixed constraints. The paper introduces the notion of a ``free amalgamated product'' as a possible solution to the first problem. We define so-called quasi-free structures (called ``strong simply-combinable structures'' in a previous publication) as a generalization of free structures. For quasi-free structures over disjoint signatures, we describe a canonical amalgamation construction that yields the free amalgamated product. The combination techniques known from unification theory can be used to combine constraint solvers for quasi-free structures over disjoint signatures into a solver for their free amalgamated product. In addition to term algebras modulo equational theories (i.e., free algebras), the class of quasi-free structures contains many solution structures that are of interest in constraint logic programming, such as the algebra of rational trees, feature structures, and domains consisting of hereditarily finite (wellfounded or non-wellfounded) nested sets and lists.

@article{ BaaderSchulz-TCS-98,
  author = {F. {Baader} and K. {Schulz}},
  journal = {Theoretical Computer Science},
  pages = {107--161},
  title = {Combination of Constraint Solvers for Free and Quasi-Free Structures},
  volume = {192},
  year = {1998},
}

The notions `expressive power' or `expressiveness' of knowledge representation languages (KR languages) can be found in most papers on knowledge representation; but these terms are usually just employed in an intuitive sense. The papers contain only informal descriptions of what is meant by expressiveness. There are several reasons that speak in favour of a formal definition of expressiveness: for example, if we want to show that certain expressions in one language cannot be expressed in another language, we need a strict formalism that can be used in mathematical proofs. Even though we shall only consider terminological KR languages—i.e. KR languages descending from the original system KL-ONE—in our motivation and in the examples, the definition of expressive power that will be given in this paper can be used for all KR languages with Tarski-style model-theoretic semantics. This definition will shed a new light on the tradeoff between expressiveness of a representation language and its computational tractability. There are KR languages with identical expressive power, but different complexity results for reasoning, which comes from the fact that sometimes the tradeoff lies between convenience and computational tractability. The definition of expressive power will be applied to compare various terminological KR languages known from the literature with respect to their expressiveness. This will yield examples for how to utilize the definition both in positive proofs—that is, proofs where it is shown that one language can be expressed by another language—and, more interestingly, in negative proofs—which show that a given language cannot be expressed by the other language.

@article{ Baader-JLC-96,
  author = {F. {Baader}},
  journal = {J. of Logic and Computation},
  number = {1},
  pages = {33--54},
  title = {A Formal Definition for the Expressive Power of Terminological Knowledge Representation Languages},
  volume = {6},
  year = {1996},
}

In most of the implemented terminological knowledge representation systems it is not possible to state recursive concept definitions, so-called terminological cycles. One reason is that it is not clear what kind of semantics to use for such cyles. In addition, the inference algorithms used in such systems may go astray in the presence of terminological cycles. In this paper we consider terminological cycles in a very small terminological representation language. For this language, the effect of the three types of semantics introduced by B. Nebel can completely be described with the help of finite automata. These descriptions provide for a rather intuitive understanding of terminologies with recursive definitions, and they give an insight into the essential features of the respective semantics. In addition, one obtains algorithms and complexity results for the subsumption problem and for related inference tasks. The results of this paper may help to decide what kind of semantics is most appropriate for cyclic definitions, depending on the representation task.

@article{ Baader-AMAI-96,
  author = {F. {Baader}},
  journal = {Annals of Mathematics and Artificial Intelligence},
  number = {2--4},
  pages = {175--219},
  title = {Using Automata Theory for Characterizing the Semantics of Terminological Cycles},
  volume = {18},
  year = {1996},
}

The concept description formalisms of existing description logics systems allow the user to express local cardinality restrictions on the fillers of a particular role. It is not possible, however, to introduce global restrictions on the number of instances of a given concept. This article argues that such cardinality restrictions on concepts are of importance in applications such as configuration of technical systems, an application domain of description logics systems that is currently gaining in interest. It shows that including such restrictions in the description language leaves the important inference problems such as instance testing decidable. The algorithm combines and simplifies the ideas developed for the treatment of qualified number restrictions and of general terminological axioms.

@article{ BaaderBuchheit+-AIJ-1996,
  author = {F. {Baader} and M. {Buchheit} and B. {Hollunder}},
  journal = {Artificial Intelligence},
  number = {1--2},
  pages = {195--213},
  title = {Cardinality Restrictions on Concepts},
  volume = {88},
  year = {1996},
}

Most of the work on the combination of unification algorithms for the union of disjoint equational theories has been restricted to algorithms that compute finite complete sets of unifiers. Thus the developed combination methods usually cannot be used to combine decision procedures, i.e., algorithms that just decide solvability of unification problems without computing unifiers. In this paper we describe a combination algorithm for decision procedures that works for arbitrary equational theories, provided that solvability of so-called unification problems with constant restrictions—a slight generalization of unification problems with constants—is decidable for these theories. As a consequence of this new method, we can, for example, show that general A-unifiability, i.e., solvability of A-unification problems with free function symbols, is decidable. Here A stands for the equational theory of one associative function symbol. Our method can also be used to combine algorithms that compute finite complete sets of unifiers. Manfred Schmidt-Schauß' combination result, the until now most general result in this direction, can be obtained as a consequence of this fact. We also obtain the new result that unification in the union of disjoint equational theories is finitary, if general unification—i.e., unification of terms with additional free function symbols—is finitary in the single theories.

@article{ BaaderSchulz-JSC-96,
  author = {F. {Baader} and K. U. {Schulz}},
  journal = {J. Symbolic Computation},
  pages = {211--243},
  title = {Unification in the Union of Disjoint Equational Theories: {C}ombining Decision Procedures},
  volume = {21},
  year = {1996},
}

We consider the problem of integrating Reiter's default logic into terminological representation systems. It turns out that such an integration is less straightforward than we expected, considering the fact that the terminological language is a decidable sublanguage of first-order logic. Semantically, one has the unpleasant effect that the consequences of a terminological default theory may be rather unintuitive, and may even vary with the syntactic structure of equivalent concept expressions. This is due to the unsatisfactory treatment of open defaults via Skolemization in Reiter's semantics. On the algorithmic side, we show that this treatment may lead to an undecidable default consequence relation, even though our base language is decidable, and we have only finitely many (open) defaults. Because of these problems, we then consider a restricted semantics for open defaults in our terminological default theories: default rules are only applied to individuals that are explicitly present in the knowledge base. In this semantics it is possible to compute all extensions of a finite terminological default theory, which means that this type of default reasoning is decidable. We describe an algorithm for computing extensions, and show how the inference procedures of terminological systems can be modified to give optimal support to this algorithm.

@article{ BaaderHollunderA-JAR-95,
  author = {F. {Baader} and B. {Hollunder}},
  journal = {J. Automated Reasoning},
  pages = {149--180},
  title = {Embedding Defaults into Terminological Representation Systems},
  volume = {14},
  year = {1995},
}

In a recent paper we have proposed terminological default logic as a formalism which combines both means for structured representation of classes and objects, and for default inheritance of properties. The major drawback that terminological default logic inherits from general default logic is that it does not take precedence of more specific defaults over more general ones into account. This behaviour has already been criticized in the general context of default logic, but it is all the more problematic in the terminological case where the emphasis lies on the hierarchical organization of concepts. The present paper addresses the problem of modifying terminological default logic such that more specific defaults are preferred. We assume that the specificity ordering is induced by the hierarchical organization of concepts, which means that default information is not taken into account when computing priorities. It turns out that the existing approaches for expressing priorities between defaults do not seem to be appropriate for defaults with prerequisites. Therefore we shall consider an alternative approach for dealing with prioritization in the framework of Reiter's default logic. The formalism is presented in the general setting of default logic where priorities are given by an arbitrary partial ordering on the defaults. We shall exhibit some interesting properties of the new formalism, compare it with existing approaches, and describe an algorithm for computing extensions. In the terminological case, we thus obtain an automated default reasoning procedure that takes specificity into account.

@article{ BaaderHollunderB-JAR-95,
  author = {F. {Baader} and B. {Hollunder}},
  journal = {J. Automated Reasoning},
  pages = {41--68},
  title = {Priorities on Defaults with Prerequisites, and their Application in Treating Specificity in Terminological Default Logic},
  volume = {15},
  year = {1995},
}

Previous work on combination techniques considered the question of how to combine unification algorithms for disjoint equational theories \(E_1,\ldots,E_n\) in order to obtain a unification algorithm for the union \(E_1 \cup \ldots\cup E_n\) of the theories. Here we want to show that variants of this method may be used to decide solvability and ground solvability of disunification problems in \(E_1 \cup \ldots\cup E_n\). Our first result says that solvability of disunification problems in the free algebra of the combined theory \(E_1 \cup \ldots\cup E_n\) is decidable if solvability of disunification problems with linear constant restrictions in the free algebras of the theories \(E_i\) (\(i = 1,\ldots,n\)) is decidable. In order to decide ground solvability (i.e., solvability in the initial algebra) of disunification problems in \(E_1 \cup \ldots\cup E_n\) we have to consider a new kind of subproblem for the particular theories \(E_i\), namely solvability (in the free algebra) of disunification problems with linear constant restriction under the additional constraint that values of variables are not \(E_i\)-equivalent to variables. The correspondence between ground solvability and this new kind of solvability holds, (1) if one theory \(E_i\) is the free theory with at least one function symbol and one constant, or (2) if the initial algebras of all theories \(E_i\) are infinite. Our results can be used to show that the existential fragment of the theory of the (ground) term algebra modulo associativity of a finite number of function symbols is decidable; the same result follows for function symbols which are associative and commutative, or associative, commutative and idempotent.

@article{ BaaderSchulz-TCS-95,
  author = {F. {Baader} and K.U. {Schulz}},
  journal = {Theoretical Computer Science B},
  pages = {229--255},
  title = {Combination Techniques and Decision Problems for Disunification},
  volume = {142},
  year = {1995},
}

@article{ Baader-JSC-89,
  author = {F. {Baader}},
  journal = {J. Symbolic Computation},
  pages = {479--497},
  title = {Unification in Commutative Theories},
  volume = {8},
  year = {1989},
}

@article{ Baader-IPL-88,
  author = {F. {Baader}},
  journal = {Information Processing Letters},
  pages = {91--93},
  title = {A Note on Unification Type Zero},
  volume = {27},
  year = {1988},
}

@article{ BaaderBuettner-TCS-88,
  author = {F. {Baader} and W. {B{\"u}ttner}},
  journal = {J. Theoretical Computer Science},
  pages = {345--352},
  title = {Unification in Commutative Idempotent Monoids},
  volume = {56},
  year = {1988},
}

@article{ Baader-SemigroupForum-87,
  author = {F. {Baader}},
  journal = {Semigroup Forum},
  pages = {127--145},
  title = {Unification in Varieties of Idempotent Semigroups},
  volume = {36},
  year = {1987},
}

@article{ Baader-JAR-86,
  author = {F. {Baader}},
  journal = {J. Automated Reasoning},
  pages = {283--286},
  title = {The Theory of Idempotent Semigroups is of Unification Type Zero},
  volume = {2},
  year = {1986},
}