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.

Effetti del chitosano su composti polifenolici in colture cellulari di vite: aspetti molecolari e metabolici

Polyphenols, including flavonoids and stilbenes, are an essential part of human diet and constitute one of the most abundant and ubiquitous group of plant secondary metabolites. The level of these compounds is inducible by stress or fungal attack, so attempts are being made to identify likely biotic and abiotic elicitors and to better understand the underlying mechanism. Resveratrol (3,5,4’-trihydroxystilbene), which belongs to the stilbene family, is a naturally occurring polyphenol, found in several fruits, vegetables and beverages including red wine. It is one of the most important plant polyphenols with proved benefic activity on animal health. In the last two decades, the potential protective effects of resveratrol against cardiovascular and neurodegenerative diseases, as well as the chemopreventive properties against cancer, have been largely investigated. The most important source of polyphenols and in particular resveratrol for human diet is grape (Vitis vinifera). Since stilbenes and flavonoids play a very important role in plant defence responses and enviromental interactions, and their effects on human health seem promising, the aim of the research of this Thesis was to study at different levels the activation and the regulation of their biosynthetic pathways after chitosan treatment. Moreover, the polyphenol production in grape cells and the optimisation of cultural conditions bioreactor scale-up, were also investigated. Cell suspensions were obtained from cv. Barbera (Vitis vinifera L.) petioles and were treated with a biotic elicitor, chitosan (50 μg/mL, dissolved in acetic acid) to promote phenylpropanoid metabolism. Chitosan is a D-glucosamine polymer from fungi cell wall and therefore mimes fungal pathogen attack. Liquid cultures have been monitored for 15 days, measuring cell number, cell viability, pH and grams of fresh weight. The endogenous and released amounts of 7 stilbenes (trans and cis isomers of resveratrol, piceid and resveratroloside, and piceatannol), gallic acid, 6 hydroxycinnamic acids (trans-cinnamic, p-coumaric, caffeic, ferulic, sinapic and chlorogenic acids), 5 catechines (catechin, epicatechin, epigallocatechin-gallate (EGCG), epigallocatechin and epicatechin-gallate) and other 5 flavonoids (chalcon, naringenin, kaempferol, quercetin and rutin) in cells and cultural medium, were measured by HPLC-DAD analysis and total anthocyanins were quantified by spectrophotometric analysis. Chitosan was effective in stimulating trans-resveratrol endogenous accumulation with a sharp peak at day 4 (exceeding acetic acid and water controls by 36% and 63%, respectively), while it did not influence the production of the cis-isomer. Compared to both water and acetic acid controls, chitosan decreased the release of both trans- and cis-resveratrol respect to controls. No effect was shown on the accumulation of single resveratrol mono-glucoside isomers, but considering their total amount, normalized for the relative water control, it was possible to evidence an increase in both accumulation and release of those compounds, in chitosan-treated cells, throughout the culture period and particularly during the second week. Many of the analysed flavonoids and hydroxycinnamic acids were not present or detectable in trace amounts. Catechin, epicatechin and epigallocatechin-gallate (EGCG) were detectable both inside the cells and in the culture media, but chitosan did not affect their amounts. On the contrary, total anthocyanins have been stimulated by chitosan and their level, from day 4 to 14, was about 2-fold higher than in both controls, confirming macroscopic observations that treated suspensions showed an intense brown-red color, from day 3 onwards. These elicitation results suggest that chitosan selectively up-regulates specific biosynthetic pathways, without modifying the general accumulation pattern of other flavonoids. Proteins have been extracted from cells at day 4 of culture (corresponding to the production peak of trans-resveratrol) and separated by bidimensional electrophoresis. The 73 proteins that showed a consistently changed amount between untreated, chitosan and acetic acid (chitosan solvent) treated cells, have been identified by mass spectrometry. Chitosan induced an increase in stilbene synthase (STS, the resveratrol biosynthetic enzyme), chalcone-flavanone isomerase (CHI, that switches the pathway from chalcones to flavones and anthocyanins), pathogenesis-related proteins 10 (PRs10, a large family of defence proteins), and a decrease in many proteins belonging to primary metabolisms. A train of six distinct spots of STS encoded by the same gene and increased by chitosan, was detected on the 2-D gels, and related to the different phosphorylation degree of STS spots. Northern blot analyses have been performed on RNA extracted from cells treated with chitosan and relative controls, using probes for STS, PAL (phenylalanine ammonia lyase, the first enzyme of the biosynthetic pathway), CHS (chalcone synthase, that shares with STS the same precursors), CHI and PR-10. The up-regulation of PAL, CHS and CHI transcript expression levels correlated with the accumulation of anthocyanins. The strong increase of different molecular weight PR-10 mRNAs, correlated with the 11 PR-10 protein spots identified in proteomic analyses. The sudden decrease in trans-resveratrol endogenous accumulation after day 4 of culture, could be simply explained by the diminished resveratrol biosynthetic activity due to the lower amount of biosynthetic enzymes. This might be indirectly demonstrated by northern blot expression analyses, that showed lower levels of phenylalanine ammonia lyase (PAL) and stilbene synthase (STS) mRNAs starting from day 4. Other possible explanations could be a resveratrol oxidation process and/or the formation of other different mono-, di-glucosides and resveratrol oligomers such as viniferins. Immunolocalisation experiments performed on grape protoplasts and the subsequent analyses by confocal microscope, showed that STS, and therefore the resveratrol synthetic site, is mostly associated to intracellular membranes close to the cytosolic side of plasma membrane and in a smaller amount is localized in the cytosol. STS seemed not to be present inside vacuole and nucleus. There were no differences in the STS intracellular localisation between the different treatments. Since it was shown that stilbenes are largely released in the culture medium and that STS is a soluble protein, a possible interaction of STS with a plasma membrane transporter responsible for the extrusion of stilbenes in the culture medium, might be hypothesized. Proteomic analyses performed on subcellular fractions identified in the microsomial fraction 5 proteins taking part in channel complexes or associated with channels, that significantly changed their amount after chitosan treatment. In soluble and membrane fractions respectively 3 and 4 STS and 6 and 3 PR-10 have been identified. Proteomic results obtained from subcellular fractions substantially confirmed previous result obtained from total cell protein extracts and added more information about protein localisation and co-localisation. The interesting results obtained on Barbera cell cultures with the aim to increase polyphenol (especially stilbenes) production, have encouraged scale up tests in 1 litre bioreactors. The first trial fermentation was performed in parallel with a normal time-course in 20 mL flasks, showing that the scale-up (bigger volume and different conditions) process influenced in a very relevant way stilbenes production. In order to optimise culture parameters such as medium sucrose amount, fermentation length and inoculum cell concentration, few other fermentations were performed. Chitosan treatments were also performed. The modification of each parameter brought relevant variations in stilbenes and catechins levels, so that the production of a certain compound (or class of compounds) could be hypothetically promoted by modulating one or more culture parameters. For example the catechin yield could be improved by increasing sucrose content and the time of fermentation. The best results in stilbene yield were obtained in a 800 mL fermentation inoculated with 10.8 grams of cells and supplemented with chitosan. The culture was fed with MS medium added with 30 g/L sucrose, 25 μg/mL rifampicin and 50 μg/mL of chitosan, and was maintained at 24°C, stirred by marine impeller at 100 rpm and supplied of air at 0.16 L/min rate. Resveratroloside was the stilbene present in the larger amount, 3-5 times more than resveratrol. Because resveratrol glucosides are similarly active and more stable than free resveratrol, their production using a bioreactor could be a great advantage in an hypothetical industrial process. In my bioreactor tests, stilbenes were mainly released in the culture medium (60-80% of the total) and this fact could be another advantage for industrial applications, because it allows recovering the products directly from the culture medium without stopping the fermentation and/or killing the cells. In my best cultural conditions, it was possible to obtain 3.95 mg/L of stilbenes at day 4 (maximum resveratrol accumulation) and 5.13 mg/L at day 14 (maximum resveratroloside production). In conclusion, chitosan effect in inducing Vitis vinifera defense mechanisms can be related to its ability to increase the intracellular content of a large spectrum of antioxidants, and in particular of resveratrol, its derivates and anthocyanins. Its effect can be observed at transcriptional, proteomic (variation of soluble and membrane protein amounts) and metabolic (polyphenols production) level. The chitosan ability to elicit specific plant matabolisms can be useful to produce large quantities of antioxidant compounds from cell culture in bioreactor.

Ricerca, mediante tecniche di proteomica, di biomarcatori proteici utili nella valutazione della qualità degli alimenti di origine animale

In the last decades, the increase of industrial activities and of the request for the world food requirement, the intensification of natural resources exploitation, directly connected to pollution, have aroused an increasing interest of the public opinion towards initiatives linked to the regulation of food production, as well to the institution of a modern legislation for the consumer guardianship. This work was planned taking into account some important thematics related to marine environment, collecting and showing the data obtained from the studies made on different marine species of commercial interest (Chamelea gallina, Mytilus edulis, Ostrea edulis, Crassostrea gigas, Salmo salar, Gadus morhua). These studies have evaluated the effects of important physic and chemical parameters variations (temperature, xenobiotics like drugs, hydrocarbons and pesticides) on cells involved in the immune defence (haemocytes) and on some important enzymatic systems involved in xenobiotic biotransformation processes (cytochrome P450 complex) and in the related antioxidant defence processes (Superoxide dismutase, Catalase, Heat Shock Protein), from a biochemical and bimolecular point of view. Oxygen is essential in the biological answer of a living organism. Its consume in the normal cellular breathing physiological processes and foreign substances biotransformation, leads to reactive oxygen species (ROS) formation, potentially toxic and responsible of biological macromolecules damages with consequent pathologies worsening. Such processes can bring to a qualitative alteration of the derived products, but also to a general state of suffering that in the most serious cases can provoke the death of the organism, with important repercussions in economic field, in the output of the breedings, of fishing and of aquaculture. In this study it seemed interesting to apply also alternative methodologies currently in use in the medical field (cytofluorimetry) and in proteomic studies (bidimensional electrophoresis, mass spectrometry) with the aim of identify new biomarkers to place beside the traditional methods for the control of the animal origin food quality. From the results it’s possible to point out some relevant aspects from each experiment: 1. The cytofluorimetric techniques applied to O. edulis and C. gigas could bring to important developments in the search of alternative methods that quickly allows to identify with precision the origin of a specific sample, contributing to oppose possible alimentary frauds, in this case for example related to presence of a different species, also under a qualitative profile, but morpholgically similar. A concrete perspective for the application in the inspective field of this method has to be confirmed by further laboratory tests that take also in account in vivo experiments to evaluate the effect in the whole organism of the factors evaluated only on haemocytes in vitro. These elements suggest therefore the possibility to suit the cytofluorimetric methods for the study of animal organisms of food interest, still before these enter the phase of industrial working processes, giving useful information about the possible presence of contaminants sources that can induce an increase of the immune defence and an alteration of normal cellular parameter values. 2. C. gallina immune system has shown an interesting answer to benzo[a]pyrene (B[a]P) exposure, dose and time dependent, with a significant decrease of the expression and of the activity of one of the most important enzymes involved in the antioxidant defence in haemocytes and haemolymph. The data obtained are confirmed by several measurements of physiological parameters, that together with the decrease of the activity of 7-etossi-resourifine-O-deetilase (EROD linked to xenobiotic biotransformation processes) during exposure, underline the major effects of B[a]P action. The identification of basal levels of EROD supports the possible presence of CYP1A subfamily in the invertebrates, still today controversial, never identified previously in C. gallina and never isolated in the immune cells, as confirmed instead in this study with the identification of CYP1A-immunopositive protein (CYP1A-IPP). This protein could reveal a good biomarker at the base of a simple and quick method that could give clear information about specific pollutants presence, even at low concentrations in the environment where usually these organisms are fished before being commercialized. 3. In this experiment it has been evaluated the effect of the antibiotic chloramphenicol (CA) in an important species of commercial interest, Chamelea gallina. Chloramphenicol is a drug still used in some developing countries, also in veterinary field. Controls to evaluate its presence in the alimentary products of animal origin, can reveal ineffective whereas the concentration results to be below the limit of sensitivity of the instruments usually used in this type of analysis. Negative effects of CA towards the CYP1A- IPP proteins, underlined in this work, seem to be due to the attack of free radicals resultant from the action of the antibiotic. This brings to a meaningful alteration of the biotransformation mechanisms through the free radicals. It seems particularly interesting to pay attention to the narrow relationships in C. gallina, between SOD/CAT and CYP450 system, actively involved in detoxification mechanism, especially if compared with the few similar works today present about mollusc, a group that is composed by numerous species that enter in the food field and on which constant controls are necessary to evaluate in a rapid and effective way the presence of possible contaminations. 4. The investigations on fishes (Gadus morhua, and Salmo salar) and on a bivalve mollusc (Mytilus edulis) have allowed to evaluate different aspects related to the possibility to identify a biomarker for the evaluation of the health of organisms of food interest and consequently for the quality of the final product through 2DE methodologies. In the seafood field these techniques are currently used with a discreet success only for vertebrates (fishes), while in the study of the invertebrates (molluscs) there are a lot of difficulties. The results obtained in this work have underline several problems in the correct identification of the isolated proteins in animal organisms of which doesn’t currently exist a complete genomic sequence. This brings to attribute some identities on the base of the comparison with similar proteins in other animal groups, incurring in the possibility to obtain inaccurate data and above all discordant with those obtained on the same animals by other authors. Nevertheless the data obtained in this work after MALDI-ToF analysis, result however objective and the spectra collected could be again analyzed in the future after the update of genomic database related to the species studied. 4-A. The investigation about the presence of HSP70 isoforms directly induced by different phenomena of stress like B[a]P presence, has used bidimensional electrophoresis methods in C. gallina, that have allowed to isolate numerous protein on 2DE gels, allowing the collection of several spots currently in phase of analysis with MALDI-ToF-MS. The present preliminary work has allowed therefore to acquire and to improve important methodologies in the study of cellular parameters and in the proteomic field, that is not only revealed of great potentiality in the application in medical and veterinary field, but also in the field of the inspection of the foods with connections to the toxicology and the environmental pollution. Such study contributes therefore to the search of rapid and new methodologies, that can increase the inspective strategies, integrating themselves with those existing, but improving at the same time the general background of information related to the state of health of the considered animal organism, with the possibility, still hypothetical, to replace in particular cases the employment of the traditional techniques in the alimentary field.

Sistemi liquido cristallini complessi: simulazioni al calcolatore e studi ESR

The aim of this PhD thesis was to study at a microscopic level different liquid crystal (LC) systems, in order to determine their physical properties, resorting to two distinct methodologies, one involving computer simulations, and the other spectroscopic techniques, in particular electron spin resonance (ESR) spectroscopy. By means of the computer simulation approach we tried to demonstrate this tool effectiveness for calculating anisotropic static properties of a LC material, as well as for predicting its behaviour and features. This required the development and adoption of suitable molecular models based on a convenient intermolecular potentials reflecting the essential molecular features of the investigated system. In particular, concerning the simulation approach, we have set up models for discotic liquid crystal dimers and we have studied, by means of Monte Carlo simulations, their phase behaviour and self­-assembling properties, with respect to the simple monomer case. Each discotic dimer is described by two oblate Gay­Berne ellipsoids connected by a flexible spacer, modelled by a harmonic "spring" of three different lengths. In particular we investigated the effects of dimerization on the transition temperatures, as well as on the characteristics of molecular aggregation displayed and the relative orientational order. Moving to the experimental results, among the many experimental techniques that are typically employed to evaluate LC system distinctive features, ESR has proved to be a powerful tool in microscopic scale investigation of the properties, structure, order and dynamics of these materials. We have taken advantage of the high sensitivity of the ESR spin probe technique to investigate increasingly complex LC systems ranging from devices constituted by a polymer matrix in which LC molecules are confined in shape of nano- droplets, as well as biaxial liquid crystalline elastomers, and dimers whose monomeric units or lateral groups are constituted by rod-like mesogens (11BCB). Reflection-mode holographic-polymer dispersed liquid crystals (H-PDLCs) are devices in which LCs are confined into nanosized (50­-300 nm) droplets, arranged in layers which alternate with polymer layers, forming a diffraction grating. We have determined the configuration of the LC local director and we have derived a model of the nanodroplet organization inside the layers. Resorting also to additional information on the nanodroplet size and shape distribution provided by SEM images of the H-PDLC cross-section, the observed director configuration has been modeled as a bidimensional distribution of elongated nanodroplets whose long axis is, on the average, parallel to the layers and whose internal director configuration is a uniaxial quasi- monodomain aligned along the nanodroplet long axis. The results suggest that the molecular organization is dictated mainly by the confinement, explaining, at least in part, the need for switching voltages significantly higher and the observed faster turn-off times in H-PDLCs compared to standard PDLC devices. Liquid crystal elastomers consist in cross-linked polymers, in which mesogens represent the monomers constituting the main chain or the laterally attached side groups. They bring together three important aspects: orientational order in amorphous soft materials, responsive molecular shape and quenched topological constraints. In biaxial nematic liquid crystalline elastomers (BLCEs), two orthogonal directions, rather than the one of normal uniaxial nematic, can be controlled, greatly enhancing their potential value for applications as novel actuators. Two versions of a side-chain BLCEs were characterized: side­-on and end­-on. Many tests have been carried out on both types of LCE, the main features detected being the lack of a significant dynamical behaviour, together with a strong permanent alignment along the principal director, and the confirmation of the transition temperatures already determined by DSC measurements. The end­-on sample demonstrates a less hindered rotation of the side group mesogenic units and a greater freedom of alignment to the magnetic field, as already shown by previous NMR studies. Biaxial nematic ESR static spectra were also obtained on the basis of Molecular Dynamics generated biaxial configurations, to be compared to the experimentally determined ones, as a mean to establish a possible relation between biaxiality and the spectral features. This provides a concrete example of the advantages of combining the computer simulation and spectroscopic approaches. Finally, the dimer α,ω-bis(4'-cyanobiphenyl-4-yl)undecane (11BCB), synthesized in the "quest" for the biaxial nematic phase has been analysed. Its importance lies in the dimer significance as building blocks in the development of new materials to be employed in innovative technological applications, such as faster switching displays, resorting to the easier aligning ability of the secondary director in biaxial phases. A preliminary series of tests were performed revealing the population of mesogenic molecules as divided into two groups: one of elongated straightened conformers sharing a common director, and one of bent molecules, which display no order, being equally distributed in the three dimensions. Employing this model, the calculated values show a consistent trend, confirming at the same time the transition temperatures indicated by the DSC measurements, together with rotational diffusion tensor values that follow closely those of the constituting monomer 5CB.

Stochastic models and dynamic measures for the characterization of bistable circuits

During the last few years, a great deal of interest has risen concerning the applications of stochastic methods to several biochemical and biological phenomena. Phenomena like gene expression, cellular memory, bet-hedging strategy in bacterial growth and many others, cannot be described by continuous stochastic models due to their intrinsic discreteness and randomness. In this thesis I have used the Chemical Master Equation (CME) technique to modelize some feedback cycles and analyzing their properties, including experimental data. In the first part of this work, the effect of stochastic stability is discussed on a toy model of the genetic switch that triggers the cellular division, which malfunctioning is known to be one of the hallmarks of cancer. The second system I have worked on is the so-called futile cycle, a closed cycle of two enzymatic reactions that adds and removes a chemical compound, called phosphate group, to a specific substrate. I have thus investigated how adding noise to the enzyme (that is usually in the order of few hundred molecules) modifies the probability of observing a specific number of phosphorylated substrate molecules, and confirmed theoretical predictions with numerical simulations. In the third part the results of the study of a chain of multiple phosphorylation-dephosphorylation cycles will be presented. We will discuss an approximation method for the exact solution in the bidimensional case and the relationship that this method has with the thermodynamic properties of the system, which is an open system far from equilibrium.In the last section the agreement between the theoretical prediction of the total protein quantity in a mouse cells population and the observed quantity will be shown, measured via fluorescence microscopy.

Fluidodinamica biomedica computazionale del flusso sanguigno in presenza di affezioni strumentali e/o patologiche

La tesi di Dottorato studia il flusso sanguigno tramite un codice agli elementi finiti (COMSOL Multiphysics). Nell’arteria è presente un catetere Doppler (in posizione concentrica o decentrata rispetto all’asse di simmetria) o di stenosi di varia forma ed estensione. Le arterie sono solidi cilindrici rigidi, elastici o iperelastici. Le arterie hanno diametri di 6 mm, 5 mm, 4 mm e 2 mm. Il flusso ematico è in regime laminare stazionario e transitorio, ed il sangue è un fluido non-Newtoniano di Casson, modificato secondo la formulazione di Gonzales & Moraga. Le analisi numeriche sono realizzate in domini tridimensionali e bidimensionali, in quest’ultimo caso analizzando l’interazione fluido-strutturale. Nei casi tridimensionali, le arterie (simulazioni fluidodinamiche) sono infinitamente rigide: ricavato il campo di pressione si procede quindi all’analisi strutturale, per determinare le variazioni di sezione e la permanenza del disturbo sul flusso. La portata sanguigna è determinata nei casi tridimensionali con catetere individuando tre valori (massimo, minimo e medio); mentre per i casi 2D e tridimensionali con arterie stenotiche la legge di pressione riproduce l’impulso ematico. La mesh è triangolare (2D) o tetraedrica (3D), infittita alla parete ed a valle dell’ostacolo, per catturare le ricircolazioni. Alla tesi sono allegate due appendici, che studiano con codici CFD la trasmissione del calore in microcanali e l’ evaporazione di gocce d’acqua in sistemi non confinati. La fluidodinamica nei microcanali è analoga all’emodinamica nei capillari. Il metodo Euleriano-Lagrangiano (simulazioni dell’evaporazione) schematizza la natura mista del sangue. La parte inerente ai microcanali analizza il transitorio a seguito dell’applicazione di un flusso termico variabile nel tempo, variando velocità in ingresso e dimensioni del microcanale. L’indagine sull’evaporazione di gocce è un’analisi parametrica in 3D, che esamina il peso del singolo parametro (temperatura esterna, diametro iniziale, umidità relativa, velocità iniziale, coefficiente di diffusione) per individuare quello che influenza maggiormente il fenomeno.

Envy: A Psychometric Refinement of the Construct

The noticeable differences in the theoretical and operative definitions of envy across studies and approaches have produced a fragmentary representation and understanding of the envious emotion. The present dissertation aimed to clarify the inherent nature of the construct of envy through the integration of findings from three independent studies. We focused on malicious envy, and investigated it from both a dispositional and an episodic perspective. Studies 1 and 2 investigated the dimensionality of envy as a stable individual characteristic and an episodic emotional state, respectively. In order to elicit episodic envy, a scenario-based experiment was conducted. Results indicated that, in both its dispositional and episodic facets, envy is a bidimensional construct composed by an inner-directed dimension of inferiority and helplessness, and an outer-directed dimension of feelings of anger and ill will. Moreover, findings from Study 1 allowed to establish boundaries between envy and competing constructs that have often been included in conceptualizations of envy. The psychometrically validated definition of envy provided by Studies 1 and 2 represents a valuable contribution to empirical research. Implications for envy research concern the promotion of a shared operationalization of envy in future studies, which will arguably facilitate the comparison of findings between studies and between approaches. Study 3 examined the mechanisms through which dispositional envy affects individuals’ social adjustment and psychological wellbeing. Findings revealed that the detrimental effects of envy on perceived social support and subjective well-being are mostly mediated by other personal characteristics, such as neuroticism and self-esteem. By reducing global self-esteem, the envious disposition may damage supportive social networks via antisocial direct and indirect behaviors that may arise from envy and that are likely to drive others away. On the other hand, by damaging both emotional stability and self-worth, dispositional envy leads to reduced subjective well-being. Implications for clinical practice are discussed.