GLyC - Logic, Language and Computability Research Group

Finished Master's Theses

  • Upper bound for the length of bad sequences in the majoring ordering with an application to complexity of decision problems in tree automata, by Gabriel Senno (supervisor: Santiago Figueira).
    We obtain tight upper bounds, in terms of the Fast Growing Hierarchy for the length of controlled decreasing sequences of multisets over the natural multiset ordering. Then we study the majoring ordering, linearize it into the multiset well-order, and obtain an upper bound for the length of controlled bad sequences over the majoring ordering. We finally apply this result to upper-bound the computational complexity of the emptiness problem for ATRA, a class of automata over data trees.
  • About the length of controlled bad sequences over well-quasi-orders, by Sergio Abriola (supervisor: Santiago Figueira).
    In this thesis we study upper and lower bounds for the length of controlled bad sequences over some well-quasi-orders, and we clasify these bounds in the Fast Growing Hierarchy. We give a constructive and simple proof of Dickson's Lemma which allows us to bound the maximum length of controlled bad sequences of tuples of natural numbers with the product ordering. We also study the majoring ordering over finite sets of tuples, and the multiset ordering over multisets of tuples.
    [Download (in spanish)]
  • Bisimulations on Neighbourhood Semantics, by Diego Figueira (supervisor: Carlos Areces).
    In this thesis we investigate the modal logic semantics known as Neighbourhood Semantics. There are two alternative definitions that correspond to different logics, the first of which was introduced by Montague and Scott in 1970 (N_strict), and the second by van Benthem some years later (N_loose). We study and define the notion of bisimulation in both logics, and observe that N_strict has a complex bisimulation. For this logic we analyse two extensions defining in each case the corresponding bisimulation. We arrive to an intuitive notion of bisimulation for the classical extension of the basic language with the universal modality: N_strict(E). In the final part of this work, we study the computational complexity of the satisfiability problem (SAT) of each logic. We show that SAT-N_loose is in NP (and therefore NP-Complete ), and that SAT-N_strict(E) has an EXP-Time upper-bound.
    [Download (in spanish)]
  • Ordered Resolution with Selection for the Logic H(@), by Daniel Gorín (supervisor: Carlos Areces)
    In this thesis we provide an ordered resolution calculus for the basic hybrid logic H(@). We prove that it is complete even if selection functions are used. Furthermore, we show how to turn this calculus into an effective decision procedure for the logic. Finally, we report on initial experiments using an automated theorem proved based on this calculus.
    [Download (in spanish)]
  • Description Logics with Parametric Model Checking, by Julián Méndez (supervisor: Carlos Areces)
    This thesis is a study of description logics with model checking of first order parametric models. Description logics are a family of less expressive formalisms than first order logic. Each description logic is characterized by its concept and role constructors. Concepts work as unary predicates and roles as binary predicates. An important field of interest of description logics is the one that incorporates concrete domains [Baader et al., 2003] for concept construction. A concrete domain is a pair formed by a domain and set of predicate names on that domain. An example of concrete domain is the set of real numbers with the usual comparison relations, and the relations corresponding to the usual arithmetic operations. In this thesis, the use of concrete domains is replaced by the use of the so-called “parametric models”, which are first order models. The resulting logic after this replacement is a new logic that includes a new concept constructor that allows to relate this logic with model checking of parametric models. The automated proving of this logic is also analyzed considering the use of tableau methods. In addition, there is a comparison between description logics with concrete domains and description logics with model checking of parametric models. A module for model checking is implemented and that module could be connected to automated provers like RACER.
    [Download (in spanish)]
  • On the Algorithmic Entropy of Abstract Objects, by Mariano Moscato (supervisors: Verónica Becher and Santiago Figueira)
    In this thesis we show that Chaitin's program size complexity theory conceived for words over a finite alphabet can be extended to other universes and we give sufficient conditions for such extensions to hold. These conditions require a good representation function mapping abstracts objects into words. For those universes admitting a good representation, a natural definition of complexity is induced, which can be interpreted as an algorithmic entropy, as it happens with Chaitin's complexity. In particular, the universe of finite sets of natural numbers and the universe of databases comply with the sufficient conditions we give. In contrast, the universe of partial recursive functions does not.
    [Download (in spanish)]
  • Turing's unpublished algorithm for normal numbers, by Rafael Picchi (supervisors: Verónica Becher and Santiago Figueira)
    In an unpublished manuscript Alan Turing gave a computable construction to show that absolutely normal real numbers between 0 and 1 have Lebesgue measure 1; furthermore, he gave an algorithm for computing instances in this set. We complete his manuscript by giving full proofs and correcting minor errors. While doing this, we recreate Turing's ideas as accurately as possible. One of his original lemmas remained unproved but we have replaced it with a weaker lemma that still allows us to maintain Turing's proof idea and obtain his result.
    [Download (in spanish)]
  • Thermodynamic Cost in Reversible Turing Machines, by José Orlicki (supervisor: Verónica Becher)
    Reversible Turing machines enable the implementation of injective recursive partial functions without information-loosing steps in the computations. In this thesis are detailed the different possibilities available to define reversible Universal Turing machines and how this definitions lead to functions related to Kolmogorov complexity as introduced by Vitányi.
    [Download (in spanish)]
  • Automatic File Classification Based on Vitányi's Universal Similarity Metric, by Martín Urtasun and Alejo Capparelli (supervisors: Verónica Becher and Santiago Figueira)
    Paul Vitányi (CWI Amsterdam) conceived a new method for classifying files based on Kolmogorov complexity. This method is based on the following two concepts: a definition of a universal similarity metric between sequences of symbols (files) based on Kolmogorov complexity, and an algorithm which interprets the similarity distance matrix between every pair of documents and generates the clustering of the sample. Since the notion of similarity is not computable, Vitányi's idea was to approximate it with standard text compressors, such as GZIP or BZIP2. In this work we introduce a new clustering algorithm which is applied to the mentioned method for automatic classification of files. We implemented Vitányi's method and tested it with many samples (including fragments from the Bible in different languages, newspaper articles, literary texts, source code of different programming languages, etc.) and obtained excellent results.
    [Download (in spanish)]