Nanogravimetric study of lead underpotential deposition on selenium thin films as a semiconductor alloy formation procedure

An electrochemical quartz crystal microbalance Au electrode modified with a Se thin film was used to investigate the electrochemical behavior of lead ad-atoms using underpotential deposition (UPD) conditions. A specific quasi-reversible process was observed during the reduction of Pb2+ on Se thin films in perchloric acid media. The charge density of Pb ad-atoms on Se thin film (46.86 mu C cm(-2)) suggests a recovery of 0.1 monolayers, which is in good agreement with EQCM data. The Se thin film can be successfully alloyed with Pb atoms that are deposited by chronoamperometry using time intervals large enough to allow for diffusion toward the inner Se phase. Linear sweep voltammetry combined with EQCM in perchloric acid was used to characterize the amount of Pb absorbed in the Se thin film. These findings offer a new strategy for alloy formation in semiconductor films using UPD as an effective tool to quantify the exact amount of the incorporated metal.

Different lead sources in an abandoned uranium mine (Urgeirica - Central Portugal) and its environment impact - isotopic evidence

Different lead sources were identified in a large uranium tailings deposit (5Mton) in the Central Region of Portugal using lead isotopic ratios obtained by ICP-QMS. These ratios helped to clarify the different sources of Pb within the tailings deposit and the impact of the tailings on the surroundings. Ten depth profiles were used for isotopic characterization of the tailings deposit; the lead background signature was evaluated in seven regional rocks (granites) and was defined as being 28 +/- 1 mg kg(-1) for Pb bulk concentration and with isotopic ratios of 1.264(2) for Pb-206/Pb-207 and 1.962(7) for Pb-208/Pb-206. In order to understand Pb isotope distribution within the tailings deposit, simple mixing/mass balance models were used to fit experimental data, involving: (1) the background component; (2) uranium ores (pitchblende) characterized by the ratios Pb-206/Pb-207 of 1.914(3) and Pb-208/Pb-206 of 1.235(2); and (3) an unknown Pb source (named 'Fonte 5') characterized by the ratios Pb-206/Pb-207 of 3.079(7) and Pb-208/Pb-206 of 0.715(1). This unknown source showed high radiogenic ratios found in the water of some tailings depth profiles located in a very specific position in the dump. In terms of isotopic characterization, 69% of the deposit material resulted from the background source, 25% from uranium minerals and only 6% from other uranium mines in the region. Finally, the environment impact revealed that the pollution was focused only in the beginning of the stream and not in the surroundings, nor in the groundwater system. The lead in the water was found only in colloidal form with a clear pitchblende signature. Those data revealed possible remobilization phenomena along the bedside and margins of the watercourse.

An EQCM-D study of the influence of chloride on the lead anodic oxidation

The influence of chloride on the electrodeposition of lead films and their dissolution in anodic stripping voltammetric experiments was examined. Gold substrates were plated with lead films, and mass changes were monitored by using the electrochemical quartz crystal microbalance with dissipation factor (EQCM-D). The results showed that the amount of electrodeposited lead is slightly dependent on the chloride concentration. The charge/mass ratio data indicated the presence of Pb(I) and Pb(II) as a result of film dissolution, and the precipitation and deposition of PbCl2 onto the electrode surface. Scanning electron microscopy images revealed that the morphology of the lead film was strongly influenced by chloride present in the plating solution and that much rougher films were obtained in comparison with those obtained in the absence of chloride. The rate of the anodic dissolution was higher for lead films with higher surface areas, which lead to an increase in their stripping voltammetric currents. (C) 2012 Elsevier Ltd. All rights reserved.

Linking origin of the electric field-assisted beta-PbF2 crystallization in lead oxyfluoroborate glasses below T (g) to simultaneous cathode/anode-compensated electrochemical reactions

Full validation of the electrochemical mechanisms so far postulated as driving force of electric field-assisted non-spontaneous crystallization development in given glasses has suffered experimental restrictions. In this work, we looked into origin of this phenomenon in lead oxyfluoroborate glasses, resulting in beta-PbF2 growth even below the corresponding glass transition temperatures, through achieving a systematic study of not only Pt,Ag/Glass/Ag,Pt- but also Pt,Ag/Glass/YSZ:PbF2/Ag,Pt-type cells, where YSZ:PbF2 represents a two-phase system (formed by Y2O3-doped ZrO2 and PbF2). It is demonstrated that crystallization induction in these glasses involves Pb2+ ions reduction at the cathode, the phenomenon being, however, confirmed only when the F- ions were simultaneously also able to reach the anode for oxidation, after assuring either a direct glass-anode contact or percolation pathways for free fluoride migration across the YSZ:PbF2 mixtures. A further support of this account is that the electrochemically induced beta-PbF2 phase crystallizes showing ramified-like microstructure morphology that arises, accordingly, from development of electroconvective diffusion processes under electric field action.

GEDI: a user-friendly toolbox for analysis of large-scale gene expression data

Abstract Background Several mathematical and statistical methods have been proposed in the last few years to analyze microarray data. Most of those methods involve complicated formulas, and software implementations that require advanced computer programming skills. Researchers from other areas may experience difficulties when they attempting to use those methods in their research. Here we present an user-friendly toolbox which allows large-scale gene expression analysis to be carried out by biomedical researchers with limited programming skills. Results Here, we introduce an user-friendly toolbox called GEDI (Gene Expression Data Interpreter), an extensible, open-source, and freely-available tool that we believe will be useful to a wide range of laboratories, and to researchers with no background in Mathematics and Computer Science, allowing them to analyze their own data by applying both classical and advanced approaches developed and recently published by Fujita et al. Conclusion GEDI is an integrated user-friendly viewer that combines the state of the art SVR, DVAR and SVAR algorithms, previously developed by us. It facilitates the application of SVR, DVAR and SVAR, further than the mathematical formulas present in the corresponding publications, and allows one to better understand the results by means of available visualizations. Both running the statistical methods and visualizing the results are carried out within the graphical user interface, rendering these algorithms accessible to the broad community of researchers in Molecular Biology.

Correlation analysis of the long latency auditory evoked potential N2 and cognitive P3 with the level of lead poisoning in children

Introduction: The effects of lead on children’s health have been widely studied. Aim: To analyze the correlation between the long latency auditory evoked potential N2 and cognitive P3 with the level of lead poisoning in Brazilian children. Methods: This retrospective study evaluated 20 children ranging in age from 7 to 14 years at the time of audiological and electrophysiological evaluations. We performed periodic surveys of the lead concentration in the blood and basic audiological evaluations. Furthermore, we studied the auditory evoked potential long latency N2 and cognitive P3 by analyzing the absolute latency of the N2 and P3 potentials and the P3 amplitude recorded at Cz. At the time of audiological and electrophysiological evaluations, the average concentration of lead in the blood was less than 10 ug/dL. Results: In conventional audiologic evaluations, all children had hearing thresholds below 20 dBHL for the frequencies tested and normal tympanometry findings; the auditory evoked potential long latency N2 and cognitive P3 were present in 95% of children. No significant correlations were found between the blood lead concentration and latency (p = 0.821) or amplitude (p = 0.411) of the P3 potential. However, the latency of the N2 potential increased with the concentration of lead in the blood, with a significant correlation (p = 0.030). Conclusion: Among Brazilian children with low lead exposure, a significant correlation was found between blood lead levels and the average latency of the auditory evoked potential long latency N2; however, a significant correlation was not observed for the amplitude and latency of the cognitive potential P3

Accessibility and demand at an Emergency Care Unit: the user's perspective

AIM: To analyze the search for Emergency Care (EC) in the Western Health District of Ribeirão Preto (São Paulo), in order to identify the reasons why users turn to these services in situations that are not characterized as urgencies and emergencies. METHODS: A qualitative and descriptive study was undertaken. A guiding script was applied to 23 EC users, addressing questions related to health service accessibility and welcoming, problem solving, reason to visit the EC and care comprehensiveness. RESULTS: The subjects reported that, at the Primary Health Care services, receiving care and scheduling consultations took a long time and that the opening hours of these services coincide with their work hours. At the EC service, access to technologies and medicines was easier. CONCLUSION: Primary health care services have been unable to turn into the entry door to the health system, being replaced by emergency services, putting a significant strain on these services' capacity.

An alternative method for the simultaneous determination of copper and lead for quality control of sugar cane spirit using a nanotube-based sensor

The development of an electroanalytical method for simultaneous determination of copper and lead ions in sugar cane spirit (cachaça) using carbon paste electrode modified with ascorbic acid and carbon nanotubes (CPE-AaCNT) is described. Squarewave voltammetry (SWV) with anodic stripping was employed, and this technique was optimized with respect to the following parameters: frequency (50 Hz), amplitude (100 mV) and scan increment (9 mV). The analytical curves were linear in the range from 0.0900 to 7.00 mg L- 1 for lead and copper. The limits of detection were 48.5 and 23.9 µg L- 1 for lead and copper, respectively. The developed method was applied to the simultaneous determination of copper and lead in five commercial samples of sugar cane spirit. The results were in good agreement with those obtained by F AAS/GF AAS (flame atomic absorption spectrometry/graphite furnace atomic absorption spectrometry) and showed that CPE-AaCNT can be successfully employed in the simultaneous determination of these metals in real sugar cane spirit samples.

PRoSPer: perceptual similarity queries in medical CBIR systems through user profiles

In this paper, we present a novel approach to perform similarity queries over medical images, maintaining the semantics of a given query posted by the user. Content-based image retrieval systems relying on relevance feedback techniques usually request the users to label relevant/irrelevant images. Thus, we present a highly effective strategy to survey user profiles, taking advantage of such labeling to implicitly gather the user perceptual similarity. The profiles maintain the settings desired for each user, allowing tuning of the similarity assessment, which encompasses the dynamic change of the distance function employed through an interactive process. Experiments on medical images show that the method is effective and can improve the decision making process during analysis.

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.

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.