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.

Modulation Techniques for Multi-Phase Converters and Control Strategies for Multi-Phase Electric Drives

The ever-increasing spread of automation in industry puts the electrical engineer in a central role as a promoter of technological development in a sector such as the use of electricity, which is the basis of all the machinery and productive processes. Moreover the spread of drives for motor control and static converters with structures ever more complex, places the electrical engineer to face new challenges whose solution has as critical elements in the implementation of digital control techniques with the requirements of inexpensiveness and efficiency of the final product. The successfully application of solutions using non-conventional static converters awake an increasing interest in science and industry due to the promising opportunities. However, in the same time, new problems emerge whose solution is still under study and debate in the scientific community During the Ph.D. course several themes have been developed that, while obtaining the recent and growing interest of scientific community, have much space for the development of research activity and for industrial applications. The first area of research is related to the control of three phase induction motors with high dynamic performance and the sensorless control in the high speed range. The management of the operation of induction machine without position or speed sensors awakes interest in the industrial world due to the increased reliability and robustness of this solution combined with a lower cost of production and purchase of this technology compared to the others available in the market. During this dissertation control techniques will be proposed which are able to exploit the total dc link voltage and at the same time capable to exploit the maximum torque capability in whole speed range with good dynamic performance. The proposed solution preserves the simplicity of tuning of the regulators. Furthermore, in order to validate the effectiveness of presented solution, it is assessed in terms of performance and complexity and compared to two other algorithm presented in literature. The feasibility of the proposed algorithm is also tested on induction motor drive fed by a matrix converter. Another important research area is connected to the development of technology for vehicular applications. In this field the dynamic performances and the low power consumption is one of most important goals for an effective algorithm. Towards this direction, a control scheme for induction motor that integrates within a coherent solution some of the features that are commonly required to an electric vehicle drive is presented. The main features of the proposed control scheme are the capability to exploit the maximum torque in the whole speed range, a weak dependence on the motor parameters, a good robustness against the variations of the dc-link voltage and, whenever possible, the maximum efficiency. The second part of this dissertation is dedicated to the multi-phase systems. This technology, in fact, is characterized by a number of issues worthy of investigation that make it competitive with other technologies already on the market. Multiphase systems, allow to redistribute power at a higher number of phases, thus making possible the construction of electronic converters which otherwise would be very difficult to achieve due to the limits of present power electronics. Multiphase drives have an intrinsic reliability given by the possibility that a fault of a phase, caused by the possible failure of a component of the converter, can be solved without inefficiency of the machine or application of a pulsating torque. The control of the magnetic field spatial harmonics in the air-gap with order higher than one allows to reduce torque noise and to obtain high torque density motor and multi-motor applications. In one of the next chapters a control scheme able to increase the motor torque by adding a third harmonic component to the air-gap magnetic field will be presented. Above the base speed the control system reduces the motor flux in such a way to ensure the maximum torque capability. The presented analysis considers the drive constrains and shows how these limits modify the motor performance. The multi-motor applications are described by a well-defined number of multiphase machines, having series connected stator windings, with an opportune permutation of the phases these machines can be independently controlled with a single multi-phase inverter. In this dissertation this solution will be presented and an electric drive consisting of two five-phase PM tubular actuators fed by a single five-phase inverter will be presented. Finally the modulation strategies for a multi-phase inverter will be illustrated. The problem of the space vector modulation of multiphase inverters with an odd number of phases is solved in different way. An algorithmic approach and a look-up table solution will be proposed. The inverter output voltage capability will be investigated, showing that the proposed modulation strategy is able to fully exploit the dc input voltage either in sinusoidal or non-sinusoidal operating conditions. All this aspects are considered in the next chapters. In particular, Chapter 1 summarizes the mathematical model of induction motor. The Chapter 2 is a brief state of art on three-phase inverter. Chapter 3 proposes a stator flux vector control for a three- phase induction machine and compares this solution with two other algorithms presented in literature. Furthermore, in the same chapter, a complete electric drive based on matrix converter is presented. In Chapter 4 a control strategy suitable for electric vehicles is illustrated. Chapter 5 describes the mathematical model of multi-phase induction machines whereas chapter 6 analyzes the multi-phase inverter and its modulation strategies. Chapter 7 discusses the minimization of the power losses in IGBT multi-phase inverters with carrier-based pulse width modulation. In Chapter 8 an extended stator flux vector control for a seven-phase induction motor is presented. Chapter 9 concerns the high torque density applications and in Chapter 10 different fault tolerant control strategies are analyzed. Finally, the last chapter presents a positioning multi-motor drive consisting of two PM tubular five-phase actuators fed by a single five-phase inverter.

Competition between evaporation and fragmentation in nuclear reactions at 15-20 AMeV beam energy

The reactions 32S+58,64Ni are studied at 14.5 AMeV. From this energy on, fragmentation begins to be a dominant process, although evaporation and fission are still present. After a selection of the collision mechanism, we show that important even-odd effects are present in the isotopic fragment distributions when the excitation energy is small. The staggering effect appears to be a universal feature of fragment production, slightly enhanced when the emission source is neutron poor. A closer look at the behavior of isotopic chains reveals that odd-even effects cannot be explained by pairing effects in the nuclear mass alone, but depend in a more complex way on the de-excitation chain.

Polymorphs solvates and co-crystals of molecular materials

The scope of my research project is to produce and characterize new crystalline forms of organic compounds, focusing the attention on co-crystals and then transferring these notions on APIs to produce co-crystals of potential interest in the pharmaceutical field. In the first part of this work co-crystallization experiments were performed using as building blocks the family of aliphatic dicarboxylic acids HOOC-(CH2)n-COOH, with n= 2-8. This class of compounds has always been an object of study because it is characterized by an interesting phenomenon of alternation of melting points: the acids with an even number of carbon atoms show a melting point higher than those with an odd one. The acids were co-crystallized with four dipyridyl molecules (formed by two pyridine rings with a different number of bridging carbon atoms) through the formation of intermolecular interactions N•••(H)O. The bases used were: 4,4’-bipyridine (BPY), 1,2-bis(4-pyridyl)ethane (BPA), 1,2-(di-4-pyridyl)ethylene (BPE) and 1,2-bis(4-pyridyl)propane (BPP). The co-crystals obtained by solution synthesis were characterized by different solid-state techniques to determine the structure and to see how the melting points in co-crystals change. In the second part of this study we tried to obtain new crystal forms of compounds of pharmaceutical interest. The APIs studied are: O-desmethylvenlafaxine, Lidocaine, Nalidixic Acid and Sulfadiazine. Each API was subjected to Polymorph Screening and Salt/Co-crystal Screening experiments to identify new crystal forms characterized by different properties. In a typical Salt/Co-crystal Screening the sample was made to react with a co-former (solid or liquid) through different methods: crystallization by solution, grinding, kneading and solid-gas reactions. The new crystal forms obtained were characterized by different solid state techniques (X-ray single crystal diffraction, X-ray powder diffraction, Differential Scanning Calorimetry, Thermogravimetric Analysis, Evolved gas analysis, FT-IR – ATR, Solid State N.M.R).

Functional and neural mechanisms of intertemporal choice

People are daily faced with intertemporal choice, i.e., choices differing in the timing of their consequences, frequently preferring smaller-sooner rewards over larger-delayed ones, reflecting temporal discounting of the value of future outcomes. This dissertation addresses two main goals. New evidence about the neural bases of intertemporal choice is provided. Following the disruption of either the medial orbitofrontal cortex or the insula, the willingness to wait for larger-delayed outcomes is affected in odd directions, suggesting the causal involvement of these areas in regulating the value computation of rewards available with different timings. These findings were also supported by a reported imaging study. Moreover, this dissertation provides new evidence about how temporal discounting can be modulated at a behavioral level through different manipulations, e.g., allowing individuals to think about the distant time, pairing rewards with aversive events, or changing their perceived spatial position. A relationship between intertemporal choice, moral judgements and aging is also discussed. All these findings link together to support a unitary neural model of temporal discounting according to which signals coming from several cortical (i.e., medial orbitofrontal cortex, insula) and subcortical regions (i.e., amygdala, ventral striatum) are integrated to represent the subjective value of both earlier and later rewards, under the top-down regulation of dorsolateral prefrontal cortex. The present findings also support the idea that the process of outcome evaluation is strictly related to the ability to pre-experience and envision future events through self-projection, the anticipation of visceral feelings associated with receiving rewards, and the psychological distance from rewards. Furthermore, taking into account the emotions and the state of arousal at the time of decision seems necessary to understand impulsivity associated with preferring smaller-sooner goods in place of larger-later goods.

q-Hook length formulas for colored labeled forests

The major index has been deeply studied from the early 1900s and recently has been generalized in different directions, such as the case of labeled forests and colored permutations. In this thesis we define new types of labelings for forests in which the labels are colored integers. We extend the definition of the flag-major index for these labelings and we present an analogue of well known major index hook length formulas. Finally, this study (which has just apparently a simple combinatoric nature) allows us to show a notion of duality for two particular families of groups obtained from the product G(r,n)×G(r,m).