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.

Trasmissione post-natale del citomegalovirus attraverso il latte materno al neonato VLBW

Introduction Postnatal human cytomegalovirus (CMV) infection is usually asymptomatic in term babies, while preterm infants are more susceptible to symptomatic CMV infection. Breastfeeding plays a dominant role in the epidemiology of transmission of postnatal CMV infection, but the risk factors of symptomatic CMV infection in preterm infants are unknown. Patients and Methods Between December 2003 and August 2006, eighty Very Low Birth Weight (VLBW) preterm infants (gestational age ≤ 32 weeks and birth weight < 1500 g), admitted to the Neonatal Intensive Care Unit of St Orsola-Malpighi General Hospital, Bologna were recruited. All of them were breastfed for at least one month. During the first week of life, serological test for CMV was performed on maternal blood. Furthermore, urinary CMV culture was performed in all the infants in order to exclude a congenital CMV infection. Urine samples from each infant were collected and processed for CMV culture once a week. Once every 15 days a blood sample was taken from each infant to evaluate the complete blood count, the hepatic function and the C reactive protein. In addition, samples of fresh breast milk were processed weekly for CMV culture. A genetic analysis of virus variant was performed in the urine of the infected infants and in their mother’s milk to confirm the origin of infection. Results We evaluated 80 VLBW infants and their 68 mothers. Fifty-three mothers (78%) were positive for CMV IgG antibodies, and 15 (22%) were seronegative. In the seronegative group, CMV was never isolated in breast milk, and none of the 18 infants developed viruria; in the seropositive group, CMV was isolated in 21 out of 53 (40%) mother’s milk. CMV was detected in the urine samples of 9 out of 26 (35%) preterm infants, who were born from 21 virolactia positive mothers. Six of these infants had clinically asymptomatic CMV infection, while 3 showed a sepsis-like illness with bradycardia, tachypnea and repeated desaturations. Eight out of nine infants showed abnormal hematologic values. The detection of neutropenia was strictly related to CMV infection (8/9 infected infants vs 17/53 non infected infants, P<.005), such as the detection of an increase in conjugated bilirubin (3/9 infected infants vs 2/53 non infected infants, P<.05). The degree of neutropenia was not different between the two groups (infected/non infected). The use of hemoderivatives (plasma and/or IgM–enriched immunoglobulin) in order to treat a suspected/certain infection in newborn with GE< 28 ws was seen as protective against CMV infection (1/4 infected infants vs 18/20 non infected infants [GE<28 ws]; P<.05). Furthermore, bronchopulmonary dysplasia (defined both as oxygen-dependency at 30 days of life and 36 ws of postmenstrual age) correlated with symptomatic infection (3/3 symptomatic vs 0/6 asymptomatic: P<.05). Conclusion Our data suggest that CMV infection transmitted to preterm newborn through human milk is always asymptomatic when newborns are clinically stable. Otherwise, the infection can worsen a preexisting disease such as bronchopulmonary dysplasia. Human milk offers many nutritional and psychological advantages to preterm newborns: according to our data, there’s no reason to contraindicate it neither to pasteurize the milk of all the mothers of preterm infants who are CMV seropositive.

Seizure prediction and control in epilepsy

The first part of my thesis presents an overview of the different approaches used in the past two decades in the attempt to forecast epileptic seizure on the basis of intracranial and scalp EEG. Past research could reveal some value of linear and nonlinear algorithms to detect EEG features changing over different phases of the epileptic cycle. However, their exact value for seizure prediction, in terms of sensitivity and specificity, is still discussed and has to be evaluated. In particular, the monitored EEG features may fluctuate with the vigilance state and lead to false alarms. Recently, such a dependency on vigilance states has been reported for some seizure prediction methods, suggesting a reduced reliability. An additional factor limiting application and validation of most seizure-prediction techniques is their computational load. For the first time, the reliability of permutation entropy [PE] was verified in seizure prediction on scalp EEG data, contemporarily controlling for its dependency on different vigilance states. PE was recently introduced as an extremely fast and robust complexity measure for chaotic time series and thus suitable for online application even in portable systems. The capability of PE to distinguish between preictal and interictal state has been demonstrated using Receiver Operating Characteristics (ROC) analysis. Correlation analysis was used to assess dependency of PE on vigilance states. Scalp EEG-Data from two right temporal epileptic lobe (RTLE) patients and from one patient with right frontal lobe epilepsy were analysed. The last patient was included only in the correlation analysis, since no datasets including seizures have been available for him. The ROC analysis showed a good separability of interictal and preictal phases for both RTLE patients, suggesting that PE could be sensitive to EEG modifications, not visible on visual inspection, that might occur well in advance respect to the EEG and clinical onset of seizures. However, the simultaneous assessment of the changes in vigilance showed that: a) all seizures occurred in association with the transition of vigilance states; b) PE was sensitive in detecting different vigilance states, independently of seizure occurrences. Due to the limitations of the datasets, these results cannot rule out the capability of PE to detect preictal states. However, the good separability between pre- and interictal phases might depend exclusively on the coincidence of epileptic seizure onset with a transition from a state of low vigilance to a state of increased vigilance. The finding of a dependency of PE on vigilance state is an original finding, not reported in literature, and suggesting the possibility to classify vigilance states by means of PE in an authomatic and objectic way. The second part of my thesis provides the description of a novel behavioral task based on motor imagery skills, firstly introduced (Bruzzo et al. 2007), in order to study mental simulation of biological and non-biological movement in paranoid schizophrenics (PS). Immediately after the presentation of a real movement, participants had to imagine or re-enact the very same movement. By key release and key press respectively, participants had to indicate when they started and ended the mental simulation or the re-enactment, making it feasible to measure the duration of the simulated or re-enacted movements. The proportional error between duration of the re-enacted/simulated movement and the template movement were compared between different conditions, as well as between PS and healthy subjects. Results revealed a double dissociation between the mechanisms of mental simulation involved in biological and non-biologial movement simulation. While for PS were found large errors for simulation of biological movements, while being more acurate than healthy subjects during simulation of non-biological movements. Healthy subjects showed the opposite relationship, making errors during simulation of non-biological movements, but being most accurate during simulation of non-biological movements. However, the good timing precision during re-enactment of the movements in all conditions and in both groups of participants suggests that perception, memory and attention, as well as motor control processes were not affected. Based upon a long history of literature reporting the existence of psychotic episodes in epileptic patients, a longitudinal study, using a slightly modified behavioral paradigm, was carried out with two RTLE patients, one patient with idiopathic generalized epilepsy and one patient with extratemporal lobe epilepsy. Results provide strong evidence for a possibility to predict upcoming seizures in RTLE patients behaviorally. In the last part of the thesis it has been validated a behavioural strategy based on neurobiofeedback training, to voluntarily control seizures and to reduce there frequency. Three epileptic patients were included in this study. The biofeedback was based on monitoring of slow cortical potentials (SCPs) extracted online from scalp EEG. Patients were trained to produce positive shifts of SCPs. After a training phase patients were monitored for 6 months in order to validate the ability of the learned strategy to reduce seizure frequency. Two of the three refractory epileptic patients recruited for this study showed improvements in self-management and reduction of ictal episodes, even six months after the last training session.

Mitochondrial dysfunction in a cell model of thyroid oncocytoma

The role of mitochondrial dysfunction in cancer has long been a subject of great interest. In this study, such dysfunction has been examined with regards to thyroid oncocytoma, a rare form of cancer, accounting for less than 5% of all thyroid cancers. A peculiar characteristic of thyroid oncocytic cells is the presence of an abnormally large number of mitochondria in the cytoplasm. Such mitochondrial hyperplasia has also been observed in cells derived from patients suffering from mitochondrial encephalomyopathies, where mutations in the mitochondrial DNA(mtDNA) encoding the respiratory complexes result in oxidative phosphorylation dysfunction. An increase in the number of mitochondria occurs in the latter in order to compensate for the respiratory deficiency. This fact spurred the investigation into the presence of analogous mutations in thyroid oncocytic cells. In this study, the only available cell model of thyroid oncocytoma was utilised, the XTC-1 cell line, established from an oncocytic thyroid metastasis to the breast. In order to assess the energetic efficiency of these cells, they were incubated in a medium lacking glucose and supplemented instead with galactose. When subjected to such conditions, glycolysis is effectively inhibited and the cells are forced to use the mitochondria for energy production. Cell viability experiments revealed that XTC-1 cells were unable to survive in galactose medium. This was in marked contrast to the TPC-1 control cell line, a thyroid tumour cell line which does not display the oncocytic phenotype. In agreement with these findings, subsequent experiments assessing the levels of cellular ATP over incubation time in galactose medium, showed a drastic and continual decrease in ATP levels only in the XTC-1 cell line. Furthermore, experiments on digitonin-permeabilised cells revealed that the respiratory dysfunction in the latter was due to a defect in complex I of the respiratory chain. Subsequent experiments using cybrids demonstrated that this defect could be attributed to the mitochondrially-encoded subunits of complex I as opposed to the nuclearencoded subunits. Confirmation came with mtDNA sequencing, which detected the presence of a novel mutation in the ND1 subunit of complex I. In addition, a mutation in the cytochrome b subunit of complex III of the respiratory chain was detected. The fact that XTC-1 cells are unable to survive when incubated in galactose medium is consistent with the fact that many cancers are largely dependent on glycolysis for energy production. Indeed, numerous studies have shown that glycolytic inhibitors are able to induce apoptosis in various cancer cell lines. Subsequent experiments were therefore performed in order to identify the mode of XTC-1 cell death when subjected to the metabolic stress imposed by the forced use of the mitochondria for energy production. Cell shrinkage and mitochondrial fragmentation were observed in the dying cells, which would indicate an apoptotic type of cell death. Analysis of additional parameters however revealed a lack of both DNA fragmentation and caspase activation, thus excluding a classical apoptotic type of cell death. Interestingly, cleavage of the actin component of the cytoskeleton was observed, implicating the action of proteases in this mode of cell demise. However, experiments employing protease inhibitors failed to identify the specific protease involved. It has been reported in the literature that overexpression of Bcl-2 is able to rescue cells presenting a respiratory deficiency. As the XTC-1 cell line is not only respiration-deficient but also exhibits a marked decrease in Bcl-2 expression, it is a perfect model with which to study the relationship between Bcl-2 and oxidative phosphorylation in respiratory-deficient cells. Contrary to the reported literature studies on various cell lines harbouring defects in the respiratory chain, Bcl-2 overexpression was not shown to increase cell survival or rescue the energetic dysfunction in XTC-1 cells. Interestingly however, it had a noticeable impact on cell adhesion and morphology. Whereas XTC-1 cells shrank and detached from the growth surface under conditions of metabolic stress, Bcl-2-overexpressing XTC-1 cells appeared much healthier and were up to 45% more adherent. The target of Bcl-2 in this setting appeared to be the actin cytoskeleton, as the cleavage observed in XTC-1 cells expressing only endogenous levels of Bcl-2, was inhibited in Bcl-2-overexpressing cells. Thus, although unable to rescue XTC-1 cells in terms of cell viability, Bcl-2 is somehow able to stabilise the cytoskeleton, resulting in modifications in cell morphology and adhesion. The mitochondrial respiratory deficiency observed in cancer cells is thought not only to cause an increased dependency on glycolysis but it is also thought to blunt cellular responses to anticancer agents. The effects of several therapeutic agents were thus assessed for their death-inducing ability in XTC-1 cells. Cell viability experiments clearly showed that the cells were more resistant to stimuli which generate reactive oxygen species (tert-butylhydroperoxide) and to mitochondrial calcium-mediated apoptotic stimuli (C6-ceramide), as opposed to stimuli inflicting DNA damage (cisplatin) and damage to protein kinases(staurosporine). Various studies in the literature have reported that the peroxisome proliferator-activated receptor-coactivator 1(PGC-1α), which plays a fundamental role in mitochondrial biogenesis, is also involved in protecting cells against apoptosis caused by the former two types of stimuli. In accordance with these observations, real-time PCR experiments showed that XTC-1 cells express higher mRNA levels of this coactivator than do the control cells, implicating its importance in drug resistance. In conclusion, this study has revealed that XTC-1 cells, like many cancer cell lines, are characterised by a reduced energetic efficiency due to mitochondrial dysfunction. Said dysfunction has been attributed to mutations in respiratory genes encoded by the mitochondrial genome. Although the mechanism of cell demise in conditions of metabolic stress is unclear, the potential of targeting thyroid oncocytic cancers using glycolytic inhibitors has been illustrated. In addition, the discovery of mtDNA mutations in XTC-1 cells has enabled the use of this cell line as a model with which to study the relationship between Bcl-2 overexpression and oxidative phosphorylation in cells harbouring mtDNA mutations and also to investigate the significance of such mutations in establishing resistance to apoptotic stimuli.

Architectures for Context Aware Services in Smart Environments

This thesis deals with Context Aware Services, Smart Environments, Context Management and solutions for Devices and Service Interoperability. Multi-vendor devices offer an increasing number of services and end-user applications that base their value on the ability to exploit the information originating from the surrounding environment by means of an increasing number of embedded sensors, e.g. GPS, compass, RFID readers, cameras and so on. However, usually such devices are not able to exchange information because of the lack of a shared data storage and common information exchange methods. A large number of standards and domain specific building blocks are available and are heavily used in today's products. However, the use of these solutions based on ready-to-use modules is not without problems. The integration and cooperation of different kinds of modules can be daunting because of growing complexity and dependency. In this scenarios it might be interesting to have an infrastructure that makes the coexistence of multi-vendor devices easy, while enabling low cost development and smooth access to services. This sort of technologies glue should reduce both software and hardware integration costs by removing the trouble of interoperability. The result should also lead to faster and simplified design, development and, deployment of cross-domain applications. This thesis is mainly focused on SW architectures supporting context aware service providers especially on the following subjects: - user preferences service adaptation - context management - content management - information interoperability - multivendor device interoperability - communication and connectivity interoperability Experimental activities were carried out in several domains including Cultural Heritage, indoor and personal smart spaces – all of which are considered significant test-beds in Context Aware Computing. The work evolved within european and national projects: on the europen side, I carried out my research activity within EPOCH, the FP6 Network of Excellence on “Processing Open Cultural Heritage” and within SOFIA, a project of the ARTEMIS JU on embedded systems. I worked in cooperation with several international establishments, including the University of Kent, VTT (the Technical Reserarch Center of Finland) and Eurotech. On the national side I contributed to a one-to-one research contract between ARCES and Telecom Italia. The first part of the thesis is focused on problem statement and related work and addresses interoperability issues and related architecture components. The second part is focused on specific architectures and frameworks: - MobiComp: a context management framework that I used in cultural heritage applications - CAB: a context, preference and profile based application broker which I designed within EPOCH Network of Excellence - M3: "Semantic Web based" information sharing infrastructure for smart spaces designed by Nokia within the European project SOFIA - NoTa: a service and transport independent connectivity framework - OSGi: the well known Java based service support framework The final section is dedicated to the middleware, the tools and, the SW agents developed during my Doctorate time to support context-aware services in smart environments.

A model for diffusive and displacive phase transitions in steels

Heat treatment of steels is a process of fundamental importance in tailoring the properties of a material to the desired application; developing a model able to describe such process would allow to predict the microstructure obtained from the treatment and the consequent mechanical properties of the material. A steel, during a heat treatment, can undergo two different kinds of phase transitions [p.t.]: diffusive (second order p.t.) and displacive (first order p.t.); in this thesis, an attempt to describe both in a thermodynamically consistent framework is made; a phase field, diffuse interface model accounting for the coupling between thermal, chemical and mechanical effects is developed, and a way to overcome the difficulties arising from the treatment of the non-local effects (gradient terms) is proposed. The governing equations are the balance of linear momentum equation, the Cahn-Hilliard equation and the balance of internal energy equation. The model is completed with a suitable description of the free energy, from which constitutive relations are drawn. The equations are then cast in a variational form and different numerical techniques are used to deal with the principal features of the model: time-dependency, non-linearity and presence of high order spatial derivatives. Simulations are performed using DOLFIN, a C++ library for the automated solution of partial differential equations by means of the finite element method; results are shown for different test-cases. The analysis is reduced to a two dimensional setting, which is simpler than a three dimensional one, but still meaningful.