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.

Microrganismi probiotici per le piante: una strategia di riduzione degli input nella coltura del pomodoro col metodo biologico

In the recent years, consumers became more aware and sensible in respect to environment and food safety matters. They are more and more interested in organic agriculture and markets and tend to prefer ‘organic’ products more than their traditional counterparts. To increase the quality and reduce the cost of production in organic and low-input agriculture, the 6FP-European “QLIF” project investigated the use of natural products such as bio-inoculants. They are mostly composed by arbuscular mycorrhizal fungi and other microorganisms, so-called “plant probiotic” microorganisms (PPM), because they help keeping an high yield, even under abiotic and biotic stressful conditions. Italian laws (DLgs 217, 2006) have recently included them as “special fertilizers”. This thesis focuses on the use of special fertilizers when growing tomatoes with organic methods in open field conditions, and the effects they induce on yield, quality and microbial rhizospheric communities. The primary objective was to achieve a better understanding of how plant-probiotic micro-flora management could buffer future reduction of external inputs, while keeping tomato fruit yield, quality and system sustainability. We studied microbial rhizospheric communities with statistical, molecular and histological methods. This work have demonstrated that long-lasting introduction of inoculum positively affected micorrhizal colonization and resistance against pathogens. Instead repeated introduction of compost negatively affected tomato quality, likely because it destabilized the ripening process, leading to over-ripening and increasing the amount of not-marketable product. Instead. After two years without any significant difference, the third year extreme combinations of inoculum and compost inputs (low inoculum with high amounts of compost, or vice versa) increased mycorrhizal colonization. As a result, in order to reduce production costs, we recommend using only inoculum rather than compost. Secondly, this thesis analyses how mycorrhizal colonization varies in respect to different tomato cultivars and experimental field locations. We found statistically significant differences between locations and between arbuscular colonization patterns per variety. To confirm these histological findings, we started a set of molecular experiments. The thesis discusses preliminary results and recommends their continuation and refinement to gather the complete results.

Study of the inter-annual variability of particle vertical fluxes in two moorings in the Ross Sea (Antarctica)

The most ocean - atmosphere exchanges take place in polar environments due to the low temperatures which favor the absorption processes of atmospheric gases, in particular CO2. For this reason, the alterations of biogeochemical cycles in these areas can have a strong impact on the global climate. With the aim of contributing to the definition of the mechanisms regulating the biogeochemical fluxes we have analyzed the particles collected in the Ross Sea in different years (ROSSMIZE, BIOSESO 1 and 2, ROAVERRS and ABIOCLEAR projects) in two sites (mooring A and B). So it has been developed a more efficient method to prepare sediment trap samples for the analyses. We have also processed satellite data of sea ice, chlorophyll a and diatoms concentration. At both sites, in each year considered, there was a high seasonal and inter-annual variability of biogeochemical fluxes closely correlated with sea ice cover and primary productivity. The comparison between the samples collected at mooring A and B in 2008 highlighted the main differences between these two sites. Particle fluxes at Mooring A, located in a polynia area, are higher than mooring B ones and they happen about a month before. In the mooring B area it has been possible to correlate the particles fluxes to the ice concentration anomalies and with the atmospheric changes in response to El Niño Southern Oscillations. In 1996 and 1999, years subjected to La Niña, the concentrations of sea ice in this area have been less than in 1998, year subjected to El Niño. Inverse correlation was found for 2005 and 2008. In the mooring A area significant differences in mass and biogenic fluxes during 2005 and 2008 has been recorded. This allowed to underline the high variability of lateral advection processes and to connect them to the physical forcing.

Teoria e pratica dell'architettura solare - Morfologia, rendimento, strategia progettuale

La recente Direttiva 31/2010 dell’Unione Europea impone agli stati membri di riorganizzare il quadro legislativo nazionale in materia di prestazione energetica degli edifici, affinchè tutte le nuove costruzioni presentino dal 1° gennaio 2021 un bilancio energetico tendente allo zero; termine peraltro anticipato al 1° gennaio 2019 per gli edifici pubblici. La concezione di edifici a energia “quasi” zero (nZEB) parte dal presupposto di un involucro energeticamente di standard passivo per arrivare a compensare, attraverso la produzione preferibilmente in sito di energia da fonti rinnovabili, gli esigui consumi richiesti su base annuale. In quest’ottica la riconsiderazione delle potenzialità dell’architettura solare individua degli strumenti concreti e delle valide metodologie per supportare la progettazione di involucri sempre più performanti che sfruttino pienamente una risorsa inesauribile, diffusa e alla portata di tutti come quella solare. Tutto ciò in considerazione anche della non più procrastinabile necessità di ridurre il carico energetico imputabile agli edifici, responsabili come noto di oltre il 40% dei consumi mondiali e del 24% delle emissioni di gas climalteranti. Secondo queste premesse la ricerca pone come centrale il tema dell’integrazione dei sistemi di guadagno termico, cosiddetti passivi, e di produzione energetica, cosiddetti attivi, da fonte solare nell’involucro architettonico. Il percorso sia analitico che operativo effettuato si è posto la finalità di fornire degli strumenti metodologici e pratici al progetto dell’architettura, bisognoso di un nuovo approccio integrato mirato al raggiungimento degli obiettivi di risparmio energetico. Attraverso una ricognizione generale del concetto di architettura solare e dei presupposti teorici e terminologici che stanno alla base della stessa, la ricerca ha prefigurato tre tipologie di esito finale: una codificazione delle morfologie ricorrenti nelle realizzazioni solari, un’analisi comparata del rendimento solare nelle principali aggregazioni tipologiche edilizie e una parte importante di verifica progettuale dove sono stati applicati gli assunti delle categorie precedenti