Aus der Einleitung: „The Guarded Fragment of first-order logic, introduced by Andréka, van Benthem, and Németi, has been a succesful attempt to transfer many good properties of modal, temporal, and description logics to a larger fragment of predicate logic. Among these are decidability, the finite modal property, invariance under an appropriate variant of bisimulation, and other nice modal theoretic properties. ...”

We examine the complexity and expressivity of the combination of the Description Logic ALCQI with a terminological formalism based on cardinality restrictions on concepts. This combination can naturally be embedded into C², the two variable fragment of predicate logic with counting quantifiers. We prove that ALCQI has the same complexity as C² but does not reach its expressive power. / An abriged version of this paper has been submitted to CSL'99

0 VORWORT Bei der maschinellen Übersetzung natürlicher Sprache dominieren mehrere Probleme. Man hat es immer mit sehr großen Datenmengen zu tun. Auch wenn man nur einen kleinen Text übersetzen will, ist diese Aufgabe in umfänglichen Kontext eingebettet, d.h. alles Wissen über Quell- und Zielsprache muß - in möglichst formalisierter Form - zur Verfügung stehen. Handelt es sich um gesprochenes Wort treten Spracherkennungs- und Sprachausgabeaufgaben sowie harte Echtzeitforderungen hinzu. Die Komplexität des Problems ist - auch unter Benutzung moderner Softwareentwicklungskonzepte - für jeden, der eine Implementation versucht, eine nicht zu unterschätzende Herausforderung. Ansätze, die die Arbeitsprinzipien und Methoden der Informatik konsequent nutzen, stellen ihre Ergebnisse meist nur prototyisch für einen sehr kleinen Teil der Sprache -etwa eine Phrase, einen Satz bzw. mehrere Beispielsätze- heraus und folgern mehr oder weniger induktiv, daß die entwickelte Lösung auch auf die ganze Sprache erfolgreich angewendet werden kann, wenn man nur genügend „Lemminge“ hat, die nach allen Seiten ausschwärmend, die „noch notwendigen Routinearbeiten“ schnell und bienenfleißig ausführen könnten.

0 VORWORT Bei der maschinellen Übersetzung natürlicher Sprache dominieren mehrere Probleme. Man hat es immer mit sehr großen Datenmengen zu tun. Auch wenn man nur einen kleinen Text übersetzen will, ist diese Aufgabe in umfänglichen Kontext eingebettet, d.h. alles Wissen über Quell- und Zielsprache muß - in möglichst formalisierter Form - zur Verfügung stehen. Handelt es sich um gesprochenes Wort treten Spracherkennungs- und Sprachausgabeaufgaben sowie harte Echtzeitforderungen hinzu. Die Komplexität des Problems ist - auch unter Benutzung moderner Softwareentwicklungskonzepte - für jeden, der eine Implementation versucht, eine nicht zu unterschätzende Herausforderung. Ansätze, die die Arbeitsprinzipien und Methoden der Informatik konsequent nutzen, stellen ihre Ergebnisse meist nur prototyisch für einen sehr kleinen Teil der Sprache -etwa eine Phrase, einen Satz bzw. mehrere Beispielsätze- heraus und folgern mehr oder weniger induktiv, daß die entwickelte Lösung auch auf die ganze Sprache erfolgreich angewendet werden kann, wenn man nur genügend „Lemminge“ hat, die nach allen Seiten ausschwärmend, die „noch notwendigen Routinearbeiten“ schnell und bienenfleißig ausführen könnten.:0 Vorwort S. 2 1 Allgemeiner Ablauf der Generierung S. 3 1.1 AUFGABE DER GENERIERUNG S. 3 1.2 EINORDNUNG DER GENERIERUNG IN DIE MASCHINELLE ÜBERSETZUNG S.4 1.3 REALISIERUNG S. 4 1.4 MORPHOLOGISCHE GENERIERUNG S.6 2 Strukturen und Abbildungen S. 8 2.1 UNIVERSELLE STRUKTUR: DEFINITION VON GRAPHEN S.8 2.2 FORMALISIERUNG SPEZIELLER SEMANTISCHER STRUKTUREN ALS GRAPHEN S.9 2.3 ABBILDUNG VON STRUKTUREN S.11 2.3.1 Strukturtyperhaltende Funktionen S. 12 2.3.2 Strukturtypverändernde Funktionen S. 19 2.3.3 Komplexe Funktionen S. 20 2.3.4 Abbildung eines gesamten Generierungsprozesses S. 21 4 Beispiel: Generierung von Texten aus prädikatenlogischen Ausdrücken (inkrementeller Algorithmus) S. 23 4.1 ABLAUF S.23 4.2 BEISPIELE VON REGELSTRUKTUREN S.27 5 Zusammenfassung S. 28 6 Quellenverzeichnis S. 30

In its many guises and variations, propositional dynamic logic (PDL) plays an important role in various areas of computer science such as databases, artificial intelligence, and computer linguistics. One relevant and powerful variation is ICPDL, the extension of PDL with intersection and converse. Although ICPDL has several interesting applications, its computational properties have never been investigated. In this paper, we prove that ICPDL is decidable by developing a translation to the monadic second order logic of infinite trees. Our result has applications in information logic, description logic, and epistemic logic. In particular, we solve a long-standing open problem in information logic. Another virtue of our approach is that it provides a decidability proof that is more transparent than existing ones for PDL with intersection (but without converse).

We introduce a modal language L which is obtained from standard modal logic by adding the Boolean operators on accessibility relations, the identity relation, and the converse of relations. It is proved that L has the same expressive power as the two-variable fragment FO² of first-order logic, but speaks less succinctly about relational structures: if the number of relations is bounded, then L-satisfiability is EXPTIME-complete but FO² satisfiability is NEXPTIME-complete. We indicate that the relation between L and FO² provides a general framework for comparing modal and temporal languages with first-order languages.

The Golog action programming language is a powerful means to express high-level behaviours in terms of programs over actions defined in a Situation Calculus theory. In particular for physical systems, verifying that the program satisfies certain desired temporal properties is often crucial, but undecidable in general, the latter being due to the language’s high expressiveness in terms of first-order quantification and program constructs. So far, approaches to achieve decidability involved restrictions where action effects either had to be contextfree (i.e. not depend on the current state), local (i.e. only affect objects mentioned in the action’s parameters), or at least bounded (i.e. only affect a finite number of objects). In this paper, we present a new, more general class of action theories (called acyclic) that allows for context-sensitive, non-local, unbounded effects, i.e. actions that may affect an unbounded number of possibly unnamed objects in a state-dependent fashion. We contribute to the further exploration of the boundary between decidability and undecidability for Golog, showing that for acyclic theories in the two-variable fragment of first-order logic, verification of CTL properties of programs over ground actions is decidable.

The verification problem for action logic programs with non-terminating behaviour is in general undecidable. In this paper, we consider a restricted setting in which the problem becomes decidable. On the one hand, we abstract from the actual execution sequences of a non-terminating program by considering infinite sequences of actions defined by a Büchi automaton. On the other hand, we assume that the logic underlying our action formalism is a decidable description logic rather than full first-order predicate logic.

The original and still a major purpose of ontologies in computer and information sciences is to serve for the semantic integration of represented content, facilitating information system interoperability. Content can be data, information, and knowledge, and it can be distributed within or across these categories. A myriad of languages is available for representation. Ontologies themselves are artifacts which are expressed in various languages. Different such languages are utilized today, including, as well-known representatives, predicate logic, subsuming first-order (predicate) logic (FOL), in particular, and higher-order (predicate) logic (HOL); the Web Ontology Language (OWL) on the basis of description logics (DL); and the Unified Modeling Language (UML). We focus primarily on languages with formally defined syntax and semantics. This overall picture immediately suggests questions of the following kinds: What is the relationship between an ontology and the language in which it is formalized? Especially, what is the impact of the formal semantics of the language on the formalized ontology? How well understood is the role of ontologies in semantic integration? Can the same ontology be represented in multiple languages and/or in distinct ways within one language? Is there an adequate understanding of whether two expressions are intensionally/conceptually equivalent and whether two ontologies furnish the same ontological commitments? One may assume that these questions are resolved. Indeed, the development and adoption of ontologies is widespread today. Ontologies are authored in a broad range of different languages, including offering equally named ontologies in distinct languages. Much research is devoted to techniques and technologies that orbit ontologies, for example, ontology matching, modularization, learning, and evolution, to name a few. Ontologies have found numerous beneficial applications, and hundreds of ontologies have been created, considering solely the context of biomedical research. For us, these observations increase the relevance of the stated questions and close relatives thereof, and raise the desire for solid theoretical underpinnings. In the literature of computer and information sciences, we have found only few approaches that tackle the foundations of ontologies and their representation to allow for answering such questions or that actually answer them. We elaborate an analysis of the subject as the first item of central contributions within this thesis. It mainly results in the identification of a vicious circularity in (i) the intended use of ontologies to mediate between formal representations and (ii) solely exploiting formal semantic notions in representing ontologies and defining ontology-based equivalence as a form of intensional/conceptual equivalence. On this basis and in order to overcome its identified limitations, we contribute a general model-theoretic semantic account, named \\\"ontological semantics\\\". This kind of semantics takes the approach of assigning arbitrary entities as referents of atomic symbols and to link syntactic constructions with corresponding ontological claims and commitments. In particular, ontological semantics targets the avoidance of encoding effects in its definition. Therefore we argue that this semantic account is well suited for interpreting formalized ontologies and for defining languages for the representation of ontologies. It is further proposed as a fundament for envisioned novel definitions of the intensional equivalence of expressions, in potential deviation from only being formally equivalent under set-theoretic semantics. The thesis is defended that a particular usage of a formalism and its respective vocabulary should be accompanied by establishing an ontological semantics that is tailored to that use of the formalism, in parallel to the formal semantics of the language, in order to capture the ontological content of the formal representation for adequate reuse in other formalisms. Accordingly, we advocate ontological semantics as a useful framework for justifying translations on an intensional basis. Despite all deviations of ontological semantics from its set-theoretic blueprint, close relationships between the two can be shown, which allow for using established FOL and DL reasoners while assuming ontological semantics.

The original and still a major purpose of ontologies in computer and information sciences is to serve for the semantic integration of represented content, facilitating information system interoperability. Content can be data, information, and knowledge, and it can be distributed within or across these categories. A myriad of languages is available for representation. Ontologies themselves are artifacts which are expressed in various languages. Different such languages are utilized today, including, as well-known representatives, predicate logic, subsuming first-order (predicate) logic (FOL), in particular, and higher-order (predicate) logic (HOL); the Web Ontology Language (OWL) on the basis of description logics (DL); and the Unified Modeling Language (UML). We focus primarily on languages with formally defined syntax and semantics. This overall picture immediately suggests questions of the following kinds: What is the relationship between an ontology and the language in which it is formalized? Especially, what is the impact of the formal semantics of the language on the formalized ontology? How well understood is the role of ontologies in semantic integration? Can the same ontology be represented in multiple languages and/or in distinct ways within one language? Is there an adequate understanding of whether two expressions are intensionally/conceptually equivalent and whether two ontologies furnish the same ontological commitments? One may assume that these questions are resolved. Indeed, the development and adoption of ontologies is widespread today. Ontologies are authored in a broad range of different languages, including offering equally named ontologies in distinct languages. Much research is devoted to techniques and technologies that orbit ontologies, for example, ontology matching, modularization, learning, and evolution, to name a few. Ontologies have found numerous beneficial applications, and hundreds of ontologies have been created, considering solely the context of biomedical research. For us, these observations increase the relevance of the stated questions and close relatives thereof, and raise the desire for solid theoretical underpinnings. In the literature of computer and information sciences, we have found only few approaches that tackle the foundations of ontologies and their representation to allow for answering such questions or that actually answer them. We elaborate an analysis of the subject as the first item of central contributions within this thesis. It mainly results in the identification of a vicious circularity in (i) the intended use of ontologies to mediate between formal representations and (ii) solely exploiting formal semantic notions in representing ontologies and defining ontology-based equivalence as a form of intensional/conceptual equivalence. On this basis and in order to overcome its identified limitations, we contribute a general model-theoretic semantic account, named \\\"ontological semantics\\\". This kind of semantics takes the approach of assigning arbitrary entities as referents of atomic symbols and to link syntactic constructions with corresponding ontological claims and commitments. In particular, ontological semantics targets the avoidance of encoding effects in its definition. Therefore we argue that this semantic account is well suited for interpreting formalized ontologies and for defining languages for the representation of ontologies. It is further proposed as a fundament for envisioned novel definitions of the intensional equivalence of expressions, in potential deviation from only being formally equivalent under set-theoretic semantics. The thesis is defended that a particular usage of a formalism and its respective vocabulary should be accompanied by establishing an ontological semantics that is tailored to that use of the formalism, in parallel to the formal semantics of the language, in order to capture the ontological content of the formal representation for adequate reuse in other formalisms. Accordingly, we advocate ontological semantics as a useful framework for justifying translations on an intensional basis. Despite all deviations of ontological semantics from its set-theoretic blueprint, close relationships between the two can be shown, which allow for using established FOL and DL reasoners while assuming ontological semantics.:* Preface ** Abstract ** Contents ** Acknowledgments ** Foreword 1 Introduction 1.1 Background 1.2 Motivations 1.3 Theses, Objectives and Scope 1.4 Outline and Contributions 1.5 Formal Preliminaries 2 Foundations on Languages, Semantics, and Ontology 2.1 Formal Syntax and Formal Semantics 2.2 The Role of Ontologies in Semantic Integration 2.3 Ontological Analysis and Meta-Ontological Architecture 2.4 Conceptualization of Categories and Relations - CR 2.5 Summary of the Analysis and Next Steps 3 Views on Set-Theoretic Semantics of Classical Predicate Logics 3.1 Tarskian Model Theory and Set-Theoretic Superstructure 3.2 Formal Semantics and Choices for Entity Postulation 3.3 Theory View of Semantics 3.4 Aims for an Ontologically Neutral Semantic Account 4 Ontological Semantics 4.1 Definition of Ontological Structures by Analogy to the Set-Theoretic Approach 4.2 Properties and Further Background for Ontological Structures in General 4.3 Ontological Models & Signature Aspects 4.4 Semantics of Predication 4.5 Semantics of Connectives and Quantifiers & Semantic Notions 4.6 Relations between Ontological and Set-Theoretic Semantics 4.7 Ontological Neutrality 5 Ontological Engineering and Applications 5.1 Formalization Method for Ontology Representation in FOL 5.2 Ontological Usage Schemes 5.3 Glimpse on Characterizing Modular Representation 5.4 Applications in the Biomedical Domain 6 Contributions to Ontologies 6.1 Formalizations of Categories and Relations - CR 6.2 Remarks on Further Contributions 6.3 Ontologies of Time 7 Conclusion and Continuation 7.1 Resume 7.2 Related Work 7.3 Conclusions 7.4 Beginnings of Future Work Appendix A Additional Preliminaries A.1 Logical Notions A.2 Axiomatic Systems of Set and Number Theory B Axioms of the CR Taxonomy in OWL B.1 Asserted OWL Class Axioms B.2 Asserted OWL Object Property Axioms C Lists of Figures and Tables C.1 List of Figures C.2 List of Tables D Abbreviations, Acronyms and Names D.1 Abbreviations D.2 Acronyms and Names E References E.1 Literature References E.2 Web References/List of URLs F Work and Author Information ** Selbständigkeitserklärung (Declaration of Authorship) ** Bibliographic Data ** Scientific Record