Conceptual graphs (CGs) are an expressive and intuitive formalism, which plays an important role in the area of knowledge representation. Due to their expressiveness, most interesting problems for CGs are inherently undecidable. We identify the syntactically defined guarded fragment of CGs, for which both subsumption and validity is decidable in deterministic exponential time.

This work introduces the concept language ALCFM which is an extension of ALC to many-valued logics. ALCFM allows to express vague concepts, e.g. more or less enlarged or very small. To realize this extension to many-valued logics, the classical notions of satisfiability and subsumption had to be modied appropriately. For example, ALCFM-concepts are no longer either satisfiable or unsatisfiable, but they are satisfiable to a certain degree. The main contribution of this paper is a sound and complete method for computing the degree of subsumption between two ALCFM-concepts. / An abridged version of this paper has been published in the Proceedings of the 13th biennial European Conference on Artificial Intelligence (ECAI'98).

Aus der Einleitung: „In this paper, we reuse the representation formalism `description graph' in order to characterize subsumption of ALN-concepts. The description logic ALN allows for conjunction, valuerestrictions, number restrictions, and primitive negation. Since Classic allows for more constructors than ALN, e.g., equality restrictions an attribute chains by the constructor SAME-AS,we can confine the notion of description graphs from [BP94]. On the other hand, ALN explicitly allows for primitive negation which yields another possibility { besides conflicting number restrictions { to express inconsistency. Thus, we have to modify the notion of canonical description graphs in order to cope with inconsistent concepts in the structural characterization of subsumption. It turns out that the description graphs obtained from ALN-concepts are in fact trees. A canonical graph is a deterministic tree. The conditions required by the structural characterization of subsumption on these trees can be tested by an eficient algorithm, i.e., we obtain an algorithm deciding subsumption of C and D in time polynomial in the size of C and D. The report is structured as follows. In the preliminaries, we define syntax and semantics of the description logic ALN as well as the inference problem of subsumption. In Section 3, we introduce description graphs, the data structure our structural subsumption algorithm is working on. Besides syntax and semantics also an algorithm for translating ALN-concepts into description graphs is given. Thereafter, we present the main result of this report in Section 6, a characterization of subsumption of ALN-concepts by a structural comparison of corresponding description graphs. Furthermore, a structural subsumption algorithm can be found in Section 6.2. In the last section we summarize our results and give an outlook to further applications of structural subsumption in terminological knowledge representation systems.

Aus der Einleitung: „Equational unification is a generalization of syntactic unification in which semantic properties of function symbols are taken into account. For example, assume that the function symbol '+' is known to be commutative. Given the unication problem x + y ≐ a + b (where x and y are variables, and a and b are constants), an algorithm for syntactic unification would return the substitution {x ↦ a; y ↦ b} as the only (and most general) unifier: to make x + y and a + b syntactically equal, one must replace the variable x by a and y by b. However, commutativity of '+' implies that {x ↦ b; y ↦ b} also is a unifier in the sense that the terms obtained by its application, namely b + a and a + b, are equal modulo commutativity of '+'. More generally, equational unification is concerned with the problem of how to make terms equal modulo a given equational theory, which specifies semantic properties of the function symbols that occur in the terms to be unified.”

Computing the least common subsumer (lcs) in description logics is an inference task first introduced for sublanguages of CLASSIC. Roughly speaking, the lcs of a set of concept descriptions is the most specific concept description that subsumes all of the input descriptions. As such, the lcs allows to extract the commonalities from given concept descriptions, a task essential for several applications like, e.g., inductive learning, information retrieval, or the bottom-up construction of KR-knowledge bases. Previous work on the lcs has concentrated on description logics that either allow for number restrictions or for existential restrictions. Many applications, however, require to combine these constructors. In this work, we present an lcs algorithm for the description logic ALEN, which allows for both constructors (as well as concept conjunction, primitive negation, and value restrictions). The proof of correctness of our lcs algorithm is based on an appropriate structural characterization of subsumption in ALEN also introduced in this paper. / This research was carried out while the second author was still at the LuFG Theoretical Computer Science, RWTH Aachen.

Most of the research on temporalized Description Logics (DLs) has concentrated on the case where temporal operators can occur within DL concept descriptions. In this setting, reasoning usually becomes quite hard if rigid roles, i.e., roles whose interpretation does not change over time, are available. In this paper, we consider the case where temporal operators are allowed to occur only in front of DL axioms (i.e., ABox assertions and general concept inclusion axioms), but not inside of concepts descriptions. As the temporal component, we use linear temporal logic (LTL) and in the DL component we consider the basic DL ALC. We show that reasoning in the presence of rigid roles becomes considerably simpler in this setting.

Non-standard inferences are particularly useful in the bottom-up construction of ontologies in description logics. One of the more common non-standard reasoning tasks is the most specific concept (msc) for an ABox-individual. In this paper we present similar non-standard reasoning task: most specific concepts for models (model-mscs). We show that, although they look similar to ABox-mscs their computational behaviour can be different. We present constructions for model-mscs in FL₀ and FLE with cyclic TBoxes and for ALC∪∗ with acyclic TBoxes. Since subsumption in FLE with cyclic TBoxes has not been examined previously, we present a characterization of subsumption and give a construction for the least common subsumer in this setting.

Consider an ontology T where every axiom is labeled with an element of a lattice (L, ≤). Then every element l of L determines a sub-ontology Tl, which consists of the axioms of T whose labels are greater or equal to l. These labels may be interpreted as required access rights, in which case Tl is the sub-ontology that a user with access right l is allowed to see, or as trust levels, in which case Tl consists of those axioms that we trust with level at least l. Given a consequence α (such as a subsumption relationship between concepts) that follows from the whole ontology T, we want to know from which of the sub-ontologies Tl determined by lattice elements l the consequence α still follows. However, instead of reasoning with Tl in the deployment phase of the ontology, we want to pre-compute this information during the development phase. More precisely, we want to compute what we call a boundary for α, i.e., an element μα of L such that α follows from T l iff l ≤ μα. In this paper we show that, under certain restrictions on the elements l used to define the sub-ontologies, such a boundary always exists, and we describe black-box approaches for computing it that are generalizations of approaches for axiom pinpointing in description logics. We also present first experimental results that compare the efficiency of these approaches on real-world ontologies.

Motivated by a chemical process engineering application, we introduce a new concept constructor in Description Logics (DLs), an n-ary variant of the existential restriction constructor, which generalizes both the usual existential restrictions and so-called qualified number restrictions. We show that the new constructor can be expressed in ALCQ, the extension of the basic DL ALC by qualified number restrictions. However, this representation results in an exponential blow-up. By giving direct algorithms for ALC extended with the new constructor, we can show that the complexity of reasoning in this new DL is actually not harder than the one of reasoning in ALCQ. Moreover, in our chemical process engineering application, a restricted DL that provides only the new constructor together with conjunction, and satisfies an additional restriction on the occurrence of roles names, is sufficient. For this DL, the subsumption problem is polynomial. / Short versions of this report have also appeared in Proc. of KI'05 and Proc. of DL'05.

We propose an approach for extending both the terminological and the assertional part of a Description Logic knowledge base by using information provided by the assertional part and by a domain expert. The use of techniques from Formal Concept Analysis ensures that, on the one hand, the interaction with the expert is kept to a minimum, and, on the other hand, we can show that the extended knowledge base is complete in a certain sense.