Thesis (Ph. D.)--Missouri University of Science and Technology, 2008. / Vita. The entire thesis text is included in file. Title from title screen of thesis/dissertation PDF file (viewed May 28, 2009) Includes bibliographical references.

Thesis (Ph. D.)--Carnegie Mellon University, 2005. / "May 2005." Includes bibliographical references.

Made available in DSpace on 2014-06-12T15:48:50Z (GMT). No. of bitstreams: 2 arquivo2717_1.pdf: 481883 bytes, checksum: bb9d70f42c1cda245b5340284b5dc431 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2011 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / Nesta tese, provamos que todo domínio infinito finitamente gerado é bi-interpretável com a estrutura dos números naturais. Usando este argumento, demonstramos que todo anel f.g. R que tem um ideal primo nilpotente I tal que R/I é um domínio é Quase-Finitamente Axiomatizável

Background: Community resilience to a disaster is a complex phenomenon studied using a variety of research lenses, such as psychological and ecological, resulting in a lack of consensus about what the key factors are that make a community resilient. Formally representing this knowledge will allow researchers to better understand the links between the knowledge generated using different lenses and help to integrate new findings into the existing body of knowledge. Objective: Using ontology engineering methods to represent this knowledge will provide a tool to aid researchers in the field. Methods: An ontology is a structured way of organizing and representing knowledge in the field of community resilience to a disaster. The model created using this method can be read by a computer, which allows a reasoner to manipulate and infer new knowledge. Results: When using these methods to structure community resilience knowledge some of the complexities and ambiguities were identified. These included semantic ambiguities, such as two distinct factors being used interchangeably or two terms being used to describe the same factor, making the distinction between what are the factors and the characteristics of those factors, and finally, the inherited characteristics and relationships associated with hierarchical relationships. Conclusions: Having the knowledge about community resilience to a disaster represented in an ontology will aid researchers when operationalizing this knowledge in the future.

Thesis. 1976. Ph.D.--Massachusetts Institute of Technology. Dept. of Philosophy. / Microfiche copy available in Archives and Humanities. / Bibliography: leaves 165-170. / Ph.D.

No description available.

Higher-Order Pushdown Automata (HOPDA) are abstract machines equipped with a nested stacks of stacks ... of stacks of stacks. Collapsible pushdown automata (CPDA) enhance these stacks with the addition of ‘links’ emanating from atomic elements to the higher-order stacks below. For trees CPDA are equi-expressive with recursion schemes, which can be viewed as simply-typed λY terms. With vanilla HOPDA, one can only capture schemes satisfying a syntactic constraint called safety. This dissertation begins with some results concerning the significance of links in terms of recursion schemes. We introduce a fine-grained notion of safety that allows us to correlate the need for links of a given order with the imposition of safety on variables of a corresponding order. This generalises some joint work with William Blum that shows we can dispense with homogeneous types when characterising safety. We complement this result with a demonstration that homogeneity by itself does not constrain the expressivity of otherwise unrestricted recursion schemes. The main results of the dissertation, however, concern the configuration graphs of CPDA. Whilst the configuration graphs of HOPDA are well understood and have decidable MSO theories (they coincide with the Caucal hierarchy), relatively little is known about the transition graphs of CPDA. It is known that they already have undecidable MSO theories at order-2, but Kartzow recently showed that 2-CPDA graphs are tree automatic and hence first-order logic is decidable at order-2. We provide a characterisation of the decidability of first-order logic on CPDA graphs in terms of quantifier-alternation and the order of CPDA stacks and the links contained within. Whilst this characterisation is fairly comprehensive, we do leave open the question of decidability for some sub-classes of CPDA. It turns out that decidability can be highly sensitive to the order of links in a stack relative to the order of the stack itself. In addition to some strong and surprising undecidability results, we also develop further Kartzow’s work on 2-CPDA. We introduce prefix-rewrite systems for nested-words that characterise the configuration graphs of both 2-CPDA and 2-HOPDA, capturing the power of collapse precisely in terms outside of the language of CPDA. It also formalises and demonstrates the inherent asymmetry of the collapse operation. This generalises the rational prefix-rewriting systems characterising conventional pushdown graphs and we believe establishes the 2-CPDA graphs as an interesting and robust class.

I explore three main points in Alfred Tarski’s Semantic Conception of Truth and the Foundation of Theoretical Semantics: (1) his physicalist program, (2) a general theory of truth, and (3) the necessity of a metalanguage when defining truth. Hartry Field argued that Tarski’s theory of truth failed to accomplish what it set out to do, which was to ground truth and semantics in physicalist terms. I argue that Tarski has been adequately defended by Richard Kirkham. Development of logic in the past three decades has created a shift away from Fregean and Russellian understandings of quantification to an independent conception of quantification in independence-friendly first-order logic. This shift has changed some of the assumptions that led to Tarski’s Impossibility Theorem.

This thesis presents a framework for understanding first-order theories by investigating their models. A common application is to help users, who are not necessarily experts in formal methods, analyze software artifacts, such as access-control policies, system configurations, protocol specifications, and software designs. The framework suggests a strategy for exploring the space of finite models of a theory via augmentation. Also, it introduces a notion of provenance information for understanding the elements and facts in models with respect to the statements of the theory. The primary mathematical tool is an information-preserving preorder, induced by the homomorphism on models, defining paths along which models are explored. The central algorithmic ideas consists of a controlled construction of the Herbrand base of the input theory followed by utilizing SMT-solving for generating models that are minimal under the homomorphism preorder. Our framework for model-exploration is realized in Razor, a model-finding assistant that provides the user with a read-eval-print loop for investigating models.

Thesis. 1978. M.S.--Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science. / MICROFICHE COPY AVAILABLE IN ARCHIVES AND ENGINEERING. / Bibliography: leaf 99. / M.S.