Thesis (Ph.D.)--Massachusetts Institute of Technology, Dept. of Linguistics and Philosophy, 1981. / MICROFICHE COPY AVAILABLE IN ARCHIVES AND HUMANITIES. / Bibliography: leaves 205-206. / by Fredric M. Katz. / Ph.D.

In this thesis we propose the use of Dijkstra's concept of a predicate transformer [Dij75] for the determination of database transaction safety [SS89] and the generation of simple conditions to check that a transaction will not violate the integrity constraints in the case that it is not safe. The generation of this simple condition is something that can be done statically, thus providing a mechanism for generating safe transactions. Our approach treats a database as state, a database transaction as a program, and the database's integrity constraints as a postcondition in order to use a predicate transformer [Dij75] to generate a weakest precondition. We begin by introducing a set-oriented update language for relational databases for which a predicate transformer is then defined. Subsequently, we introduce a more powerful update language for deductive databases and define a new predicate transformer to deal with this language and the more powerful integrity constraints that can be expressed using recursive rules. Next we introduce a data model with object-oriented features including methods, inheritance and dynamic overriding. We then extend the predicate transformer to handle these new features. For each of the predicate transformers, we prove that they do indeed generate a weakest precondition for a transaction and the database integrity constraints. However, the weakest precondition generated by a predicate transformer still involves much redundant checking. For several general classes of integrity constraint, including referential integrity and functional dependencies, we prove that the weakest precondition can be substantially further simplified to avoid checking things we already know to be true under the assumption that the database currently satisfies its integrity con-straints. In addition, we propose the use of the predicate transformer in combination with meta-rules that capture the exact incremental change to the database of a particular transaction. This provides a more general approach to generating simple checks for enforcing transaction safety. We show that this approach is superior to known existing previous approaches to the problem of efficient integrity constraint checking and transaction safety for relational, deductive, and deductive object-oriented databases. Finally we demonstrate several further applications of the predicate transformer to the problems of schema constraints, dynamic integrity constraints, and determining the correctness of methods for view updates. We also show how to support transactions embedded in procedural languages such as C.

<p>This thesis treats ultrasheaves, sheaves on the category of ultrafilters. </p><p>In the classical theory of ultrapowers, you start with an ultrafilter and, given a structure, you construct the ultrapower of the structure over the ultrafilter. The fundamental result is Los's theorem for ultrapowers giving the connection between what formulas are satisfied in the ultrapower and in the original structure. In this thesis we instead start with the category of ultrafilters (denoted <b>U</b>). On this category <b>U</b> we build the topos of sheaves on <b>U</b> (the ultrasheaves), which we think of as generalized ultrapowers. </p><p>The theorem for ultrapowers corresponding to Los's theorem is Moerdijk's theorem, first proved by Moerdijk for the topos Sh(<b>F</b>) of sheaves on filters. In the thesis we prove that Los's theorem follows from Moerdijk's theorem. We also investigate the exact relation between the topos of ultrasheaves and Moerdijk's topos Sh(<b>F</b>) and prove that Sh(<b>U</b>) is the double negation subtopos of Sh(<b>F</b>). </p><p>The connection between ultrapowers and ultrasheaves is investigated in detail. We also prove some model theoretic results for ultrasheaves, for instance we prove that they are saturated models. The Rudin-Keisler ordering is a tool used in set theory to study ultrafilters. It has a strong relationship to the category <b>U</b>. Blass has given a model theoretic characterization of this ordering and in the thesis we give a new proof of his result. </p><p>One common use of ultrapowers is to give non-standard models. In the thesis we prove that you can model internal set theory (IST) in the ultrasheaves. IST, introduced by Nelson, is a non-standard set theory, an axiomatic approach to non-standard mathematics.</p>

This thesis treats ultrasheaves, sheaves on the category of ultrafilters. In the classical theory of ultrapowers, you start with an ultrafilter and, given a structure, you construct the ultrapower of the structure over the ultrafilter. The fundamental result is Los's theorem for ultrapowers giving the connection between what formulas are satisfied in the ultrapower and in the original structure. In this thesis we instead start with the category of ultrafilters (denoted <b>U</b>). On this category <b>U</b> we build the topos of sheaves on <b>U</b> (the ultrasheaves), which we think of as generalized ultrapowers. The theorem for ultrapowers corresponding to Los's theorem is Moerdijk's theorem, first proved by Moerdijk for the topos Sh(<b>F</b>) of sheaves on filters. In the thesis we prove that Los's theorem follows from Moerdijk's theorem. We also investigate the exact relation between the topos of ultrasheaves and Moerdijk's topos Sh(<b>F</b>) and prove that Sh(<b>U</b>) is the double negation subtopos of Sh(<b>F</b>). The connection between ultrapowers and ultrasheaves is investigated in detail. We also prove some model theoretic results for ultrasheaves, for instance we prove that they are saturated models. The Rudin-Keisler ordering is a tool used in set theory to study ultrafilters. It has a strong relationship to the category <b>U</b>. Blass has given a model theoretic characterization of this ordering and in the thesis we give a new proof of his result. One common use of ultrapowers is to give non-standard models. In the thesis we prove that you can model internal set theory (IST) in the ultrasheaves. IST, introduced by Nelson, is a non-standard set theory, an axiomatic approach to non-standard mathematics.

Thesis (Ph. D.)--Stanford University, 1986. / Cover title. "March 1986." Includes bibliographical references.

The purpose of this study is to explore that mathematics provides a convenient formalism for studying classical database management system problems. There are two main parts in this study, devoted respectively to using mathematical theory of relations and using logical theory to study database management systems. In the first part we focus on relational model and relational algebra. The second part deals with the application of mathematical logic to database management systems, where logic may be used both as a inference system and as a representation language. The features and logical mechanisms of Prolog programming language have been studied. A sample logical database model is developed and tested, using the logic programming language Prolog. / Department of Computer Science

No description available.

Modal logics have found applications in many diferent contexts. For example, epistemic modal logics can be used to reason about security protocols, temporal modal logics can be used to reason about the correctness of distributed systems and propositional dynamic logic can reason about the correctness of programs. However, pure modal logic is expressively weak and cannot represent many interesting secondorder properties that are expressible, for example, in the μ-calculus. Here we investigate the extension of modal logics with propositional quantification modulo bisimulation (bisimulation quantification). We extend existing work on bisimulation quantified modal logic by considering the variety of logics that result by restricting the structures over which they are interpreted. We show this can be a natural extension of modal logic preserving the intuitions of both modal logic and propositional quantification. However, we also find cases where such intuitions are not preserved. We examine cases where the axioms of pure modal logic and propositional quantification are preserved and where bisimulation quantifiers preserve the decidability of modal logic. We translate a number of recent decidability results for monadic second-order logics into the context of bisimulation quantified modal logics, and show how these results can be used to generate a number of interesting bisimulation quantified modal logics.

Zugl.: Rostock, Univ., Habil.-Schr.

Thesis (Ph. D.)--Northeastern University, 2008. / Title from title page (viewed March 24, 2009). College of Computer and Information Science. Includes bibliographical references (p. 163-171).