Indagini in Deep Inference

La tesi è uno studio di alcuni aspetti della nuova metodologia “deep inference”, abbinato ad una rivisitazione dei concetti classici di proof theory, con l'aggiunta di alcuni risultati originali orientati ad una maggior comprensione dell'argomento, nonché alle applicazioni pratiche. Nel primo capitolo vengono introdotti, seguendo un approccio di stampo formalista (con alcuni spunti personali), i concetti base della teoria della dimostrazione strutturale – cioè quella che usa strumenti combinatoriali (o “finitistici”) per studiare le proprietà delle dimostrazioni. Il secondo capitolo focalizza l'attenzione sulla logica classica proposizionale, prima introducendo il calcolo dei sequenti e dimostrando il Gentzen Hauptsatz, per passare poi al calcolo delle strutture (sistema SKS), dimostrando anche per esso un teorema di eliminazione del taglio, appositamente adattato dall'autore. Infine si discute e dimostra la proprietà di località per il sistema SKS. Un percorso analogo viene tracciato dal terzo ed ultimo capitolo, per quanto riguarda la logica lineare. Viene definito e motivato il calcolo dei sequenti lineari, e si discute del suo corrispettivo nel calcolo delle strutture. L'attenzione qui è rivolta maggiormente al problema di definire operatori non-commutativi, che mettono i sistemi in forte relazione con le algebre di processo.

Phage therapy: A software system for phage quantification and kinetic model inference.

One of the most serious problems of the modern medicine is the growing emergence of antibiotic resistance among pathogenic bacteria. In this circumstance, different and innovative approaches for treating infections caused by multidrug-resistant bacteria are imperatively required. Bacteriophage Therapy is one among the fascinating approaches to be taken into account. This consists of the use of bacteriophages, viruses that infect bacteria, in order to defeat specific bacterial pathogens. Phage therapy is not an innovative idea, indeed, it was widely used around the world in the 1930s and 1940s, in order to treat various infection diseases, and it is still used in Eastern Europe and the former Soviet Union. Nevertheless, Western scientists mostly lost interest in further use and study of phage therapy and abandoned it after the discovery and the spread of antibiotics. The advancement of scientific knowledge of the last years, together with the encouraging results from recent animal studies using phages to treat bacterial infections, and above all the urgent need for novel and effective antimicrobials, have given a prompt for additional rigorous researches in this field. In particular, in the laboratory of synthetic biology of the department of Life Sciences at the University of Warwick, a novel approach was adopted, starting from the original concept of phage therapy, in order to study a concrete alternative to antibiotics. The innovative idea of the project consists in the development of experimental methodologies, which allow to engineer a programmable synthetic phage system using a combination of directed evolution, automation and microfluidics. The main aim is to make “the therapeutics of tomorrow individualized, specific, and self-regulated” (Jaramillo, 2015). In this context, one of the most important key points is the Bacteriophage Quantification. Therefore, in this research work, a mathematical model describing complex dynamics occurring in biological systems involving continuous growth of bacteriophages, modulated by the performance of the host organisms, was implemented as algorithms into a working software using MATLAB. The developed program is able to predict different unknown concentrations of phages much faster than the classical overnight Plaque Assay. What is more, it gives a meaning and an explanation to the obtained data, making inference about the parameter set of the model, that are representative of the bacteriophage-host interaction.

Inference of Raja miraletus population structure using mitochondrial and nuclear DNA: comparing the resolution power of molecular markers in exploring species and population boundaries

This study focused on the role of oceanographic discontinuities and the presence of transitional areas in shaping the population structure and the phylogeography of the Raja miraletus species complex, coupled with the test of the effective occurrence of past speciation events. The comparisons between the Atlantic African and the North-Eastern Atlantic-Mediterranean geographic populations were unravelled using both Cytochrome Oxidase I and eight microsatellite loci. This approach guaranteed a robust dataset for the identification of a speciation event between the Atlantic African clade, corresponding to the ex Raja ocellifera nominal species, and the NE Atlantic-Mediterranean R. miraletus clade. As a matter of fact, the origin of the Atlantic Africa and the NE Atlantic-Mediterranean deep split dated about 11.74MYA and was likely due to the synergic influence currents and two upwelling areas crossing the Western African Waters. Within the Mediterranean Sea, particular attention was also paid to the transitional area represented by Adventura and Maltese Bank, that might have contributed in sustaining the connectivity of the Western and the Eastern Mediterranean geographical populations. Furthermore, the geology of the easternmost part of Sicily and the geo-morphological depression of the Calabrian Arc could have driven the differentiation of the Eastern Mediterranean Sea. Although bathymetric and oceanographic discontinuity could represent barriers to dispersal and migration between Eastern and Western Mediterranean samples, a clear and complete genetic separation among them was not detected. Results produced by this work identified a speciation event defining Raja ocellifera and R. miraletus as two different species, and describing the R. miraletus species complex as the most ancient cryptic speciation event in the family Rajidae, representing another example of how strictly connected the environment, the behavioural habits and the evolutionary and ecologic drivers are.