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.

Reasoning with incomplete and imprecise preferences

Preferences are present in many real life situations but it is often difficult to quantify them giving a precise value. Sometimes preference values may be missing because of privacy reasons or because they are expensive to obtain or to produce. In some other situations the user of an automated system may have a vague idea of whats he wants. In this thesis we considered the general formalism of soft constraints, where preferences play a crucial role and we extended such a framework to handle both incomplete and imprecise preferences. In particular we provided new theoretical frameworks to handle such kinds of preferences. By admitting missing or imprecise preferences, solving a soft constraint problem becomes a different task. In fact, the new goal is to find solutions which are the best ones independently of the precise value the each preference may have. With this in mind we defined two notions of optimality: the possibly optimal solutions and the necessary optimal solutions, which are optimal no matter we assign a precise value to a missing or imprecise preference. We provided several algorithms, bases on both systematic and local search approaches, to find such kind of solutions. Moreover, we also studied the impact of our techniques also in a specific class of problems (the stable marriage problems) where imprecision and incompleteness have a specific meaning and up to now have been tackled with different techniques. In the context of the classical stable marriage problem we developed a fair method to randomly generate stable marriages of a given problem instance. Furthermore, we adapted our techniques to solve stable marriage problems with ties and incomplete lists, which are known to be NP-hard, obtaining good results both in terms of size of the returned marriage and in terms of steps need to find a solution.

Novel tools for conservation genetics in marine fish: population structure and evolution of the European hake (Merluccius merluccius) inferred by SNP variation and applications to traceability

The research presented in my PhD thesis is part of a wider European project, FishPopTrace, focused on traceability of fish populations and products. My work was aimed at developing and analyzing novel genetic tools for a widely distributed marine fish species, the European hake (Merluccius merluccius), in order to investigate population genetic structure and explore potential applications to traceability scenarios. A total of 395 SNPs (Single Nucleotide Polymorphisms) were discovered from a massive collection of Expressed Sequence Tags, obtained by high-throughput sequencing, and validated on 19 geographic samples from Atlantic and Mediterranean. Genome-scan approaches were applied to identify polymorphisms on genes potentially under divergent selection (outlier SNPs), showing higher genetic differentiation among populations respect to the average observed across loci. Comparative analysis on population structure were carried out on putative neutral and outlier loci at wide (Atlantic and Mediterranean samples) and regional (samples within each basin) spatial scales, to disentangle the effects of demographic and adaptive evolutionary forces on European hake populations genetic structure. Results demonstrated the potential of outlier loci to unveil fine scale genetic structure, possibly identifying locally adapted populations, despite the weak signal showed from putative neutral SNPs. The application of outlier SNPs within the framework of fishery resources management was also explored. A minimum panel of SNP markers showing maximum discriminatory power was selected and applied to a traceability scenario aiming at identifying the basin (and hence the stock) of origin, Atlantic or Mediterranean, of individual fish. This case study illustrates how molecular analytical technologies have operational potential in real-world contexts, and more specifically, potential to support fisheries control and enforcement and fish and fish product traceability.

Land use change to perennial energy crops in Northern Italy: Effects on soil organic carbon sequestration and distribution, soil enzyme activities and microbial communities.

Studies on soil organic carbon (SOC) sequestration in perennial energy crops are available for North-Central Europe, while there is insufficient information for Southern Europe. This research was conducted in the Po Valley, a Mediterranean-temperate zone characterised by low SOC levels, due to intensive management. The aim was to assess the factors influencing SOC sequestration and its distribution through depth and within soil fractions, after a 9-year old conversion from two annual systems to Miscanthus (Miscanthus × giganteus) and giant reed (Arundo donax). The 13C natural abundance was used to evaluate the amount of SOC in annual and perennial species, and determine the percentage of carbon derived from perennial crops. SOC was significantly higher under perennial species, especially in the topsoil (0-0.15 m). After 9 years, the amount of C derived from Miscanthus was 18.7 Mg ha-1, mostly stored at 0-0.15 m, whereas the amount of C derived from giant reed was 34.7 Mg ha-1, evenly distributed through layers. Physical soil fractionation was combined with 13C abundance analysis. C derived from perennial crops was mainly found in macroaggregates. Under giant reed, more newly derived-carbon was stored in microaggregates and mineral fraction than under Miscanthus. A molecular approach based on denaturing gradient gel electrophoresis (DGGE) allowed to evaluate changes on microbial community, after the introduction of perennial crops. Functional aspects were investigated by determining relevant soil enzymes (β-glucosidase, urease, alkaline phosphatase). Perennial crops positively stimulated these enzymes, especially in the topsoil. DGGE profiles revealed that community richness was higher in perennial crops; Shannon index of diversity was influenced only by depth. In conclusion, Miscanthus and giant reed represent a sustainable choice for the recovery of soils exhausted by intensive management, also in Mediterranean conditions and this is relevant mainly because this geographical area is notoriously characterised by a rapid turnover of SOC.