Molecular detection of Leishmania spp. in road-killed wild mammals in the Central Western area of the State of São Paulo, Brazil

Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)

Application of an auditory steady-state response test to evaluate the attenuation of hearing protection devices

This research aims to present a new method to get real attenuation of hearing protection devices, with good reproducibility and a small standard deviation, without relying on skills and cooperation individual. Thus the authors performed tests in 10 individuals without protection and after with two kinds of ear protections (ear plug and ear muffs), to get the threshold limit value in each of the 3 stages. For this, the research used an electrophysical exam, normally used in speech therapy, named ASSR (auditory steady-state response). The principle of this exam is put on individual’s head 3 electrodes, to capture electrical signs directly in auditory nerve. In summary, the authors presented the final results. The method proposed by ANSI (American National Standards Institute) indicated an attenuation of 27.6 dB for ear plugs, while the value found in this work was 16 dB; and for ear muffs, the ANSI method indicated 29.8 dB while the value found here was 28.5 dB.

Comunicação pública e acesso à informação: análise da atuação da SABESP em plataformas virtuais

This undergraduate research final paper analyzed the communication process carried out by the São Paulo State Water and Sanitation Company - Sabesp from the perspective of public communication, social capital and right to information theories. By monitoring Sabesp's institutional fanpage and website from 24 to 30 August 2015, it sought to assess the performance of Sabesp in disclosing public information on the context of the water supply crisis in São Paulo, concerning the fulfillment of requirements of the Right to Information Law (12.527/2011) and the need for interaction and dialogue between the institution and its stakeholders, taken as principles of public communication. The results suggest that digital media can enhance information flow and contribute to foster public relations and civic participation, but there are opportunities for Sabesp to improve communication and reach greater transparency

Selecting for rust (Puccinia psidii) reistance in Euclyptus grandis in São Paulo state, Brazil

In Brazil, Eucalyptus grandis is a key species for wood production. However, some genotypes are susceptible to rust (Puccinia psidii), mainly in São Paulo State, where climatic conditions are favorable for its development. Rust represents a high economic risk to forest companies because of the high potential of damage to commercial eucalypt plantations. The aims of the present study were (i) to select progenies of E. grandis for stability and adaptability regarding resistance to rust at different locations; (ii) compare the selections under these different climatic conditions; and (iii) compare rust severity in the field with the theoretical model. We observed that climatic conditions were extremely influential factors for rust development, but even under favorable conditions for disease development, we found rust-resistant progenies. In sites unfavorable for rust development, we detected highly susceptible progenies. We found significant correlation among the genetic material, environmental conditions and disease symptoms, however, we observed a simple genotype-environmental interaction and significant genetic variability among the progenies. The average heritability was high among the progenies in all sites, indicating substantial genetic control for rust resistance. We also observed a good relationship between rust severity in the field and the theoretical model that considered annual average temperature and leaf wetness.

Interaction between Trypanosoma rangeli and the Rhodnius prolixus salivary gland depends on the phosphotyrosine ecto-phosphatase activity of the parasite

Trypanosoma rangeli is the trypanosomatid that colonizes the salivary gland of its insect vector, with a profound impact on the feeding capacity of the insect. In this study we investigated the role of the phosphotyrosine (P-Tyr) ecto-phosphatase activity of T. rangeli in its interaction with Rhodnius prolixus salivary glands. Long but not short epimastigotes adhered to the gland cells and the strength of interaction correlated with the enzyme activity levels in different strains. Differential interference contrast microscopy demonstrated that clusters of parasites are formed in most cases, suggesting cooperative interaction in the adhesion process. The tightness of the correlation was evidenced by modulating the P-Tyr ecto-phosphatase activity with various concentrations of inhibitors. Sodium orthovanadate, ammonium molybdate and zinc chloride decreased the interaction between T. rangeli and R. prolixus salivary glands in parallel. Levamisole, an inhibitor of alkaline phosphatases, affected neither process. EDTA strongly inhibited adhesion and P-Tyr ecto-phosphatase activity to the same extent, an effect that was no longer seen if the parasites were pre-incubated with the chelator and then washed. When the P-Tyr ecto-phosphatase of living T. ranged epimastigotes was irreversibly inactivated with sodium orthovanadate and the parasite cells were then injected into the insect thorax, colonization of the salivary glands was greatly depressed for several days after blood feeding. Addition of P-Tyr ecto-phosphatase substrates such as p-nitrophenyl phosphate (pNPP) and P-Tyr inhibited the adhesion of T. rangeli to salivary glands, but P-Ser, P-Thr and beta-glycerophosphate were completely ineffective. Immunoassays using anti-P-Tyr-residues revealed a large number of P-Tyr-proteins in extracts of R. prolixus salivary glands, which could be potentially targeted by T. rangeli during adhesion. These results indicate that dephosphorylation of structural P-Tyr residues on the gland cell surfaces, mediated by a P-Tyr ecto-phosphatase of the parasite, is a key event in the interaction between T. rangeli and R. prolixus salivary glands. (C) 2012 Australian Society for Parasitology Inc. Published by Elsevier Ltd. All rights reserved.

Syntax of social life in postpartum depression: Mother-child interaction

Purpose: Understand the difficulties and experienced of individuals suffering from postpartum depression, related to mood disturbances, the mother-child bond and its repercussions in the meanings established for the experience of being a mother. Methods: Forty-one patients were interviewed, with ages ranging from 20 to 49 years, from a total of 106 attended at the Primary Care Unit, in the interior of the state of Parahiba, Brazil. A sample of 21 women was selected, presenting an inclusion profile, propitious to mapping postpartum depression. The eligible patients were referred by two PSF (Health Family) teams (one each from the urban and rural zones), aimed at diagnosing the psychic disturbance of the perperium. They were accompanied by a psychologist and all signed an informed consent form. A field diary supported the information recorded. Beck's Depression Inventory complemented the inclusion and follow-up of the patients. The data were analyzed statistically. Results: We confirmed the findings of the most recent studies that infant abandonment in the postpartum period occurs in situations where multiple and serious factors add up, such as misery (86.7%), little schooling (67%), lack of a support network (36.5%), estrangement of the mother's family relations (12%) and lack of paternal involvement (91.5%). Conclusion: The feeling of psyching pain and suffering, resulting from postpartum depression, is the most emphasized by women (87%) because it triggers the greatest discomfort, due to the difficulty in overcoming it.

Magmatism and fenitization in the Cretaceous potassium-alkaline-carbonatitic complex of Ipanema So Paulo State, Brazil

The Ipanema alkaline-carbonatitic complex is part of the Meso-Cenozoic alkaline magmatism located within the southeastern part of the Brazilian Platform. Drill-core and field sampling have indicated the occurrence of glimmerites, with subordinate shonkinites (mela-syenites), clinopyroxene-bearing glimmerites, diorites and syenites. The glimmerites are cross-cut by lamprophyric dykes and calciocarbonatites. Fenitization has deeply affected the country rocks, originating dioritic and syenitic rocks. The Ipanema rocks show a distinct potassic affinity. The initial Sr-Nd- isotopic composition of the Ipanema rocks ((87)Sr/(86)Sr = 0.70661-0.70754 and (143)Nd/(144)Nd = 0.51169-0.51181) is similar to that of tholeiitic and potassium-rich-alkaline rocks of the Eastern Paraguay. Stable isotope data for the Ipanema calciocarbonatite suggest interaction with fluids at temperatures typical of hydrothermal stages, as hypothesized for other carbonatite complexes from southeastern Brazil. The chemical differences between the lamprophyre, glimmerites, carbonatites, apatitites and magnetitites, and the absence of marked REE enrichment in the evolved lithologies, all indicate that fractional crystallization and accumulus of liquidus phases in a magma reservoir, likely coupled with liquid immiscibility processes, may have played an important role in the genesis of the Ipanema rocks.

Charge dynamics in half-filled Hubbard chains with finite on-site interaction

We study the charge dynamic structure factor of the one-dimensional Hubbard model with finite on-site repulsion U at half-filling. Numerical results from the time-dependent density matrix renormalization group are analyzed by comparison with the exact spectrum of the model. The evolution of the line shape as a function of U is explained in terms of a relative transfer of spectral weight between the two-holon continuum that dominates in the limit U -> infinity and a subset of the two-holon-two-spinon continuum that reconstructs the electron-hole continuum in the limit U -> 0. Power-law singularities along boundary lines of the spectrum are described by effective impurity models that are explicitly invariant under spin and eta-spin SU(2) rotations. The Mott-Hubbard metal-insulator transition is reflected in a discontinuous change of the exponents of edge singularities at U = 0. The sharp feature observed in the spectrum for momenta near the zone boundary is attributed to a van Hove singularity that persists as a consequence of integrability.

Holographic field theory models of dark energy in interaction with dark matter

We discuss two Lagrangian interacting dark energy models in the context of the holographic principle. The potentials of the interacting fields are constructed. The models are compared with CMB distance information, baryonic acoustic oscillations, lookback time and the Constitution supernovae sample. For both models, the results are consistent with a nonvanishing interaction in the dark sector of the Universe and the sign of coupling is consistent with dark energy decaying into dark matter, alleviating the coincidence problem-with more than 3 standard deviations of confidence for one of them. However, this is because the noninteracting holographic dark energy model is a bad fit to the combination of data sets used in this work as compared to the cosmological constant with cold dark matter model, so that one needs to introduce the interaction in order to improve this model.

Occurrence and sorption of fluoroquinolones in poultry litters and soils from sao Paulo State, Brazil

Animal production is one of the most expressive sectors of Brazilian agro-economy. Although antibiotics are routinely used in this activity, their occurrence, fate, and potential impacts to the local environment are largely unknown. This research evaluated sorption-desorption and occurrence of four commonly used fluoroquinolones (norfloxacin, ciprofloxacin, danofloxacin, and enrofloxacin) in poultry litter and soil samples from Sao Paulo State, Brazil. The sorption-desorption studies involved batch equilibration technique and followed the OECD guideline for pesticides. All compounds were analyzed by HPLC, using fluorescence detector. Fluoroquinolones' sorption potential to the poultry litters (K-d <= 65 L kg(-1)) was lower than to the soil (K-d similar to 40,000 L kg(-1)), but was always high (>= 69% of applied amount) indicating a higher specificity of fluoroquinolones interaction with soils. The addition of poultry litter (5%) to the soil had not affected sorption or desorption of these compounds. Desorption was negligible in the soil (<= 0.5% of sorbed amount), but not in the poultry litters (up to 42% of sorbed amount). Fluoroquinolones' mean concentrations found in the poultry litters (1.37 to 6.68 mg kg(-1)) and soils (22.93 mu g kg(-1)) were compatible to those found elsewhere (Austria, China, and Turkey). Enrofloxacin was the most often detected compound (30% of poultry litters and 27% of soils) at the highest mean concentrations (6.68 mg kg(-1) for poultry litters and 22.93 mu g kg(-1) for soils). These results show that antibiotics are routinely used in poultry production and might represent one potential source of pollution to the environment that has been largely ignored and should be further investigated in Brazil. (C) 2012 Elsevier B.V. All rights reserved.

Assessment of integration of the Leprosy Program into primary health care in Aracaju, State of Sergipe, Brazil

Introduction: The aim of this study was to assess the epidemiological and operational characteristics of the Leprosy Program before and after its integration into the Primary Healthcare Services of the municipality of Aracaju-Sergipe, Brazil. Methods: Data were drawn from the national database. The study periods were divided into preintegration (1996-2000) and postintegration (2001-2007). Annual rates of epidemiological detection were calculated. Frequency data on clinico-epidemiological variables of cases detected and treated for the two periods were compared using the Chi-squared (chi(2)) test adopting a 5% level of significance. Results: Rates of detection overall, and in subjects younger than 15 years, were greater for the postintegration period and were higher than rates recorded for Brazil as a whole during the same periods. A total of 780 and 1,469 cases were registered during the preintegration and postintegration periods, respectively. Observations for the postintegration period were as follows: I) a higher proportion of cases with disability grade assessed at diagnosis, with increase of 60.9% to 78.8% (p < 0.001), and at end of treatment, from 41.4% to 44.4% (p < 0.023); II) an increase in proportion of cases detected by contact examination, from 2.1% to 4.1% (p < 0.001); and III) a lower level of treatment default with a decrease from 5.64 to 3.35 (p < 0.008). Only 34% of cases registered from 2001 to 2007 were examined. Conclusions: The shift observed in rates of detection overall, and in subjects younger than 15 years, during the postintegration period indicate an increased level of health care access. The fall in number of patients abandoning treatment indicates greater adherence to treatment. However, previous shortcomings in key actions, pivotal to attaining the outcomes and impact envisaged for the program, persisted in the postintegration period.

Mixed-valence state of symmetric diruthenium complexes: synthesis, characterization, and electron transfer investigation

Complexes of the type {[(pyS)Ru(NH3)(4)](2)-mu-L}(n), where pyS = 4-mercaptopyridine, L = 4,4'-dithiodipyridine (pySSpy), pyrazine (pz) and 1,4-dicyanobenzene (DCB), and n = +4 and +5 for fully reduced and mixed-valence complexes, respectively, were synthesized and characterized. Electrochemical data showed that there is electron communication between the metal centers with comproportionation constants of 33.2, 1.30 x 10(8) and 5.56 x 10(5) for L = pySSpy, pz and DCB, respectively. It was also observed that the electronic coupling between the metal centers is affected by the p-back-bonding interaction toward the pyS ligand. Raman spectroscopy showed a dependence of the intensity of the vibrational modes on the exciting radiations giving support to the assignments of the electronic transitions. The degree of electron communication between the metal centers through the bridging ligands suggests that these systems can be molecular wire materials.

The Emergence of the Post-Socialist Welfare State - The Case of the Baltic States : Estonia, Latvia and Lithuania

This dissertation takes a step towards providing a better understanding of post-socialist welfare state development from a theoretical as well as an empirical perspective. The overall analytical goal of this thesis has been to critically assess the development of social policies in Estonia, Latvia and Lithuania using them as illustrative examples of post-socialist welfare state development in the light of the theories, approaches and typologies that have been developed to study affluent capitalist democracies. The four studies included in this dissertation aspire to a common aim in a number of specific ways. The first study tries to place the ideal-typical welfare state models of the Baltic States within the well-known welfare state typologies. At the same time, it provides a rich overview of the main social security institutions in the three countries by comparing them with each other and with the previous structures of the Soviet period. It examines the social insurance institutions of the Baltic States (old-age pensions, unemployment insurance, short-term benefits, sickness, maternity and parental insurance and family benefits) with respect to conditions of eligibility, replacement rates, financing and contributions. The findings of this study indicate that the Latvian social security system can generally be labelled as a mix of the basic security and corporatist models. The Estonian social security system can generally also be characterised as a mix of the basic security and corporatist models, even if there are some weak elements of the targeted model in it. It appears that the institutional changes developing in the social security system of Lithuania have led to a combination of the basic security and targeted models of the welfare state. Nevertheless, as the example of the three Baltic States shows, there is diversity in how these countries solve problems within the field of social policy. In studying the social security schemes in detail, some common features were found that could be attributed to all three countries. Therefore, the critical analysis of the main social security institutions of the Baltic States in this study gave strong supporting evidence in favour of identifying the post-socialist regime type that is already gaining acceptance within comparative welfare state research. Study Two compares the system of social maintenance and insurance in the Soviet Union, which was in force in the three Baltic countries before their independence, with the currently existing social security systems. The aim of the essay is to highlight the forces that have influenced the transformation of the social policy from its former highly universal, albeit authoritarian, form, to the less universal, social insurance-based systems of present-day Estonia, Latvia and Lithuania. This study demonstrates that the welfare–economy nexus is not the only important factor in the development of social programs. The results of this analysis revealed that people's attitudes towards distributive justice and the developmental level of civil society also play an important part in shaping social policies. The shift to individualism in people’s mentality and the decline of the labour movement, or, to be more precise, the decline in trade union membership and influence, does nothing to promote the development of social rights in the Baltic countries and hinders the expansion of social policies. The legacy of the past has been another important factor in shaping social programs. It can be concluded that social policy should be studied as if embedded not only in the welfare-economy nexus, but also in the societal, historical and cultural nexus of a given society. Study Three discusses the views of the state elites on family policy within a wider theoretical setting covering family policy and social policy in a broader sense and attempts to expand this analytical framework to include other post-socialist countries. The aim of this essay is to explore the various views of the state elites in the Baltics concerning family policy and, in particular, family benefits as one of the possible explanations for the observed policy differences. The qualitative analyses indicate that the Baltic States differ significantly with regard to the motives behind their family policies. Lithuanian decision-makers seek to reduce poverty among families with children and enhance the parents’ responsibility for bringing up their children. Latvian policy-makers act so as to increase the birth rate and create equal opportunities for children from all families. Estonian policy-makers seek to create equal opportunities for all children and the desire to enhance gender equality is more visible in the case of Estonia in comparison with the other two countries. It is strongly arguable that there is a link between the underlying motives and the kinds of family benefits in a given country. This study, thus, indicates how intimately the attitudes of the state bureaucrats, policy-makers, political elite and researchers shape social policy. It confirms that family policy is a product of the prevailing ideology within a country, while the potential influence of globalisation and Europeanisation is detectable too. The final essay takes into account the opinions of welfare users and examines the performances of the institutionalised family benefits by relying on the recipients’ opinions regarding these benefits. The opinions of the populations as a whole regarding government efforts to help families are compared with those of the welfare users. Various family benefits are evaluated according to the recipients' satisfaction with those benefits as well as the contemporaneous levels of subjective satisfaction with the welfare programs related to the absolute level of expenditure on each program. The findings of this paper indicate that, in Latvia, people experience a lower level of success regarding state-run family insurance institutions, as compared to those in Lithuania and Estonia. This is deemed to be because the cash benefits for families and children in Latvia are, on average, seen as marginally influencing the overall financial situation of the families concerned. In Lithuania and Estonia, the overwhelming majority think that the family benefit systems improve the financial situation of families. It appears that recipients evaluated universal family benefits as less positive than targeted benefits. Some universal benefits negatively influenced the level of general satisfaction with the family benefits system provided in the countries being researched. This study puts forward a discussion about whether universalism is always more legitimate than targeting. In transitional economies, in which resources are highly constrained, some forms of universal benefits could turn out to be very expensive in relative terms, without being seen as useful or legitimate forms of help to families. In sum, by closely examining the different aspects of social policy, this dissertation goes beyond the over-generalisation of Eastern European welfare state development and, instead, takes a more detailed look at what is really going on in these countries through the examples of Lithuania, Latvia and Estonia. In addition, another important contribution made by this study is that it revives ‘western’ theoretical knowledge through ‘eastern’ empirical evidence and provides the opportunity to expand the theoretical framework for post-socialist societies.

New materials for electrochemiluminescence

The study of electrochemiluminescence (ECL) involves photophysical and electrochemical aspects. Excited states are populated by an electrical stimulus. The most important applications are in the diagnostic field where a number of different biologically-relevant molecules (e.g. proteins and nucleic acids) can be recognized and quantified with a sensitivity and specificity previously not reachable. As a matter of fact the electrochemistry, differently to the classic techniques as fluorescence and chemiluminescence, allows to control the excited state generation spatially and temporally. The two research visits into A. J. Bard electrochemistry laboratories were priceless. Dr. Bard has been one of ECL pioneers, the first to introduce the technique and the one who discovered in 1972 the surprising emission of Ru(bpy)3 2+. I consider necessary to thank by now my supervisors Massimo and Francesco for their help and for giving me the great opportunity to know this unique science man that made me feel enthusiastic. I will never be grateful enough… Considering that the experimental techniques of ECL did not changed significantly in these last years the most convenient research direction has been the developing of materials with new or improved properties. In Chapter I the basics concepts and mechanisms of ECL are introduced so that the successive experiments can be easily understood. In the final paragraph the scopes of the thesis are briefly described. In Chapter II by starting from ECL experimental apparatus of Dr. Bard’s laboratories the design, assembly and preliminary tests of the new Bologna instrument are carefully described. The instrument assembly required to work hard but resulted in the introduction of the new technique in our labs by allowing the continuation of the ECL studies began in Texas. In Chapter III are described the results of electrochemical and ECL studies performed on new synthesized Ru(II) complexes containing tetrazolate based ligands. ECL emission has been investigated in solution and in solid thin films. The effect of the chemical protonation of the tetrazolate ring on ECL emission has been also investigated evidencing the possibility of a catalytic effect (generation of molecular hydrogen) of one of the complexes in organic media. Finally, after a series of preliminary studies on ECL emission in acqueous buffers, the direct interaction with calf thymus DNA of some complexes has been tested by ECL and photoluminescence (PL) titration. In Chapter IV different Ir(III) complexes have been characterized electrochemically and photophysically (ECL and PL). Some complexes were already well-known in literature for their high quantum efficiency whereas the remaining were new synthesized compounds containing tetrazolate based ligands analogous to those investigated in Chapt. III. During the tests on a halogenated complex was unexpectedly evidenced the possibility to follow the kinetics of an electro-induced chemical reaction by using ECL signal. In the last chapter (V) the possibility to use mono-use silicon chips electrodes as ECL analitycal devices is under investigation. The chapter begins by describing the chip structure and materials then a signal reproducibility study and geometry optimization is carried on by using two different complexes. In the following paragraphs is reported in detail the synthesis of an ECL label based on Ru(bpy)3 2+ and the chip functionalization by using a lipoic acid SAM and the same label. After some preliminary characterizations (mass spectroscopy TOF) has been demonstrated that by mean of a simple and fast ECL measurement it’s possible to confirm the presence of the coupling product SAM-label into the chip with a very high sensitivity. No signal was detected from the same system by using photoluminescence.

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.