User interaction widgets for interactive theorem proving

Matita (that means pencil in Italian) is a new interactive theorem prover under development at the University of Bologna. When compared with state-of-the-art proof assistants, Matita presents both traditional and innovative aspects. The underlying calculus of the system, namely the Calculus of (Co)Inductive Constructions (CIC for short), is well-known and is used as the basis of another mainstream proof assistant—Coq—with which Matita is to some extent compatible. In the same spirit of several other systems, proof authoring is conducted by the user as a goal directed proof search, using a script for storing textual commands for the system. In the tradition of LCF, the proof language of Matita is procedural and relies on tactic and tacticals to proceed toward proof completion. The interaction paradigm offered to the user is based on the script management technique at the basis of the popularity of the Proof General generic interface for interactive theorem provers: while editing a script the user can move forth the execution point to deliver commands to the system, or back to retract (or “undo”) past commands. Matita has been developed from scratch in the past 8 years by several members of the Helm research group, this thesis author is one of such members. Matita is now a full-fledged proof assistant with a library of about 1.000 concepts. Several innovative solutions spun-off from this development effort. This thesis is about the design and implementation of some of those solutions, in particular those relevant for the topic of user interaction with theorem provers, and of which this thesis author was a major contributor. Joint work with other members of the research group is pointed out where needed. The main topics discussed in this thesis are briefly summarized below. Disambiguation. Most activities connected with interactive proving require the user to input mathematical formulae. Being mathematical notation ambiguous, parsing formulae typeset as mathematicians like to write down on paper is a challenging task; a challenge neglected by several theorem provers which usually prefer to fix an unambiguous input syntax. Exploiting features of the underlying calculus, Matita offers an efficient disambiguation engine which permit to type formulae in the familiar mathematical notation. Step-by-step tacticals. Tacticals are higher-order constructs used in proof scripts to combine tactics together. With tacticals scripts can be made shorter, readable, and more resilient to changes. Unfortunately they are de facto incompatible with state-of-the-art user interfaces based on script management. Such interfaces indeed do not permit to position the execution point inside complex tacticals, thus introducing a trade-off between the usefulness of structuring scripts and a tedious big step execution behavior during script replaying. In Matita we break this trade-off with tinycals: an alternative to a subset of LCF tacticals which can be evaluated in a more fine-grained manner. Extensible yet meaningful notation. Proof assistant users often face the need of creating new mathematical notation in order to ease the use of new concepts. The framework used in Matita for dealing with extensible notation both accounts for high quality bidimensional rendering of formulae (with the expressivity of MathMLPresentation) and provides meaningful notation, where presentational fragments are kept synchronized with semantic representation of terms. Using our approach interoperability with other systems can be achieved at the content level, and direct manipulation of formulae acting on their rendered forms is possible too. Publish/subscribe hints. Automation plays an important role in interactive proving as users like to delegate tedious proving sub-tasks to decision procedures or external reasoners. Exploiting the Web-friendliness of Matita we experimented with a broker and a network of web services (called tutors) which can try independently to complete open sub-goals of a proof, currently being authored in Matita. The user receives hints from the tutors on how to complete sub-goals and can interactively or automatically apply them to the current proof. Another innovative aspect of Matita, only marginally touched by this thesis, is the embedded content-based search engine Whelp which is exploited to various ends, from automatic theorem proving to avoiding duplicate work for the user. We also discuss the (potential) reusability in other systems of the widgets presented in this thesis and how we envisage the evolution of user interfaces for interactive theorem provers in the Web 2.0 era.

Studio di ausili tecnologici compensativi di supporto all'iter di apprendimento matematico secondario e universitario degli studenti con dislessia

Data coming out from various researches carried out over the last years in Italy on the problem of school dispersion in secondary school show that difficulty in studying mathematics is one of the most frequent reasons of discomfort reported by students. Nevertheless, it is definitely unrealistic to think we can do without such knowledge in today society: mathematics is largely taught in secondary school and it is not confined within technical-scientific courses only. It is reasonable to say that, although students may choose academic courses that are, apparently, far away from mathematics, all students will have to come to terms, sooner or later in their life, with this subject. Among the reasons of discomfort given by the study of mathematics, some mention the very nature of this subject and in particular the complex symbolic language through which it is expressed. In fact, mathematics is a multimodal system composed by oral and written verbal texts, symbol expressions, such as formulae and equations, figures and graphs. For this, the study of mathematics represents a real challenge to those who suffer from dyslexia: this is a constitutional condition limiting people performances in relation to the activities of reading and writing and, in particular, to the study of mathematical contents. Here the difficulties in working with verbal and symbolic codes entail, in turn, difficulties in the comprehension of texts from which to deduce operations that, once combined together, would lead to the problem final solution. Information technologies may support this learning disorder effectively. However, these tools have some implementation limits, restricting their use in the study of scientific subjects. Vocal synthesis word processors are currently used to compensate difficulties in reading within the area of classical studies, but they are not used within the area of mathematics. This is because the vocal synthesis (or we should say the screen reader supporting it) is not able to interpret all that is not textual, such as symbols, images and graphs. The DISMATH software, which is the subject of this project, would allow dyslexic users to read technical-scientific documents with the help of a vocal synthesis, to understand the spatial structure of formulae and matrixes, to write documents with a technical-scientific content in a format that is compatible with main scientific editors. The system uses LaTex, a text mathematic language, as mediation system. It is set up as LaTex editor, whose graphic interface, in line with main commercial products, offers some additional specific functions with the capability to support the needs of users who are not able to manage verbal and symbolic codes on their own. LaTex is translated in real time into a standard symbolic language and it is read by vocal synthesis in natural language, in order to increase, through the bimodal representation, the ability to process information. The understanding of the mathematic formula through its reading is made possible by the deconstruction of the formula itself and its “tree” representation, so allowing to identify the logical elements composing it. Users, even without knowing LaTex language, are able to write whatever scientific document they need: in fact the symbolic elements are recalled by proper menus and automatically translated by the software managing the correct syntax. The final aim of the project, therefore, is to implement an editor enabling dyslexic people (but not only them) to manage mathematic formulae effectively, through the integration of different software tools, so allowing a better teacher/learner interaction too.

Measurement of top quark pairs production cross-section in the semi-leptonic channel with the ATLAS experiment

This thesis is about three major aspects of the identification of top quarks. First comes the understanding of their production mechanism, their decay channels and how to translate theoretical formulae into programs that can simulate such physical processes using Monte Carlo techniques. In particular, the author has been involved in the introduction of the POWHEG generator in the framework of the ATLAS experiment. POWHEG is now fully used as the benchmark program for the simulation of ttbar pairs production and decay, along with MC@NLO and AcerMC: this will be shown in chapter one. The second chapter illustrates the ATLAS detectors and its sub-units, such as calorimeters and muon chambers. It is very important to evaluate their efficiency in order to fully understand what happens during the passage of radiation through the detector and to use this knowledge in the calculation of final quantities such as the ttbar production cross section. The last part of this thesis concerns the evaluation of this quantity deploying the so-called "golden channel" of ttbar decays, yielding one energetic charged lepton, four particle jets and a relevant quantity of missing transverse energy due to the neutrino. The most important systematic errors arising from the various part of the calculation are studied in detail. Jet energy scale, trigger efficiency, Monte Carlo models, reconstruction algorithms and luminosity measurement are examples of what can contribute to the uncertainty about the cross-section.

A moment symbolic representation of Lévy processes with applications

By using a symbolic method, known in the literature as the classical umbral calculus, a symbolic representation of Lévy processes is given and a new family of time-space harmonic polynomials with respect to such processes, which includes and generalizes the exponential complete Bell polynomials, is introduced. The usefulness of time-space harmonic polynomials with respect to Lévy processes is that it is a martingale the stochastic process obtained by replacing the indeterminate x of the polynomials with a Lévy process, whereas the Lévy process does not necessarily have this property. Therefore to find such polynomials could be particularly meaningful for applications. This new family includes Hermite polynomials, time-space harmonic with respect to Brownian motion, Poisson-Charlier polynomials with respect to Poisson processes, Laguerre and actuarial polynomials with respect to Gamma processes , Meixner polynomials of the first kind with respect to Pascal processes, Euler, Bernoulli, Krawtchuk, and pseudo-Narumi polynomials with respect to suitable random walks. The role played by cumulants is stressed and brought to the light, either in the symbolic representation of Lévy processes and their infinite divisibility property, either in the generalization, via umbral Kailath-Segall formula, of the well-known formulae giving elementary symmetric polynomials in terms of power sum symmetric polynomials. The expression of the family of time-space harmonic polynomials here introduced has some connections with the so-called moment representation of various families of multivariate polynomials. Such moment representation has been studied here for the first time in connection with the time-space harmonic property with respect to suitable symbolic multivariate Lévy processes. In particular, multivariate Hermite polynomials and their properties have been studied in connection with a symbolic version of the multivariate Brownian motion, while multivariate Bernoulli and Euler polynomials are represented as powers of multivariate polynomials which are time-space harmonic with respect to suitable multivariate Lévy processes.

Studies on the dual in Mycenaean, in the Homeric poetry and in the Attic Theatre of the 5th century — morphological, dialectal and stylistical variations

The present dissertation focuses on the dual number in Ancient Greek in a diachronical lapse stretching from the Mycenaean age to the Attic Drama and Comedy of the 5th century BC. In the first chapter morphological issues are addressed, chiefly in a comparative perspective. The Indo European evidence on the dual is hence gathered in order to sketch patterns of grammaticalisation and paradigmatisation of specific grams, growing increasingly functional within the Greek domain. In the second chapter syntactical problems are tackled. After a survey of scholarly literature on the Greek dual, we engage in a functional and typological approach, in order to disentangle some biased assessments on the dual, namely its alleged lack of regularity and intermittent agreement. Some recent frameworks in General Linguistics provide useful grounds for casting new light on the subject. Internal Reconstruction, for instance, supports the facultativity of the dual in each and every stage of its development; Typology and the Animacy Hierarcy add precious cross linguistical insight on the behaviour of the dual toward agreement. Glaring differences also arise as to the adoption — or avoidance — of the dual by different authors. Idiolectal varieties prove in fact conditioned by stylistical and register necessity. By means of a comparison among Epics, Tragedy and Comedy it is possible to enhance differences in the evaluation of the dual, which led sometimes to forms of ‘censure’ — thus triggering the onset of competing strategies to express duality. The last two chapters delve into the tantalising variety of the Homeric evidence, first of all in an account of the notorious issue of the Embassy of Iliad IX, and last in a commentary of all significant Homeric duals — mostly represented by archaisms, formulae, and ad hoc coinages.

Fracture Mechanics Investigation of Structures with Defects

Fracture mechanics plays an important role in the material science, structure design and industrial production due to the failure of materials and structures are paid high attention in human activities. This dissertation, concentrates on some of the fractural aspects of shaft and composite which have being increasingly used in modern structures, consists four chapters within two parts. Chapters 1 to 4 are included in part 1. In the first chapter, the basic knowledge about the stress and displacement fields in the vicinity of a crack tip is introduced. A review involves the general methods of calculating stress intensity factors are presented. In Chapter 2, two simple engineering methods for a fast and close approximation of stress intensity factors of cracked or notched beams under tension, bending moment, shear force, as well as torque are presented. New formulae for calculating the stress intensity factors are proposed. One of the methods named Section Method is improved and applied to the three dimensional analysis of cracked circular section for calculating stress intensity factors. The comparisons between the present results and the solutions calculated by ABAQUS for single mode and mixed mode are studied. In chapter 3, fracture criteria for a crack subjected to mixed mode loading of two-dimension and three-dimension are reviewed. The crack extension angle for single mode and mixed mode, and the critical loading domain obtained by SEDF and MTS are compared. The effects of the crack depth and the applied force ratio on the crack propagation angle and the critical loading are investigated. Three different methods calculating the crack initiation angle for three-dimension analysis of various crack depth and crack position are compared. It should be noted that the stress intensity factors used in the criteria are calculated in section 2.1.

Milk and dairy products: evaluation of bioactive components by analytical techniques

Milk and dairy products are important source of bioactive compounds useful to satisfy the nutritional and physiological needs of any newborns of mammalian species and useful to guarantee adequate growth and development of infants as well as provide a complete nourishment of adults. Physico-chemical, nutritional and organoleptic properties of the main constituents and the “minor” components have a crucial role in the quality of milk and milk products. Although in the past decades dietary milk fat was often regarded as harmful for the human health, recent researches suggest that milk contains specific fatty acids with nutritional and physiological health benefits. For these reasons, a major attention is given to the quantity and quality of total fat intake. In the recent years, as a result of the new concept of multifunctional agriculture and the changing behaviours about diet, consumer demands in favor of high-quality, security and safety dairy products are increased. Moreover, milk proteins and milk-derived bioactive peptides are recognized to have a high nutritive value, several health-promoting functional activities and excellent technological properties. Accordingly, growing interest in the development of functional dairy products and preparation of infant formulae for babies who cannot be breast-fed, has been give in order to meet the specific consumer’s requests. This manuscript presents the main results obtained during my PhD research aimed to evaluate the main bioactive lipids and proteins in milk and dairy products using innovative analytical techniques. The experimental section of this manuscript is divided in two sections where are reported the main results obtained during my research activities on dairy products and human milks in order to characterize their bioactive compounds for functional food applications.

Neural network modelling of the wave-structure interaction processes

This thesis presents a new Artificial Neural Network (ANN) able to predict at once the main parameters representative of the wave-structure interaction processes, i.e. the wave overtopping discharge, the wave transmission coefficient and the wave reflection coefficient. The new ANN has been specifically developed in order to provide managers and scientists with a tool that can be efficiently used for design purposes. The development of this ANN started with the preparation of a new extended and homogeneous database that collects all the available tests reporting at least one of the three parameters, for a total amount of 16’165 data. The variety of structure types and wave attack conditions in the database includes smooth, rock and armour unit slopes, berm breakwaters, vertical walls, low crested structures, oblique wave attacks. Some of the existing ANNs were compared and improved, leading to the selection of a final ANN, whose architecture was optimized through an in-depth sensitivity analysis to the training parameters of the ANN. Each of the selected 15 input parameters represents a physical aspect of the wave-structure interaction process, describing the wave attack (wave steepness and obliquity, breaking and shoaling factors), the structure geometry (submergence, straight or non-straight slope, with or without berm or toe, presence or not of a crown wall), or the structure type (smooth or covered by an armour layer, with permeable or impermeable core). The advanced ANN here proposed provides accurate predictions for all the three parameters, and demonstrates to overcome the limits imposed by the traditional formulae and approach adopted so far by some of the existing ANNs. The possibility to adopt just one model to obtain a handy and accurate evaluation of the overall performance of a coastal or harbor structure represents the most important and exportable result of the work.