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.

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.