Browsing by Subject "Computer Science BS CompSc"

Now showing 1 - 3 of 3
  • Thumbnail Image
    Item
    Automating the Proofs of Strengthening Lemmas in the Abella Proof Assistant
    (2017) Michaelson, Dawn;
    In logical reasoning, it is often the case that only some of a collection of assumptions are needed to reach a conclusion. A strengthening lemma is an assertion that a given conclusion is independent in this sense of a particular assumption. Strengthening lemmas underlie many useful techniques for simplifying proofs in automated and interactive theorem-provers. For example, they underlie a mechanism called subordination that is useful in determining that expressions of a particular type cannot contain objects of another type and in thereby reducing the number of cases to be considered in proving universally quanti ed statements. This thesis concerns the automation of the proofs of strengthening lemmas in a speci cation logic called the logic of hereditary Harrop formulas (HOHH). The Abella Proof Assistant embeds this logic in a way that allows it to prove properties of both the logic itself and of speci cations written in it. Previous research has articulated a (conservative) algorithm for checking if a claimed strengthening lemma is, in fact, true. We provide here an implementation of this algorithm within the setting of Abella. Moreover, we show how to generate an actual proof of the strengthening lemma in Abella from the information computed by the algorithm; such a proof serves as a more trustworthy certifi cate of the correctness of the lemma than the algorithm itself. The results of this work have been incorporated into the Abella system in the form of a \tactic command" that can be invoked within the interactive theorem-prover and that will result in an elaboration of a proof of the lemma and its incorporation into the collection of proven facts about a given speci cation.
  • Thumbnail Image
    Item
    A Kullback-Leibler Divergence Exploration into a Look-Ahead Simulation Optimization of the Extended Compact Genetic Algorithm
    (2017) Vasquez, Nathan;
    The Kullback-Leibler Divergence of gene distributions between successive generations of the Extended Compact Genetic Algorithm (ECGA) is explored. Therein, the fragility of the algorithm’s dependability to the beginning generations’ biasing is suggested. A novel approach within the scope of the ECGA for choosing a better bias by allowing the ECGA to simulate itself is presented. It is shown that, by simulating itself, the ECGA is able to use a smaller population and evaluate fewer fitness calls while maintaining the same ability to find optimal solutions.
  • Thumbnail Image
    Item
    Using the Adelfa Proof Assistant to Construct Proofs of Programming Language Properties
    (2021-05) Luick, Daniel
    In this thesis, we demonstrate stating and proving properties of a programming language using a dependently typed lambda calculus called LF and a system called Adelfa which provides mechanized support for reasoning about statements concerning typing derivations in LF. Proving properties in this manner allows the proofs to be undertaken using a formal logic, and builds greater trust in the proofs because the details of the steps are checked mechanically. The property that we consider in our demonstration is subject reduction for the Simply Typed Lambda Calculus. The Simply Typed Lambda Calculus is the theoretical foundation for many important programming languages and more complex lambda calculi, and subject reduction is a nontrivial properties with important equivalents in these more complex systems. Therefore, this proof constitutes a nontrivial demonstration of the usefulness of LF and Adelfa for proving properties of programming languages.