Interactive theorem provers: issues faced as a user and tackled as a developer

Interactive theorem provers (ITP for short) are tools whose final aim is to certify proofs written by human beings. To reach that objective they have to fill the gap between the high level language used by humans for communicating and reasoning about mathematics and the lower level language that a machine is able to “understand” and process. The user perceives this gap in terms of missing features or inefficiencies. The developer tries to accommodate the user requests without increasing the already high complexity of these applications. We believe that satisfactory solutions can only come from a strong synergy between users and developers. We devoted most part of our PHD designing and developing the Matita interactive theorem prover. The software was born in the computer science department of the University of Bologna as the result of composing together all the technologies developed by the HELM team (to which we belong) for the MoWGLI project. The MoWGLI project aimed at giving accessibility through the web to the libraries of formalised mathematics of various interactive theorem provers, taking Coq as the main test case. The motivations for giving life to a new ITP are: • study the architecture of these tools, with the aim of understanding the source of their complexity • exploit such a knowledge to experiment new solutions that, for backward compatibility reasons, would be hard (if not impossible) to test on a widely used system like Coq. Matita is based on the Curry-Howard isomorphism, adopting the Calculus of Inductive Constructions (CIC) as its logical foundation. Proof objects are thus, at some extent, compatible with the ones produced with the Coq ITP, that is itself able to import and process the ones generated using Matita. Although the systems have a lot in common, they share no code at all, and even most of the algorithmic solutions are different. The thesis is composed of two parts where we respectively describe our experience as a user and a developer of interactive provers. In particular, the first part is based on two different formalisation experiences: • our internship in the Mathematical Components team (INRIA), that is formalising the finite group theory required to attack the Feit Thompson Theorem. To tackle this result, giving an effective classification of finite groups of odd order, the team adopts the SSReflect Coq extension, developed by Georges Gonthier for the proof of the four colours theorem. • our collaboration at the D.A.M.A. Project, whose goal is the formalisation of abstract measure theory in Matita leading to a constructive proof of Lebesgue’s Dominated Convergence Theorem. The most notable issues we faced, analysed in this part of the thesis, are the following: the difficulties arising when using “black box” automation in large formalisations; the impossibility for a user (especially a newcomer) to master the context of a library of already formalised results; the uncomfortable big step execution of proof commands historically adopted in ITPs; the difficult encoding of mathematical structures with a notion of inheritance in a type theory without subtyping like CIC. In the second part of the manuscript many of these issues will be analysed with the looking glasses of an ITP developer, describing the solutions we adopted in the implementation of Matita to solve these problems: integrated searching facilities to assist the user in handling large libraries of formalised results; a small step execution semantic for proof commands; a flexible implementation of coercive subtyping allowing multiple inheritance with shared substructures; automatic tactics, integrated with the searching facilities, that generates proof commands (and not only proof objects, usually kept hidden to the user) one of which specifically designed to be user driven.

The application of a new psychotherapeutic strategy for enhancing eudaimonic well-being in children with mood and anxiety disorders

The aim of the dissertation was to test the feasibility of a new psychotherapeutic protocol for treating children and adolescents with mood and anxiety disorders: Child-Well-Being Therapy (CWBT). It originates from adult Well-Being Therapy protocol (WBT) and represents a conceptual innovation for treating affective disorders. WBT is based on the multidimensional model of well-being postulated by Ryff (eudaimonic perspective), in sequential combination with cognitive-behavioral therapy (CBT). Results showed that eudaimonic well-being was impaired in children with affective disorders in comparison with matched healthy students. A first open investigation aimed at exploring the feasibility of a 8-session CWBT protocol in a group of children with emotional and behavioural disorders has been implemented. Data showed how CWBT resulted associated to symptoms reduction, together with the decrease of externalizing problems, maintained at 1-year follow-up. CWBT triggered also an improvement in psychological well-being as well as an increasing flourishing trajectory over time. Subsequently, a modified and extended version of CWBT (12-sessions) has been developed and then tested in a controlled study with 34 patients (8 to 16 years) affected by mood and anxiety disorders. They were consecutively randomized into 3 different groups: CWBT, CBT, 6-month waiting list (WL). Both treatments resulted effective in decreasing distress and in improving well-being. Moreover, CWBT was associated with higher improvement in anxiety and showed a greater recovery rate (83%) than CBT (54%). Both groups maintained beneficial effects and CWBT group displayed a lower level of distress as well as a higher positive trend in well-being scores over time. Findings need to be interpret with caution, because of study limitations, however important clinical implications emerged. Further investigations should determine whether the sequential integration of well-being and symptom-oriented strategies could play an important role in children and adolescents’ psychotherapeutic options, fostering a successful adaptation to adversities during the growth process.

The relationship between eating behavior and psychological distress among overweight and obese people: is there a role for mindfulness?

This research based on 3 indipendent studies, sought to explore the nature of the relationship between overweight/obesity, eating behaviors and psychological distress; the construct of Mindful eating trough the validation of the Italian adaptation of the Mindful Eating Questionnaire (MEQ); the role of mindfulnessand mindful eating as respectively potential mediator and moderator between overeating behavior (binge eating and emotional overeating) and negative outcomes (psychological distress, body dissatisfaction). All the samples were divided in normal weight, overweight and obese according to BMI categories. STUDY1: In a sample of 691 subjects (69.6% female, mean aged 39.26 years) was found that BMI was not associated with psychological distress, whereas binge eating increases the psychopathological level. BMI and male gender represent negative predictors of psychological distress, but certain types of overeating (i.e., NES/grazing, overeating during or out of meals, and guilt/restraint) result as positive predictors.. STUDY 2 : A sample of 1067 subjects (61.4% female, mean aged 34 years) was analized. The Italian MEQ resulted in a 26-item 4-factor model measuring Disinhibition, Awareness, Distraction, and Emotional response. Internal consistency and test-retest reliability were acceptable MEQ correlated positively with mindfulness (FMI) and it was associated with sociodemographic variables, BMI, meditation. type of exercise and diet. STUDY 3, based on a sample of 502 subjects (68.8% female, mean aged 39.42 years) showed that MEQ and FMI negatively correlated with BES, EOQ, SCL-90-R, and BIAQ. Obese people showed lower level of mindful eating and higher levels of binge eating, emotional overeating, and body dissatisfaction, compared to the other groups Mindfulness resulted to partially mediates the relationship between a) binge eating and psychological distress, b) emotional overeating and psychological distress, c) binge eating and mental well-being, d) emotional overeating and menal well-being. Mindful eating was a moderator only in the relationship between emotional overeating and body dissatisfaction.

Aerobic biodegradation of chlorinated solvents and plastics in batch and continuous-flow bioreactors: process development, and identification of suitable chemical pre-Treatments

The purpose of the first part of the research activity was to develop an aerobic cometabolic process in packed bed reactors (PBR) to treat real groundwater contaminated by trichloroethylene (TCE) and 1,1,2,2-tetrachloroethane (TeCA). In an initial screening conducted in batch bioreactors, different groundwater samples from 5 wells of the contaminated site were fed with 5 growth substrates. The work led to the selection of butane as the best growth substrate, and to the development and characterization from the site’s indigenous biomass of a suspended-cell consortium capable to degrade TCE with a 90 % mineralization of the organic chlorine. A kinetic study conducted in batch and continuous flow PBRs and led to the identification of the best carrier. A kinetic study of butane and TCE biodegradation indicated that the attached-cell consortium is characterized by a lower TCE specific degredation rates and by a lower level of mutual butane-TCE inhibition. A 31 L bioreactor was designed and set up for upscaling the experiment. The second part of the research focused on the biodegradation of 4 polymers, with and with-out chemical pre-treatments: linear low density polyethylene (LLDPE), polyethylene (PP), polystyrene (PS) and polyvinyl chloride (PVC). Initially, the 4 polymers were subjected to different chemical pre-treatments: ozonation and UV/ozonation, in gaseous and aqueous phase. It was found that, for LLDPE and PP, the coupling UV and ozone in gas phase is the most effective way to oxidize the polymers and to generate carbonyl groups on the polymer surface. In further tests, the effect of chemical pretreatment on polyner biodegrability was studied. Gas-phase ozonated and virgin polymers were incubated aerobically with: (a) a pure strain, (b) a mixed culture of bacteria; and (c) a fungal culture, together with saccharose as a co-substrate.

Retrieval of trace gases vertical profile in the lower atmosphere combining. Differential Optical Absorption Spectroscopy with radiative transfer models

The motivation for the work presented in this thesis is to retrieve profile information for the atmospheric trace constituents nitrogen dioxide (NO2) and ozone (O3) in the lower troposphere from remote sensing measurements. The remote sensing technique used, referred to as Multiple AXis Differential Optical Absorption Spectroscopy (MAX-DOAS), is a recent technique that represents a significant advance on the well-established DOAS, especially for what it concerns the study of tropospheric trace consituents. NO2 is an important trace gas in the lower troposphere due to the fact that it is involved in the production of tropospheric ozone; ozone and nitrogen dioxide are key factors in determining the quality of air with consequences, for example, on human health and the growth of vegetation. To understand the NO2 and ozone chemistry in more detail not only the concentrations at ground but also the acquisition of the vertical distribution is necessary. In fact, the budget of nitrogen oxides and ozone in the atmosphere is determined both by local emissions and non-local chemical and dynamical processes (i.e. diffusion and transport at various scales) that greatly impact on their vertical and temporal distribution: thus a tool to resolve the vertical profile information is really important. Useful measurement techniques for atmospheric trace species should fulfill at least two main requirements. First, they must be sufficiently sensitive to detect the species under consideration at their ambient concentration levels. Second, they must be specific, which means that the results of the measurement of a particular species must be neither positively nor negatively influenced by any other trace species simultaneously present in the probed volume of air. Air monitoring by spectroscopic techniques has proven to be a very useful tool to fulfill these desirable requirements as well as a number of other important properties. During the last decades, many such instruments have been developed which are based on the absorption properties of the constituents in various regions of the electromagnetic spectrum, ranging from the far infrared to the ultraviolet. Among them, Differential Optical Absorption Spectroscopy (DOAS) has played an important role. DOAS is an established remote sensing technique for atmospheric trace gases probing, which identifies and quantifies the trace gases in the atmosphere taking advantage of their molecular absorption structures in the near UV and visible wavelengths of the electromagnetic spectrum (from 0.25 μm to 0.75 μm). Passive DOAS, in particular, can detect the presence of a trace gas in terms of its integrated concentration over the atmospheric path from the sun to the receiver (the so called slant column density). The receiver can be located at ground, as well as on board an aircraft or a satellite platform. Passive DOAS has, therefore, a flexible measurement configuration that allows multiple applications. The ability to properly interpret passive DOAS measurements of atmospheric constituents depends crucially on how well the optical path of light collected by the system is understood. This is because the final product of DOAS is the concentration of a particular species integrated along the path that radiation covers in the atmosphere. This path is not known a priori and can only be evaluated by Radiative Transfer Models (RTMs). These models are used to calculate the so called vertical column density of a given trace gas, which is obtained by dividing the measured slant column density to the so called air mass factor, which is used to quantify the enhancement of the light path length within the absorber layers. In the case of the standard DOAS set-up, in which radiation is collected along the vertical direction (zenith-sky DOAS), calculations of the air mass factor have been made using “simple” single scattering radiative transfer models. This configuration has its highest sensitivity in the stratosphere, in particular during twilight. This is the result of the large enhancement in stratospheric light path at dawn and dusk combined with a relatively short tropospheric path. In order to increase the sensitivity of the instrument towards tropospheric signals, measurements with the telescope pointing the horizon (offaxis DOAS) have to be performed. In this circumstances, the light path in the lower layers can become very long and necessitate the use of radiative transfer models including multiple scattering, the full treatment of atmospheric sphericity and refraction. In this thesis, a recent development in the well-established DOAS technique is described, referred to as Multiple AXis Differential Optical Absorption Spectroscopy (MAX-DOAS). The MAX-DOAS consists in the simultaneous use of several off-axis directions near the horizon: using this configuration, not only the sensitivity to tropospheric trace gases is greatly improved, but vertical profile information can also be retrieved by combining the simultaneous off-axis measurements with sophisticated RTM calculations and inversion techniques. In particular there is a need for a RTM which is capable of dealing with all the processes intervening along the light path, supporting all DOAS geometries used, and treating multiple scattering events with varying phase functions involved. To achieve these multiple goals a statistical approach based on the Monte Carlo technique should be used. A Monte Carlo RTM generates an ensemble of random photon paths between the light source and the detector, and uses these paths to reconstruct a remote sensing measurement. Within the present study, the Monte Carlo radiative transfer model PROMSAR (PROcessing of Multi-Scattered Atmospheric Radiation) has been developed and used to correctly interpret the slant column densities obtained from MAX-DOAS measurements. In order to derive the vertical concentration profile of a trace gas from its slant column measurement, the AMF is only one part in the quantitative retrieval process. One indispensable requirement is a robust approach to invert the measurements and obtain the unknown concentrations, the air mass factors being known. For this purpose, in the present thesis, we have used the Chahine relaxation method. Ground-based Multiple AXis DOAS, combined with appropriate radiative transfer models and inversion techniques, is a promising tool for atmospheric studies in the lower troposphere and boundary layer, including the retrieval of profile information with a good degree of vertical resolution. This thesis has presented an application of this powerful comprehensive tool for the study of a preserved natural Mediterranean area (the Castel Porziano Estate, located 20 km South-West of Rome) where pollution is transported from remote sources. Application of this tool in densely populated or industrial areas is beginning to look particularly fruitful and represents an important subject for future studies.

Metamorfismo ercinico di bassa-pressione: evoluzione tettonico-metamorfica del complesso di mandatoriccio (massiccio della Sila - Calabria)

Low-pressure/high-temperature (LP/HT) metamorphic belts are characterised by rocks that experienced abnormal heat flow in shallow crustal levels (T > 600 °C; P < 4 kbar) resulting in anomalous geothermal gradients (60-150 °C/km). The abnormal amount of heat has been related to crustal underplating of mantle-derived basic magmas or to thermal perturbation linked to intrusion of large volumes of granitoids in the intermediate crust. In particular, in this latter context, magmatic or aqueous fluids are able to transport relevant amounts of heat by advection, thus favouring regional LP/HT metamorphism. However, the thermal perturbation consequent to heat released by cooling magmas is responsible also for contact metamorphic effects. A first problem is that time and space relationships between regional LP/HT metamorphism and contact metamorphism are usually unclear. A second problem is related to the high temperature conditions reached at different crustal levels. These, in some cases, can completely erase the previous metamorphic history. Notwithstanding this problem is very marked in lower crustal levels, petrologic and geochronologic studies usually concentrate in these attractive portions of the crust. However, only in the intermediate/upper-crustal levels of a LP/HT metamorphic belt the tectono-metamorphic events preceding the temperature peak, usually not preserved in the lower crustal portions, can be readily unravelled. The Hercynian Orogen of Western Europe is a well-documented example of a continental collision zone with widespread LP/HT metamorphism, intense crustal anatexis and granite magmatism. Owing to the exposure of a nearly continuous cross-section of the Hercynian continental crust, the Sila massif (northern Calabria) represents a favourable area to understand large-scale relationships between granitoids and LP/HT metamorphic rocks, and to discriminate regional LP/HT metamorphic events from contact metamorphic effects. Granulite-facies rocks of the lower crust and greenschist- to amphibolite-facies rocks of the intermediate-upper crust are separated by granitoids emplaced into the intermediate level during the late stages of the Hercynian orogeny. Up to now, advanced petrologic studies have been focused mostly in understanding P-T evolution of deeper crustal levels and magmatic bodies, whereas the metamorphic history of the shallower crustal levels is poorly constrained. The Hercynian upper crust exposed in Sila has been subdivided in two different metamorphic complexes by previous authors: the low- to very low-grade Bocchigliero complex and the greenschist- to amphibolite-facies Mandatoriccio complex. The latter contains favourable mineral assemblages in order to unravel the tectono-metamorphic evolution of the Hercynian upper crust. The Mandatoriccio complex consists mainly of metapelites, meta-arenites, acid metavolcanites and metabasites with rare intercalations of marbles and orthogneisses. Siliciclastic metasediments show a static porphyroblastic growth mainly of biotite, garnet, andalusite, staurolite and muscovite, whereas cordierite and fibrolite are less common. U-Pb ages and internal features of zircons suggest that the protoliths of the Mandatoriccio complex formed in a sedimentary basin filled by Cambrian to Silurian magmatic products as well as by siliciclastic sediments derived from older igneous and metamorphic rocks. In some localities, metamorphic rocks are injected by numerous aplite/pegmatite veins. Small granite bodies are also present and are always associated to spotted schists with large porphyroblasts. They occur along a NW-SE trending transcurrent cataclastic fault zone, which represents the tectonic contact between the Bocchigliero and the Mandatoriccio complexes. This cataclastic fault zone shows evidence of activity at least from middle-Miocene to Recent, indicating that brittle deformation post-dated the Hercynian orogeny. P-T pseudosections show that micaschists and paragneisses of the Mandatoriccio complex followed a clockwise P-T path characterised by four main prograde phases: thickening, peak-pressure condition, decompression and peak-temperature condition. During the thickening phase, garnet blastesis started up with spessartine-rich syntectonic core developed within micaschists and paragneisses. Coevally (340 ± 9.6 Ma), mafic sills and dykes injected the upper crustal volcaniclastic sedimentary sequence of the Mandatoriccio complex. After reaching the peak-pressure condition (≈4 kbar), the upper crust experienced a period of deformation quiescence marked by the static overgrowths of S2 by Almandine-rich-garnet rims and by porphyroblasts of biotite and staurolite. Probably, this metamorphic phase is related to isotherms relaxation after the thickening episode recorder by the Rb/Sr isotopic system (326 ± 6 Ma isochron age). The post-collisional period was mainly characterised by decompression with increasing temperature. This stage is documented by the andalusite+biotite coronas overgrown on staurolite porphyroblasts and represents a critical point of the metamorphic history, since metamorphic rocks begin to record a significant thermal perturbation. Peak-temperature conditions (≈620 °C) were reached at the end of this stage. They are well constrained by some reaction textures and mineral assemblages observed almost exclusively within paragneisses. The later appearance of fibrolitic sillimanite documents a small excursion of the P-T path across the And-Sil boundary due to the heating. Stephanian U-Pb ages of monazite crystals from the paragneiss, can be related to this heating phase. Similar monazite U-Pb ages from the micaschist combined with the lack of fibrolitic sillimanite suggest that, during the same thermal perturbation, micaschists recorded temperatures slightly lower than those reached by paragneisses. The metamorphic history ended with the crystallisation of cordierite mainly at the expense of andalusite. Consequently, the Ms+Bt+St+And+Sill+Crd mineral assemblage observed in the paragneisses is the result of a polyphasic evolution and is characterised by the metastable persistence of the staurolite in the stability fields of the cordierite. Geologic, geochronologic and petrographic data suggest that the thermal peak recorded by the intermediate/upper crust could be strictly connected with the emplacement of large amounts of granitoid magmas in the middle crust. Probably, the lithospheric extension in the relatively heated crust favoured ascent and emplacement of granitoids and further exhumation of metamorphic rocks. After a comparison among the tectono-metamorphic evolutions of the different Hercynian crustal levels exposed in Sila, it is concluded that the intermediate/upper crustal level offers the possibility to reconstruct a more detailed tectono-metamorphic history. The P-T paths proposed for the lower crustal levels probably underestimate the amount of the decompression. Apart from these considerations, the comparative analysis indicates that P-T paths at various crustal levels in the Sila cross section are well compatible with a unique geologic scenario, characterized by post-collisional extensional tectonics and magmas ascent.

Sea Level Variations from Decades to Millennia: A few Case Studies

The main goals of this Ph.D. study are to investigate the regional and global geophysical components related to present polar ice melting and to provide independent cross validation checks of GIA models using both geophysical data detected by satellite mission, and geological observations from far field sites, in order to determine a lower and upper bound of uncertainty of GIA effect. The subject of this Thesis is the sea level change from decades to millennia scale. Within ice2sea collaboration, we developed a Fortran numerical code to analyze the local short-term sea level change and vertical deformation resulting from the loss of ice mass. This method is used to investigate polar regions: Greenland and Antarctica. We have used mass balance based on ICESat data for Greenland ice sheet and a plausible mass balance for Antarctic ice sheet. We have determined the regional and global fingerprint of sea level variations, vertical deformations of the solid surface of the Earth and variations of shape of the geoid for each ice source mentioned above. The coastal areas are affected by the long wavelength component of GIA process. Hence understanding the response of the Earth to loading is crucial in various contexts. Based on the hypothesis that Earth mantle materials obey to a linear rheology, and that the physical parameters of this rheology can be only characterized by their depth dependence, we investigate the Glacial Isostatic Effect upon the far field sites of Mediterranean area using an improved SELEN program. We presented new and revised observations for archaeological fish tanks located along the Tyrrhenian and Adriatic coast of Italy and new RSL for the SE Tunisia. Spatial and temporal variations of the Holocene sea levels studied in central Italy and Tunisia, provided important constraints on the melting history of the major ice sheets.