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.

Diagnostic techniques for EHD and MHD interaction

The impact of plasma technologies is growing both in the academic and in the industrial fields. Nowadays, a great interest is focused in plasma applications in aeronautics and astronautics domains. Plasma actuators based on the Magneto-Hydro-Dynamic (MHD) and Electro- Hydro-Dynamic (EHD) interactions are potentially able to suitably modify the fluid-dynamics characteristics around a flying body without utilizing moving parts. This could lead to the control of an aircraft with negligible response time, more reliability and improvements of the performance. In order to study the aforementioned interactions, a series of experiments and a wide number of diagnostic techniques have been utilized. The EHD interaction, realized by means of a Dielectric Barrier Discharge (DBD) actuator, and its impact on the boundary layer have been evaluated by means of two different experiments. In the first one a three phase multi-electrode flat panel actuator is used. Different external flow velocities (from 1 to 20m/s) and different values of the supplied voltage and frequency have been considered. Moreover a change of the phase sequence has been done to verify the influence of the electric field existing between successive phases. Measurements of the induced speed had shown the effect of the supply voltage and the frequency, and the phase order in the momentum transfer phenomenon. Gains in velocity, inside the boundary layer, of about 5m/s have been obtained. Spectroscopic measurements allowed to determine the rotational and the vibrational temperature of the plasma which lie in the range of 320 ÷ 440°K and of 3000 ÷ 3900°K respectively. A deviation from thermodynamic equilibrium had been found. The second EHD experiment is realized on a single electrode pair DBD actuator driven by nano-pulses superimposed to a DC or an AC bias. This new supply system separates the plasma formation mechanism from the acceleration action on the fluid, leading to an higher degree of the control of the process. Both the voltage and the frequency of the nano-pulses and the amplitude and the waveform of the bias have been varied during the experiment. Plasma jets and vortex behavior had been observed by means of fast Schlieren imaging. This allowed a deeper understanding of the EHD interaction process. A velocity increase in the boundary layer of about 2m/s had been measured. Thrust measurements have been performed by means of a scales and compared with experimental data reported in the literature. For similar voltage amplitudes thrust larger than those of the literature, had been observed. Surface charge measurements led to realize a modified DBD actuator able to obtain similar performances when compared with that of other experiments. However in this case a DC bias replacing the AC bias had been used. MHD interaction experiments had been carried out in a hypersonic wind tunnel in argon with a flow of Mach 6. Before the MHD experiments a thermal, fluid-dynamic and plasma characterization of the hypersonic argon plasma flow have been done. The electron temperature and the electron number density had been determined by means of emission spectroscopy and microwave absorption measurements. A deviation from thermodynamic equilibrium had been observed. The electron number density showed to be frozen at the stagnation region condition in the expansion through the nozzle. MHD experiments have been performed using two axial symmetric test bodies. Similar magnetic configurations were used. Permanent magnets inserted into the test body allowed to generate inside the plasma azimuthal currents around the conical shape of the body. These Faraday currents are responsible of the MHD body force which acts against the flow. The MHD interaction process has been observed by means of fast imaging, pressure and electrical measurements. Images showed bright rings due to the Faraday currents heating and exciting the plasma particles. Pressure measurements showed increases of the pressure in the regions where the MHD interaction is large. The pressure is 10 to 15% larger than when the MHD interaction process is silent. Finally by means of electrostatic probes mounted flush on the test body lateral surface Hall fields of about 500V/m had been measured. These results have been used for the validation of a numerical MHD code.

Specification and Verification of Declarative Open Interaction Models - A Logic-based framework

The advent of distributed and heterogeneous systems has laid the foundation for the birth of new architectural paradigms, in which many separated and autonomous entities collaborate and interact to the aim of achieving complex strategic goals, impossible to be accomplished on their own. A non exhaustive list of systems targeted by such paradigms includes Business Process Management, Clinical Guidelines and Careflow Protocols, Service-Oriented and Multi-Agent Systems. It is largely recognized that engineering these systems requires novel modeling techniques. In particular, many authors are claiming that an open, declarative perspective is needed to complement the closed, procedural nature of the state of the art specification languages. For example, the ConDec language has been recently proposed to target the declarative and open specification of Business Processes, overcoming the over-specification and over-constraining issues of classical procedural approaches. On the one hand, the success of such novel modeling languages strongly depends on their usability by non-IT savvy: they must provide an appealing, intuitive graphical front-end. On the other hand, they must be prone to verification, in order to guarantee the trustworthiness and reliability of the developed model, as well as to ensure that the actual executions of the system effectively comply with it. In this dissertation, we claim that Computational Logic is a suitable framework for dealing with the specification, verification, execution, monitoring and analysis of these systems. We propose to adopt an extended version of the ConDec language for specifying interaction models with a declarative, open flavor. We show how all the (extended) ConDec constructs can be automatically translated to the CLIMB Computational Logic-based language, and illustrate how its corresponding reasoning techniques can be successfully exploited to provide support and verification capabilities along the whole life cycle of the targeted systems.

Interaction between APOE4 genotype and environmental risk factors in Alzheimer's disease

Alzheimer's disease (AD) is probably caused by both genetic and environmental risk factors. The major genetic risk factor is the E4 variant of apolipoprotein E gene called apoE4. Several risk factors for developing AD have been identified including lifestyle, such as dietary habits. The mechanisms behind the AD pathogenesis and the onset of cognitive decline in the AD brain are presently unknown. In this study we wanted to characterize the effects of the interaction between environmental risk factors and apoE genotype on neurodegeneration processes, with particular focus on behavioural studies and neurodegenerative processes at molecular level. Towards this aim, we used 6 months-old apoE4 and apoE3 Target Replacement (TR) mice fed on different diets (high intake of cholesterol and high intake of carbohydrates). These mice were evaluated for learning and memory deficits in spatial reference (Morris Water Maze (MWM)) and contextual learning (Passive Avoidance) tasks, which involve the hippocampus and the amygdala, respectively. From these behavioural studies we found that the initial cognitive impairments manifested as a retention deficit in apoE4 mice fed on high carbohydrate diet. Thus, the genetic risk factor apoE4 genotype associated with a high carbohydrate diet seems to affect cognitive functions in young mice, corroborating the theory that the combination of genetic and environmental risk factors greatly increases the risk of developing AD and leads to an earlier onset of cognitive deficits. The cellular and molecular bases of the cognitive decline in AD are largely unknown. In order to determine the molecular changes for the onset of the early cognitive impairment observed in the behavioural studies, we performed molecular studies, with particular focus on synaptic integrity and Tau phosphorylation. The most relevant finding of our molecular studies showed a significant decrease of Brain-derived Neurotrophic Factor (BDNF) in apoE4 mice fed on high carbohydrate diet. Our results may suggest that BDNF decrease found in apoE4 HS mice could be involved in the earliest impairment in long-term reference memory observed in behavioural studies. The second aim of this thesis was to study possible involvement of leptin in AD. There is growing evidence that leptin has neuroprotective properties in the Central Nervous System (CNS). Recent evidence has shown that leptin and its receptors are widespread in the CNS and may provide neuronal survival signals. However, there are still numerous questions, regarding the molecular mechanism by which leptin acts, that remain unanswered. Thus, given to the importance of the involvement of leptin in AD, we wanted to clarify the function of leptin in the pathogenesis of AD and to investigate if apoE genotype affect leptin levels through studies in vitro, in mice and in human. Our findings suggest that apoE4 TR mice showed an increase of leptin in the brain. Leptin levels are also increased in the cerebral spinal fluid of AD patients and apoE4 carriers with AD have higher levels of leptin than apoE3 carriers. Moreover, leptin seems to be expressed by reactive glial cells in AD brains. In vitro, ApoE4 together with Amyloid beta increases leptin production by microglia and astrocytes. Taken together, all these findings suggest that leptin replacement might not be a good strategy for AD therapy. Our results show that high leptin levels were found in AD brains. These findings suggest that, as high leptin levels do not promote satiety in obese individuals, it might be possible that they do not promote neuroprotection in AD patients. Therefore, we hypothesized that AD brain could suffer from leptin resistance. Further studies will be critical to determine whether or not the central leptin resistance in SNC could affect its potential neuroprotective effects.

Fiber beam-columns models with flexure-shear interaction for nonlinear analysis of reinforced concrete structures

The aim of this study was to develop a model capable to capture the different contributions which characterize the nonlinear behaviour of reinforced concrete structures. In particular, especially for non slender structures, the contribution to the nonlinear deformation due to bending may be not sufficient to determine the structural response. Two different models characterized by a fibre beam-column element are here proposed. These models can reproduce the flexure-shear interaction in the nonlinear range, with the purpose to improve the analysis in shear-critical structures. The first element discussed is based on flexibility formulation which is associated with the Modified Compression Field Theory as material constitutive law. The other model described in this thesis is based on a three-field variational formulation which is associated with a 3D generalized plastic-damage model as constitutive relationship. The first model proposed in this thesis was developed trying to combine a fibre beamcolumn element based on the flexibility formulation with the MCFT theory as constitutive relationship. The flexibility formulation, in fact, seems to be particularly effective for analysis in the nonlinear field. Just the coupling between the fibre element to model the structure and the shear panel to model the individual fibres allows to describe the nonlinear response associated to flexure and shear, and especially their interaction in the nonlinear field. The model was implemented in an original matlab® computer code, for describing the response of generic structures. The simulations carried out allowed to verify the field of working of the model. Comparisons with available experimental results related to reinforced concrete shears wall were performed in order to validate the model. These results are characterized by the peculiarity of distinguishing the different contributions due to flexure and shear separately. The presented simulations were carried out, in particular, for monotonic loading. The model was tested also through numerical comparisons with other computer programs. Finally it was applied for performing a numerical study on the influence of the nonlinear shear response for non slender reinforced concrete (RC) members. Another approach to the problem has been studied during a period of research at the University of California Berkeley. The beam formulation follows the assumptions of the Timoshenko shear beam theory for the displacement field, and uses a three-field variational formulation in the derivation of the element response. A generalized plasticity model is implemented for structural steel and a 3D plastic-damage model is used for the simulation of concrete. The transverse normal stress is used to satisfy the transverse equilibrium equations of at each control section, this criterion is also used for the condensation of degrees of freedom from the 3D constitutive material to a beam element. In this thesis is presented the beam formulation and the constitutive relationships, different analysis and comparisons are still carrying out between the two model presented.

Fluid-structure interaction by a coupled lattice Boltzmann-finite element approach

In this thesis, a strategy to model the behavior of fluids and their interaction with deformable bodies is proposed. The fluid domain is modeled by using the lattice Boltzmann method, thus analyzing the fluid dynamics by a mesoscopic point of view. It has been proved that the solution provided by this method is equivalent to solve the Navier-Stokes equations for an incompressible flow with a second-order accuracy. Slender elastic structures idealized through beam finite elements are used. Large displacements are accounted for by using the corotational formulation. Structural dynamics is computed by using the Time Discontinuous Galerkin method. Therefore, two different solution procedures are used, one for the fluid domain and the other for the structural part, respectively. These two solvers need to communicate and to transfer each other several information, i.e. stresses, velocities, displacements. In order to guarantee a continuous, effective, and mutual exchange of information, a coupling strategy, consisting of three different algorithms, has been developed and numerically tested. In particular, the effectiveness of the three algorithms is shown in terms of interface energy artificially produced by the approximate fulfilling of compatibility and equilibrium conditions at the fluid-structure interface. The proposed coupled approach is used in order to solve different fluid-structure interaction problems, i.e. cantilever beams immersed in a viscous fluid, the impact of the hull of the ship on the marine free-surface, blood flow in a deformable vessels, and even flapping wings simulating the take-off of a butterfly. The good results achieved in each application highlight the effectiveness of the proposed methodology and of the C++ developed software to successfully approach several two-dimensional fluid-structure interaction problems.

Targeting the p53–MDM2 interaction by the small-molecule MDM2 antagonist Nutlin-3a: a new challenged target therapy in adult Philadelphia positive acute lymphoblastic leukemia patients

The human p53 tumor suppressor, known as the “guardian of the genome”, is one of the most important molecules in human cancers. One mechanism for suppressing p53 uses its negative regulator, MDM2, which modulates p53 by binding directly to and decreasing p53 stability. In testing novel therapeutic approaches activating p53, we investigated the preclinical activity of the MDM2 antagonist, Nutlin-3a, in Philadelphia positive (Ph+) and negative (Ph-) leukemic cell line models, and primary B-Acute lymphoblastic leukemia (ALL) patient samples. In this study we demonstrated that treatment with Nutlin-3a induced grow arrest and apoptosis mediated by p53 pathway in ALL cells with wild-type p53, in time and dose-dependent manner. Consequently, MDM2 inhibitor caused an increase of pro-apoptotic proteins and key regulators of cell cycle arrest. The dose-dependent reduction in cell viability was confirmed in primary blast cells from Ph+ ALL patients with the T315I Bcr-Abl kinase domain mutation. In order to better elucidate the implications of p53 activation and to identify biomarkers of clinical activity, gene expression profiling analysis in sensitive cell lines was performed. A total of 621 genes were differentially expressed (p < 0.05). We found a strong down-regulation of GAS41 (growth-arrest specific 1 gene) and BMI1 (a polycomb ring-finger oncogene) (fold-change -1.35 and -1.11, respectively; p-value 0.02 and 0.03, respectively) after in vitro treatment as compared to control cells. Both genes are repressors of INK4/ARF and p21. Given the importance of BMI in the control of apoptosis, we investigated its pattern in treated and untreated cells, confirming a marked decrease after exposure to MDM2 inhibitor in ALL cells. Noteworthy, the BMI-1 levels remained constant in resistant cells. Therefore, BMI-1 may be used as a biomarker of response. Our findings provide a strong rational for further clinical investigation of Nutlin-3a in Ph+ and Ph-ALL.

Analysis and mathematical modeling of wave-structure interaction

The aim of this thesis, included within the THESEUS project, is the development of a mathematical model 2DV two-phase, based on the existing code IH-2VOF developed by the University of Cantabria, able to represent together the overtopping phenomenon and the sediment transport. Several numerical simulations were carried out in order to analyze the flow characteristics on a dike crest. The results show that the seaward/landward slope does not affect the evolution of the flow depth and velocity over the dike crest whereas the most important parameter is the relative submergence. Wave heights decrease and flow velocities increase while waves travel over the crest. In particular, by increasing the submergence, the wave height decay and the increase of the velocity are less marked. Besides, an appropriate curve able to fit the variation of the wave height/velocity over the dike crest were found. Both for the wave height and for the wave velocity different fitting coefficients were determined on the basis of the submergence and of the significant wave height. An equation describing the trend of the dimensionless coefficient c_h for the wave height was derived. These conclusions could be taken into consideration for the design criteria and the upgrade of the structures. In the second part of the thesis, new equations for the representation of the sediment transport in the IH-2VOF model were introduced in order to represent beach erosion while waves run-up and overtop the sea banks during storms. The new model allows to calculate sediment fluxes in the water column together with the sediment concentration. Moreover it is possible to model the bed profile evolution. Different tests were performed under low-intensity regular waves with an homogeneous layer of sand on the bottom of a channel in order to analyze the erosion-deposition patterns and verify the model results.

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.

Apple latent infection caused by Neofabraea alba: host-pathogen interaction and disease management

Apple latent infection caused by Neofabraea alba: host-pathogen interaction and disease management Bull’s eye rot (BER) caused by Neofabraea alba is one of the most frequent and damaging latent infection occurring in stored pome fruits worldwide. Fruit infection occurs in the orchard, but disease symptoms appear only 3 months after harvest, during refrigerated storage. In Italy BER is particularly serious for late harvest apple cultivar as ‘Pink Lady™’. The purposes of this thesis were: i) Evaluate the influence of ‘Pink Lady™’ apple primary metabolites in N. alba quiescence ii) Evaluate the influence of pH in five different apple cultivars on BER susceptibility iii) To find out not chemical method to control N. alba infection iv) Identify some fungal volatile compounds in order to use them as N. alba infections markers. Results regarding the role of primary metabolites showed that chlorogenic, quinic and malic acid inhibit N. alba development. The study based on the evaluation of cultivar susceptibility, showed that Granny Smith was the most resistant apple cultivar among the varieties analyzed. Moreover, Granny Smith showed the lowest pH value from harvest until the end of storage, supporting the thesis that ambient pH could be involved in the interaction between N. alba and apple. In order to find out new technologies able to improve lenticel rot management, the application of a non-destructive device for the determination of chlorophyll content was applied. Results showed that fruit with higher chlorophyll content are less susceptible to BER, and molecular analyses comforted this result. Fruits with higher chlorophyll content showed up-regulation of PGIP and HCT, genes involved in plant defence. Through the application of PTR-MS and SPME GC-MS, 25 volatile organic compounds emitted by N. alba were identified. Among them, 16 molecules were identified as potential biomarkers.

Study of Rapid Alkalinization Factor (RALF)genes as plant susceptibility agents during plant-pathogen interaction in strawberry

Rapid Alkalinization Factor (RALF) are cysteins-rich peptides ubiquitous in plant kingdom. They play multiple roles as hormone signals and recently their involvement in host-pathogen crosstalk as negative regulator of immunity in Arabidopsis has also been recognized. In addition, RALF homologue peptides are secreted by different fungal pathogens as effectors during early stages of infections. The aim of this work was to characterize RALF genes as susceptibility factors during plant pathogen interaction in strawberry. For this, the genomic organization of the RALF gene families in the octoploid strawberry (Fragaria × ananassa) and the re-annotated genome of Fragaria vesca were described , identifying 13 member in F. vesca (FvRALF) and 50 members in F. x ananassa (FaRALF). The changes in expression of fruit FaRALF genes was investigated upon infection with C.acutatum and B. cinerea showing that, among RALF genes expressed in fruit, FaRALF3 was the only one upregulated by fungal infection in the ripe stage. A role of FaRALF3 as susceptibility gene was then assessed trough Agrobacterium-mediated transient FaRALF3 overexpression and silencing in fruits, revealing that FaRALF3 expression promotes fungal growth and hyphae penetration in host tissues. In silico analysis was used to identify distinct pathogen inducible elements upstream of the FaRALF3 gene. Agroinfiltration of strawberry fruit with deletion constructs of the FaRALF3 promoter identified a 5’ region required for FaRALF3 expression in fruit, but failed to identify a region responsible for fungal induced expression. Furthermore, FaRALF3 and strawberry receptor FERONIA (FaMRLK47) were heterologously expressed in E. coli in order to purify active proteins forms and study RALF-FERONIA interaction in strawberry. However, it was not possible to obtain pure and active proteins. Finally RNAi transgenic plants silenced for the FvRALF13 gene were genotypically and phenotypically characterized suggesting a role of FvRALF13 in flowering time regulation and reproductive organs development.