Unification has been introduced in Description Logic (DL) as a means to detect redundancies in ontologies. In particular, it was shown that testing unifiability in the DL EL is an NP-complete problem, and this result has been extended in several directions. Surprisingly, it turned out that the complexity increases to PSpace if one disallows the use of the top concept in concept descriptions. Motivated by features of the medical ontology SNOMED CT, we extend this result to a setting where the top concept is disallowed, but there is a background ontology consisting of restricted forms of concept and role inclusion axioms. We are able to show that the presence of such axioms does not increase the complexity of unification without top, i.e., testing for unifiability remains a PSpace-complete problem.

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. / This revised version of LTCS-Report 97-02 provides a stronger complexity result in Section 6. An abridged version will appear in Proc. ECAI'98 .

Unification modulo the theory of Boolean algebras has been investigated by several autors. Nevertheless, the exact complexity of the decision problem for unification with constants and general unification was not known. In this research note, we show that the decision problem is complete for unification with constants and PSPACE-complete for general unification. In contrast, the decision problem for elementary unification (where the terms to be unified contain only symbols of the signature of Boolean algebras) is 'only' NP-complete.

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.

The Description Logic EL is an inexpressive knowledge representation language, which nevertheless has recently drawn considerable attention in the knowledge representation and the ontology community since, on the one hand, important inference problems such as the subsumption problem are polynomial. On the other hand, EL is used to define large biomedical ontologies. Unification in Description Logics has been proposed as a novel inference service that can, for example, be used to detect redundancies in ontologies. In a recent paper, we have shown that unification in EL is NP-complete, and thus of a complexity that is considerably lower than in other Description Logics of comparably restricted expressive power. In this paper, we introduce a new NP-algorithm for solving unification problem in EL, which is based on a reduction to satisfiability in propositional logic (SAT). The advantage of this new algorithm is, on the one hand, that it allows us to employ highly optimized state of the art SAT solverswhen implementing an EL-unification algorithm. On the other hand, this reduction provides us with a proof of the fact that EL-unification is in NP that is much simpler than the one given in our previous paper on EL-unification.

Unification in Description Logics has been proposed as a novel inference service that can, for example, be used to detect redundancies in ontologies. The inexpressive Description Logic EL is of particular interest in this context since, on the one hand, several large biomedical ontologies are defined using EL. On the other hand, unification in EL has recently been shown to be NP-complete, and thus of considerably lower complexity than unification in other DLs of similarly restricted expressive power. However, EL allows the use of the top concept (>), which represents the whole interpretation domain, whereas the large medical ontology SNOMEDCT makes no use of this feature. Surprisingly, removing the top concept from EL makes the unification problem considerably harder. More precisely, we will show that unification in EL without the top concept is PSpace-complete. / This is an updated version of the original report that includes Appendix A on locality of unifiers.

Unification has been investigated both in modal logics and in description logics, albeit with different motivations. In description logics, unification can be used to detect redundancies in ontologies. In this context, it is not sufficient to decide unifiability, one must also compute appropriate unifiers and present them to the user. For the description logic EL, which is used to define several large biomedical ontologies, deciding unifiability is an NP-complete problem. It is known that every solvable EL-unification problem has a minimal unifier, and that every minimal unifier is a local unifier. Existing unification algorithms for EL compute all minimal unifiers, but additionally (all or some) non-minimal local unifiers. Computing only the minimal unifiers would be better since there are considerably less minimal unifiers than local ones, and their size is usually also quite small. In this paper we investigate the question whether the known algorithms for EL-unification can be modified such that they compute exactly the minimal unifiers without changing the complexity and the basic nature of the algorithms. Basically, the answer we give to this question is negative.

Es werden verschiedene Aspekte interner magnetischer Hintergrundfelder in Theorien offener Strings diskutiert. Phaenomenologisch und konzeptionell interessante Eigenschaften solcher Vakua, die Brechung von Supersymmetrie, Eichsymmetrie und chiraler Symmetrie, werden auf ganz generische Weise behandelt. Dann wird eine Spezialisierung auf Typ I Modelle, kompaktifiziert auf Tori und Bahnfaltigkeiten, durchgefuehrt. Daraus wird eine Methode gewonnen zur Konstruktion von Typ I Vakua mit attraktiven effektiven Feldtheorien als Niederenergienaeherungen, sowohl supersymmetrische wie nicht supersymmetrische Modelle mit chiralen Fermionspektren und Eichgruppen aehnlich dem Standardmodell oder einer vereinheitlichenden Verallgemeinerung desselben. Die am weitesten entwickelten Beispiele kombinieren magnetische Felder mit NSNS B-Feldern auf Bahnfaltigkeiten. Zuletzt wird noch eine verwandte Klasse von Modellen besprochen, die zwar eher weniger vielversprechende phaenomenologische Perspektiven bietet, aber einige konzeptionelle Spezialitaeten aufweist. In diesen Kompaktifizierungen werden asymmetrische Rotationen geeicht, so dass D-branen mit unterschiedlichen Werten fuer die magnetischen Felder auf ihrem Weltvolumen identifiziert werden, womit die Unterscheidung von kommutativen und nicht kommutativen Geometrien verlorengeht. / We discuss various aspects of internal magnetic background fields in open string theories. Phenomenologically and conceptually interesting properties of such string theory backgrounds, supersymmetry and gauge symmetry breaking, chiral fermion spectra and noncommutativity of the internal compactification manifolds, are treated in a rather generic framework. We then specialize to type I compactifications on tori and toroidal orbifolds with magnetic fields on the internal space. This allows to develop a strategy for constructing type I vacua with attractive low energy field theories which may either be supersymmetric or not and contain chiral spectra and gauge groups close to the Standard Model or some grand unified generalization thereof. The most sophisticated version uses magnetic fields and NSNS B-fields on orbifold spaces giving rise to a plethora of promising examples for semi-realistic string compactifications. We finally also present a related class of asymmetric orbifolds of type I which are of little phenomenological interest but still display certain interesting features. The asymmetric rotations which are gauged in these models identify D-branes with different values for the magnetic field on their world volume, such that the distinction of commutative and noncommutative internal geometries is lost.

Am Beispiel des (seinerzeit geplanten) Baus einer Automobilteststrecke in Baden-Württemberg untersucht der Beitrag, unter welchen Voraussetzungen und mit welchen Bedingungen eine dafür für erforderlich angesehene Enteignung privaten Grund und Bodens für ein anderes privatwirtschaftliches Unternehmen mit der verfassungsrechtlichen Eigentumsgarantie vereinbar sein kann.Dabei werden auch in anderen Staaten bestehende Regelungen zum Vergleich einbezogen.