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.

Effects of environmental complexity on neurogenesis in the hippocampal dentate gyrus

Introduction. Postnatal neurogenesis in the hippocampal dentate gyrus, can be modulated by numerous determinants, such as hormones, transmitters and stress. Among the factors positively interfering with neurogenesis, the complexity of the environment appears to play a particularly striking role. Adult mice reared in an enriched environment produce more neurons and exhibit better performance in hippocampus-specific learning tasks. While the effects of complex environments on hippocampal neurogenesis are well documented, there is a lack of information on the effects of living under socio-sensory deprivation conditions. Due to the immaturity of rats and mice at birth, studies dealing with the effects of environmental enrichment on hippocampal neurogenesis were carried out in adult animals, i.e. during a period of relatively low rate of neurogenesis. The impact of environment is likely to be more dramatic during the first postnatal weeks, because at this time granule cell production is remarkably higher than at later phases of development. The aim of the present research was to clarify whether and to what extent isolated or enriched rearing conditions affect hippocampal neurogenesis during the early postnatal period, a time window characterized by a high rate of precursor proliferation and to elucidate the mechanisms underlying these effects. The experimental model chosen for this research was the guinea pig, a precocious rodent, which, at 4-5 days of age can be independent from maternal care. Experimental design. Animals were assigned to a standard (control), an isolated, or an enriched environment a few days after birth (P5-P6). On P14-P17 animals received one daily bromodeoxyuridine (BrdU) injection, to label dividing cells, and were sacrificed either on P18, to evaluate cell proliferation or on P45, to evaluate cell survival and differentiation. Methods. Brain sections were processed for BrdU immunhistochemistry, to quantify the new born and surviving cells. The phenotype of the surviving cells was examined by means of confocal microscopy and immunofluorescent double-labeling for BrdU and either a marker of neurons (NeuN) or a marker of astrocytes (GFAP). Apoptotic cell death was examined with the TUNEL method. Serial sections were processed for immunohistochemistry for i) vimentin, a marker of radial glial cells, ii) BDNF (brain-derived neurotrofic factor), a neurotrophin involved in neuron proliferation/survival, iii) PSA-NCAM (the polysialylated form of the neural cell adhesion molecule), a molecule associated with neuronal migration. Total granule cell number in the dentate gyrus was evaluated by stereological methods, in Nissl-stained sections. Results. Effects of isolation. In P18 isolated animals we found a reduced cell proliferation (-35%) compared to controls and a lower expression of BDNF. Though in absolute terms P45 isolated animals had less surviving cells than controls, they showed no differences in survival rate and phenotype percent distribution compared to controls. Evaluation of the absolute number of surviving cells of each phenotype showed that isolated animals had a reduced number of cells with neuronal phenotype than controls. Looking at the location of the new neurons, we found that while in control animals 76% of them had migrated to the granule cell layer, in isolated animals only 55% of the new neurons had reached this layer. Examination of radial glia cells of P18 and P45 animals by vimentin immunohistochemistry showed that in isolated animals radial glia cells were reduced in density and had less and shorter processes. Granule cell count revealed that isolated animals had less granule cells than controls (-32% at P18 and -42% at P45). Effects of enrichment. In P18 enriched animals there was an increase in cell proliferation (+26%) compared to controls and a higher expression of BDNF. Though in both groups there was a decline in the number of BrdU-positive cells by P45, enriched animals had more surviving cells (+63) and a higher survival rate than controls. No differences were found between control and enriched animals in phenotype percent distribution. Evaluation of the absolute number of cells of each phenotype showed that enriched animals had a larger number of cells of each phenotype than controls. Looking at the location of cells of each phenotype we found that enriched animals had more new neurons in the granule cell layer and more astrocytes and cells with undetermined phenotype in the hilus. Enriched animals had a higher expression of PSA-NCAM in the granule cell layer and hilus Vimentin immunohistochemistry showed that in enriched animals radial glia cells were more numerous and had more processes.. Granule cell count revealed that enriched animals had more granule cells than controls (+37% at P18 and +31% at P45). Discussion. Results show that isolation rearing reduces hippocampal cell proliferation but does not affect cell survival, while enriched rearing increases both cell proliferation and cell survival. Changes in the expression of BDNF are likely to contribute to he effects of environment on precursor cell proliferation. The reduction and increase in final number of granule neurons in isolated and enriched animals, respectively, are attributable to the effects of environment on cell proliferation and survival and not to changes in the differentiation program. As radial glia cells play a pivotal role in neuron guidance to the granule cell layer, the reduced number of radial glia cells in isolated animals and the increased number in enriched animals suggests that the size of radial glia population may change dynamically, in order to match changes in neuron production. The high PSA-NCAM expression in enriched animals may concur to favor the survival of the new neurons by facilitating their migration to the granule cell layer. Conclusions. By using a precocious rodent we could demonstrate that isolated/enriched rearing conditions, at a time window during which intense granule cell proliferation takes place, lead to a notable decrease/increase of total granule cell number. The time-course and magnitude of postnatal granule cell production in guinea pigs are more similar to the human and non-human primate condition than in rats and mice. Translation of current data to humans would imply that exposure of children to environments poor/rich of stimuli may have a notably large impact on dentate neurogenesis and, very likely, on hippocampus dependent memory functions.

Come tradurre il metadiscorso letterario. Esempi di scrittura femminile nell'Ottocento austriaco

L’argomento affrontato nel presente lavoro di tesi dal titolo “Come tradurre il metadiscorso letterario. Esempi di scrittura femminile nell’Ottocento austriaco” è la versione interlinguistica di testi saggistici afferenti all’ambito del metadiscorso letterario. Nello specifico, non vengono analizzati testi di critica e/o metodologia ma scritti funzionali, di forte carattere pragmatico, che pur tuttavia rientrano tra le testimonianze di alta caratura letteraria, perché dovuti ad autrici che hanno fatto dell’espressione estetica la propria finalità primaria. I materiali scelti per l’analisi linguistico-testuale, compresi in un arco temporale tra la fine del Settecento e la metà dell’Ottocento, sono realizzati da donne che hanno operato in ambito teatrale facendo dell’attività di scrittura lo strumento della propria emancipazione intellettuale ed economica. La necessità di trovare una via alla pubblicazione le ha indotte a strategie di scrittura connotate da particolari stilemi e artifici retorici atti a favorire l’accettazione e la diffusione delle proposte editoriali di cui questi “paratesti” costituivano il momento giustificante. Il “lavoro di penna” è un’esperienza che viene ad assumere molteplici contorni, non privi di ricadute al momento della scelta delle strategie traduttive. Dal punto di vista formale, le testimonianze si collocano in una zona di modalità espressiva contigua alla testimonianza autobiografica. Il periodo storico e l’area di provenienza delle autrici hanno reso necessario un approccio capace di incrociare il piano diacronico con la dimensione diatopica, rendendo conto delle componenti diamesiche di una scrittura che nasce dal teatro per il teatro e ad esso e ai suoi frequentatori deve rapportarsi. Il modello traduttologico applicato ricava le sue linee fondamentali dalle riflessioni della linguistica testuale e dall’approccio integrato/multidisciplinare della “prototipologia dinamica”.

Durability of crystalline monumental stones in terms of their petrophysical characteristics

The durability of stone building materials is an issue of utmost importance in the field of monument conservation. In order to be able to preserve our built cultural heritage, the thorough knowledge of its constituent materials and the understanding of the processes that affect them are indispensable. The main objective of this research was to evaluate the durability of a special stone type, the crystalline stones, in correlation with their intrinsic characteristics, the petrophysical properties. The crystalline stones are differentiated from the cemented stones on the basis of textural features. Their most important specific property is the usually low, fissure-like porosity. Stone types of significant monumental importance, like the marble or granite belong to this group. The selected materials for this investigation, indeed, are a marble (Macael marble, Spain) and a granite (Silvestre Vilachán granite, Spain). In addition, an andesite (Szob andesite, Hungary) also of significant monumental importance was selected. This way a wide range of crystalline rocks is covered in terms of petrogenesis: stones of metamorphic, magmatic and volcanic origin, which can be of importance in terms of mineralogical, petrological or physical characteristics. After the detailed characterization of the petrophysical properties of the selected stones, their durability was assessed by means of artificial ageing. The applied ageing tests were: the salt crystallization, the frost resistance in pure water and in the presence of soluble salts, the salt mist and the action of SO2 in the presence of humidity. The research aimed at the understanding of the mechanisms of each weathering process and at finding the petrophysical properties most decisive in the degradation of these materials. Among the several weathering mechanisms, the most important ones were found to be the physical stress due to crystallization pressure of both salt and ice, the thermal fatigue due to cyclic temperature changes and the chemical reactions (mostly the acidic attack) between the mineral phases and the external fluids. The properties that fundamentally control the degradation processes, and thus the durability of stones were found to be: the mineralogical and chemical composition; the hydraulic properties especially the water uptake, the permeability and the drying; the void space structure, especially the void size and aperture size distribution and the connectivity of the porous space; and the thermal and mechanical properties. Because of the complexity of the processes and the high number of determining properties, no mechanisms or characteristics could be identified as typical for crystalline stones. The durability or alterability of each stone type must be assessed according to its properties and not according to the textural or petrophysical classification they belong to. Finally, a critical review of standardized methods is presented, based on which an attempt was made for recommendations of the most adequate methodology for the characterization and durability assessment of crystalline stones.

Il concetto di sezione nel metodo compositivo di Aldo Rossi.

Purpose of this research is to deepen the study on the section in architecture. The survey aims as important elements in the project Teatro Domestico by Aldo Rossi built for the XVII Triennale di Milano in 1986 and, through the implementation on several topics of architecture, verify the timeliness and fertility in the new compositional exercises. Through the study of certain areas of the Rossi’s theory we tried to find a common thread for the reading of the theater project. The theater is the place of the ephemeral and the artificial, which is why his destiny is the end and the fatal loss. The design and construction of theater setting has always had a double meaning between the value of civil architecture and testing of new technologies available. Rossi's experience in this area are clear examples of the inseparable relationship between the representation of architecture as art and design of architecture as a model of reality. In the Teatro Domestico, the distinction between representation and the real world is constantly canceled and returned through the reversal of the meaning and through the skip of scale. At present, studies conducted on the work of Rossi concern the report that the architectural composition is the theory of form, focusing compositional development of a manufacturing process between the typological analysis and form invention. The research, through the analysis of some projects few designs, will try to analyze this issue through the rules of composition both graphical and concrete construction, hoping to decipher the mechanism underlying the invention. The almost total lack of published material on the project Teatro Domestico and the opportunity to visit the archives that preserve the drawings, has allowed the author of this study to deepen the internal issues in the project, thus placing this search as a first step toward possible further analysis on the works of Rossi linked to performance world. The final aim is therefore to produce material that can best describe the work of Rossi. Through the reading of the material published by the same author and the vision of unpublished material preserved in the archives, it was possible to develop new material and increasing knowledge about the work, otherwise difficult to analyze. The research is divided into two groups. The first, taking into account the close relationship most frequently mentioned by Rossi himself between archeology and architectural composition, stresses the importance of tipo such as urban composition reading system as well as open tool of invention. Resuming Ezio Bonfanti’s essay on the work of the architect we wanted to investigate how the paratactic method is applied to the early work conceived and, subsequently as the process reaches a complexity accentuated, while keeping stable the basic terms. Following a brief introduction related to the concept of the section and the different interpretations that over time the term had, we tried to identify with this facility a methodology for reading Rossi’s projects. The result is a constant typological interpretation of the term, not only related to the composition in plant but also through the elevation plans. The section is therefore intended as the overturning of such elevation is marked on the same plane of the terms used, there is a different approach, but a similarity of characters. The identification of architectural phonemes allows comparison with other arts. The research goes in the direction of language trying to identify the relationship between representation and construction, between the ephemeral and the real world. In this sense it will highlight the similarities between the graphic material produced by Ross and some important examples of contemporary author. The comparison between the composition system with the surrealist world of painting and literature will facilitate the understanding and identification of possible rules applied by Rossi. The second part of the research is characterized by a focus on the intent of the project chosen. Teatro Domestico embodies a number of elements that seem to conclude (assuming an end point but also to start) a curriculum author. With it, the experiments carried out on the theater started with the project for the Teatrino Scientifico (1978) through the project for the Teatro del Mondo (1979), into a Laic Tabernacle representative collective and private memory of the city. Starting from a reading of the draft, through the collection of published material, we’ve made an analysis on the explicit themes of the work, finding the conceptual references. Following the taking view of the original materials not published kept at Aldo Rossi's Archive Collection of the Canadian Center for Architecture in Montréal, will be implemented through the existing techniques for digital representation, a virtual reconstruction of the project, adding little to the material, a new element for future studies. The reconstruction is part of a larger research studies where the current technologies of composition and representation in architecture stand side by side with research on the method of composition of this architect. The results achieved are in addition to experiences in the past dealt with the reconstruction of some of the lost works of Aldo Rossi. A partial objective is to reactivate a discourse around this work is considered non-principal, among others born in the prolific activities. Reassessment of development projects which would bring the level of ephemeral works most frequented by giving them the value earned. In conclusion, the research aims to open a new field of interest on the part not only as a technical instrument of representation of an idea but as an actual mechanism through which composition is formed and the idea is developed.

L'attitudine alla comunicazione. Uno studio nel Corso di Laurea in Infermieristica

It is believed that the way of being and the communicative-relational skills of every individual have multifactorial origins, including the quality of primary relationships with caregivers. For some time, the need for health care professionals to possess specific communicative and interpersonal skills has been highlighted. To the degree course in Nursing, like to all other degree programs related to health, access is granted to students who have large individual differences, both in terms of personality, and in terms of relational skills. Each academic year, therefore, the people responsible for the didactic organization of every course, are faced with having to prepare a training plan capable of addressing communicative-relational aspects and, at the same time, of being adequate to the real attitudes of incoming students. Thus, the need for appropriate tools for measuring the personological and vocational traits considered specific to health professions was born. This study has a twofold objective. On one hand, it aims at selecting a battery of psychological tests to detect psychological and attitudinal patterns, to facilitate the coordinators of graduate courses in their didactic organization and planning of educational training; on the other hand, it seeks to assess the correlations between communicative-relational skills (Relational-Communicative style, according to the model of patient-centered medicine-TRS) (Mucchielli’s Test of Spontaneous Attitudes – usual kind of attitude in dual relationships), personality traits (Alexithymia), styles of attachment to parental figures (PBI), and the capability of recognizing facial emotions, in a sample of students enrolled in the first year of a degree in Nursing.

La salute detenuta: tra diritto e sicurezza”. Un’ indagine nella Casa Circondariale di Rimini.

The survey approachs the issue of health and the problem of its effective protection in a context of deprivation of liberty and coercion, which is the prison. The theoretical reflection born from the reform of the Legislative Decree 230/99 which marked the transition from an employee by the Prison Health within prison a fully integrated in the National Health Service. The comparison between an institution of health promotion and institution of punishment which may operate on the same subject held produces multiple attrits, making their relationship problematic. The work shows the daily difficulties in the management of prison health within the institution, physician-patient between different health care roles, and between the latter and prison workers. The coexistence, in fact, is not always harmonious though quite often it is common sense and the willingness of operators to reduce barriers: overcrowding, limited resources and insufficient staff make the application of the rule and therefore the right to goal a difficult to be pursued. It is designed for a scheme of semi-structured interview essay is divided into 3 sections covering: "staff and its functions", "health reform" and "health of the prisoner"; questions were directed to doctors, nurses and psychologists engaged inside the prison of Rimini with the specific aim of examining the ambivalent relationship between the demand for health care in prisons and the need for security and a clear - albeit partial - point of view. We tried to reconstruct the situation of prison health care through the perception of prison operators, capturing the problematic issues that deal on both issues is instrumental to the experience of persons detained by analyzing, in terms of operators , what happens inside of a prison institution in everyday health care.

Il Lessico d’amore nei primi tre libri delle Odi di Orazio

Il presente studio si è posto come obiettivo quello di redigere un lessico dei termini d’amore nella poesia di Orazio, e, specificamente, dei lemmi presenti nei primi tre libri delle Odi. L’interesse per la lirica del Venosino ci ha indotti ad affrontarne la lettura non solo considerando quelle che sono le tematiche diremo topiche della sua poetica ( modus, angulus, mors, tempus, cura, solo per citare quelle più significative ), ma anche quelle meno note, quale appunto il tema dell’amore, oggetto di questo lavoro. Si è proceduto così all’analisi di ogni singolo libro di ogni ode, catalogandone ed analizzandone rispettivamente tutte le occorrenze di quei termini che abbiamo ritenuto essere propri del lessico amoroso. Il commento ad ogni libro è stato supportato dagli studi di Nisbet-Hubbard per il primo ed il secondo libro delle Odi ( cfr. R.G.M. Nisbet-M. Hubbard, A commentary on Horace: Odes Book 1, Oxford 1970; R.G.M. Nisbet-M. Hubbard, A commentary on Horace: Odes Book 2, Oxford 1978 ) e Nisbet-Rudd per il terzo ( cfr. R.G.M. Nisbet-Rudd, A commentary on Horace: Odes Book 3, Oxford, 2003 ). Trattandosi di un lessico è stato altresì fondamentale il contributo dell’ Index uerborum amatorium ( Cfr. R. Pichon, De sermone amatorio apud Latinos elegiarum scriptores, Paris 1902 ) e del ThLL. Si è infine proceduto ad individuare quei termini maggiormente significativi nell’ambito della poesia d’amore in generale, il cui riflesso è presente anche nella poesia oraziana, con una particolare attenzione al rapporto che intercorre tra Orazio e la tradizione neoterica ed elegiaca e al lessico dei colori, che vanta numerose occorrenze nella poesia d’amore, soprattutto in riferimento alla bellezza muliebre e maschile e che quindi appare di rilevante importanza per comprendere l’estetica della poesia oraziana nel ritrarre la forma degli amanti che popolano i suoi più celebri versi d’amore.

Monismo e dualismo nei rapporti tra Cedu e ordinamento costituzionale interno. Fonti e processi interpretativi

La tesi analizza i rapporti tra l’ordinamento italiano e la Cedu, in particolare la collocazione della Cedu all’interno del sistema delle fonti alla luce della modifica dell’art. 117, comma 1 Cost. Si tratta di un tema molto dibattuto in dottrina, specialmente a seguito dell’entrata in vigore del Trattato di Lisbona. Questa tematica risulta strettamente connessa al profilo dell’interazione tra la Corte di Strasburgo e la Corte costituzionale e i giudici ordinari. L’analisi del profilo statico concernente lo status della Cedu nel sistema italiano deve quindi essere accompagnata dall’esame del profilo dinamico, relativo al ruolo della giurisprudenza della Corte di Strasburgo nell’esperienza dell’ordinamento nazionale. Entrambi i profili di indagine sono esaminati alla luce delle indicazioni provenienti dalla giurisprudenza della Corte costituzionale, della Corte di Cassazione e della Corte di Strasburgo. Prima di essere esaminate singolarmente, queste tematiche richiedono la preliminare ricognizione dei termini della dicotomia tra i due modelli concettuali di riferimento in tema di rapporti interordinamentali: il monismo e il dualismo. Trasferite nel peculiare contesto del sistema Cedu, tali categorie dogmatiche si arricchiscono di ulteriori profili, che esorbitano dalla sistemazione del rapporto tra fonti. La tenuta dei due paradigmi concettuali, che sono nati ed operano nel contesto della teorica delle fonti, deve essere verificata anche rispetto all’attuale fenomeno della produzione europea di diritto giurisprudenziale ed alla capacità paradigmatica assunta dalla giurisprudenza di Strasburgo. Il diritto e le istituzioni giuridiche tendono ad assumere sempre più sembianze giurisdizionali, generando un’osmosi che porta a trasferire il focus dai rapporti interordinamentali ai rapporti tra giurisprudenze.

Geomorphological and statistical analysis on Ravenna dune fields changes, based on Terrestrial Laser Technology

Coastal sand dunes represent a richness first of all in terms of defense from the sea storms waves and the saltwater ingression; moreover these morphological elements constitute an unique ecosystem of transition between the sea and the land environment. The research about dune system is a strong part of the coastal sciences, since the last century. Nowadays this branch have assumed even more importance for two reasons: on one side the born of brand new technologies, especially related to the Remote Sensing, have increased the researcher possibilities; on the other side the intense urbanization of these days have strongly limited the dune possibilities of development and fragmented what was remaining from the last century. This is particularly true in the Ravenna area, where the industrialization united to the touristic economy and an intense subsidence, have left only few dune ridges residual still active. In this work three different foredune ridges, along the Ravenna coast, have been studied with Laser Scanner technology. This research didn’t limit to analyze volume or spatial difference, but try also to find new ways and new features to monitor this environment. Moreover the author planned a series of test to validate data from Terrestrial Laser Scanner (TLS), with the additional aim of finalize a methodology to test 3D survey accuracy. Data acquired by TLS were then applied on one hand to test some brand new applications, such as Digital Shore Line Analysis System (DSAS) and Computational Fluid Dynamics (CFD), to prove their efficacy in this field; on the other hand the author used TLS data to find any correlation with meteorological indexes (Forcing Factors), linked to sea and wind (Fryberger's method) applying statistical tools, such as the Principal Component Analysis (PCA).