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.

This work focuses on the presentation of a methodology for the development and verification of expressive ontologies. Motivated by experiences with the development of first-order logic ontologies, we call attention to the inadequacies of existing development methodologies for expressive ontologies. We attempt to incorporate pragmatic considerations inspired by our experiences while maintaining the rigorous definition and verification of requirements necessary for the development of expressive ontologies. We leverage automated reasoning tools to enable semiautomatic verification of requirements, and to assist other aspects of development where possible. In addition, we discuss the related issue of ontology quality, and formulate a set of requirements for MACLEOD - a proposed development tool that would support our lifecycle.

This work focuses on the presentation of a methodology for the development and verification of expressive ontologies. Motivated by experiences with the development of first-order logic ontologies, we call attention to the inadequacies of existing development methodologies for expressive ontologies. We attempt to incorporate pragmatic considerations inspired by our experiences while maintaining the rigorous definition and verification of requirements necessary for the development of expressive ontologies. We leverage automated reasoning tools to enable semiautomatic verification of requirements, and to assist other aspects of development where possible. In addition, we discuss the related issue of ontology quality, and formulate a set of requirements for MACLEOD - a proposed development tool that would support our lifecycle.

In this thesis we investigate the design and complexity analysis of the algorithms to solve convex programming problems under inexact first-order information. In the first part of this thesis we focus on the general non-smooth convex minimization under a stochastic oracle. We start by introducing an important algorithmic advancement in this area, namely, the development of the mirror descent stochastic approximation algorithm. The main contribution is to develop a validation procedure for this algorithm applied to stochastic programming. In the second part of this thesis we consider the Stochastic Composite Optimizaiton (SCO) which covers smooth, non-smooth and stochastic convex optimization as certain special cases. Note that the optimization algorithms that can achieve this lower bound had never been developed. Our contribution in this topic mainly consists of the following aspects. Firstly, with a novel analysis, it is demonstrated that the simple RM-SA algorithm applied to the aforementioned problems exhibits the best known so far rate of convergence. Moreover, by adapting Nesterov's optimal method, we propose an accelerated SA, which can achieve, uniformly in dimension, the theoretically optimal rate of convergence for solving this class of problems. Finally, the significant advantages of the accelerated SA over the existing algorithms are illustrated in the context of solving a class of stochastic programming problems. In the last part of this work, we extend our attention to certain deterministic optimization techniques which operate on approximate first-order information for the dual problem. In particular, we establish, for the first time in the literature, the iteration-complexity for the inexact augmented Lagrangian (I-AL) methods applied to a special class of convex programming problems.

Ce mémoire présente le résultat de mon travail de thèse sur la génération d'impliqués premiers en logique équationnelle fermée, i.e., la génération des conséquences les plus générales de formules logiques contenants des équations et des disequations entre termes sans variables. Ce mémoire est divisé en trois parties. Tout d'abord, deux calculs de génération d'impliqués sont définis. Leur complétude pour la déduction est prouvée, ce qui signifie qu'ils sont tous deux capables de générer l'ensemble des impliqués modulo redondance d'une formule équationnelle fermée. Dans une deuxième partie, une structure de données arborescente est proposée pour stocker les impliqués générés, accompagnée d'algorithmes pour déceler les redondances et couper les branches de l'arbre lorsque c'est nécessaire. Cette structure de données est adaptée aux différents types de clauses (avec et sans symboles de fonctions, avec et sans contraintes) ainsi qu'aux différentes notions de redondance utilisées dans les calculs. En effet, chaque calcul utilise un critère de redondance légèrement différent des autres. Les preuves de correction et de terminaison des algorithmes sont fournies pour chaque algorithme. Enfin, une évaluation expérimentale des différentes méthodes de génération d'impliqués premiers est réalisée. Pour cela, un prototype de ces méthodes, écrit en Ocaml est comparé à des outils de génération d'impliqués premiers récents.Les résultats de ces expériences sont utilisés pour identifier les variantes les plus efficaces des algorithmes proposés. Les résultats sont prometteurs et dans la plupart des cas, meilleurs que ceux de l'état de l'art. / The work presented in this memoir deals with the generation of prime implicates in ground equational logic, i.e., of the most general consequences of formulae containing equations and disequations between ground terms.It is divided in three parts. First, two calculi that generate implicates are defined. Their deductive-completeness is proved, meaning they can both generate all the implicates up to redundancy of equational formulae.Second, a tree data structure to store the generated implicates is proposed along with algorithms to detect redundancies and prune the branches of the tree accordingly. This data structure is adapted to the different kinds of clauses (with and without function symbols, with and without constraints) and to the various formal definitions of redundancy used in the calculi since each calculus uses different -- although similar -- redundancy criteria. Termination and correction proofs are provided with each algorithm. Finally, an experimental evaluation of the different prime implicate generation methods based on research prototypes written in Ocaml is conducted including a comparison with state-of-the-art prime implicate generation tools. This experimental study is used to identify the most efficient variants of the proposed algorithms. These show promising results overstepping the state of the art.

abstract: Natural Language Processing is a subject that combines computer science and linguistics, aiming to provide computers with the ability to understand natural language and to develop a more intuitive human-computer interaction. The research community has developed ways to translate natural language to mathematical formalisms. It has not yet been shown, however, how to automatically translate different kinds of knowledge in English to distinct formal languages. Most of the recent work presents the problem that the translation method aims to a specific formal language or is hard to generalize. In this research, I take a first step to overcome this difficulty and present two algorithms which take as input two lambda-calculus expressions G and H and compute a lambda-calculus expression F. The expression F returned by the first algorithm satisfies F@G=H and, in the case of the second algorithm, we obtain G@F=H. The lambda expressions represent the meanings of words and sentences. For each formal language that one desires to use with the algorithms, the language must be defined in terms of lambda calculus. Also, some additional concepts must be included. After doing this, given a sentence, its representation and knowing the representation of several words in the sentence, the algorithms can be used to obtain the representation of the other words in that sentence. In this work, I define two languages and show examples of their use with the algorithms. The algorithms are illustrated along with soundness and completeness proofs, the latter with respect to typed lambda-calculus formulas up to the second order. These algorithms are a core part of a natural language semantics system that translates sentences from English to formulas in different formal languages. / Dissertation/Thesis / M.S. Computer Science 2010