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.

Sulla progettazione in zona sismica di strutture dotate di dissipatori fluido-viscosi: proposta di una metodologia

CHAPTER 1:FLUID-VISCOUS DAMPERS In this chapter the fluid-viscous dampers are introduced. The first section is focused on the technical characteristics of these devices, their mechanical behavior and the latest evolution of the technology whose they are equipped. In the second section we report the definitions and the guide lines about the design of these devices included in some international codes. In the third section the results of some experimental tests carried out by some authors on the response of these devices to external forces are discussed. On this purpose we report some technical schedules that are usually enclosed to the devices now available on the international market. In the third section we show also some analytic models proposed by various authors, which are able to describe efficiently the physical behavior of the fluid-viscous dampers. In the last section we propose some cases of application of these devices on existing structures and on new-construction structures. We show also some cases in which these devices have been revealed good for aims that lies outside the reduction of seismic actions on the structures. CHAPTER 2:DESIGN METHODS PROPOSED IN LITERATURE In this chapter the more widespread design methods proposed in literature for structures equipped by fluid-viscous dampers are introduced. In the first part the response of sdf systems in the case of harmonic external force is studied, in the last part the response in the case of random external force is discussed. In the first section the equations of motion in the case of an elastic-linear sdf system equipped with a non-linear fluid-viscous damper undergoing a harmonic force are introduced. This differential problem is analytically quite complex and it’s not possible to be solved in a closed form. Therefore some authors have proposed approximate solution methods. The more widespread methods are based on equivalence principles between a non-linear device and an equivalent linear one. Operating in this way it is possible to define an equivalent damping ratio and the problem becomes linear; the solution of the equivalent problem is well-known. In the following section two techniques of linearization, proposed by some authors in literature, are described: the first technique is based on the equivalence of the energy dissipated by the two devices and the second one is based on the equivalence of power consumption. After that we compare these two techniques by studying the response of a sdf system undergoing a harmonic force. By introducing the equivalent damping ratio we can write the equation of motion of the non-linear differential problem in an implicit form, by dividing, as usual, for the mass of the system. In this way, we get a reduction of the number of variables, by introducing the natural frequency of the system. The equation of motion written in this form has two important properties: the response is linear dependent on the amplitude of the external force and the response is dependent on the ratio of the frequency of the external harmonic force and the natural frequency of the system only, and not on their single values. All these considerations, in the last section, are extended to the case of a random external force. CHAPTER 3: DESIGN METHOD PROPOSED In this chapter the theoretical basis of the design method proposed are introduced. The need to propose a new design method for structures equipped with fluid-viscous dampers arises from the observation that the methods reported in literature are always iterative, because the response affects some parameters included in the equation of motion (such as the equivalent damping ratio). In the first section the dimensionless parameterε is introduced. This parameter has been obtained from the definition of equivalent damping ratio. The implicit form of the equation of motion is written by introducing the parameter ε, instead of the equivalent damping ratio. This new implicit equation of motions has not any terms affected by the response, so that once ε is known the response can be evaluated directly. In the second section it is discussed how the parameter ε affects some characteristics of the response: drift, velocity and base shear. All the results described till this point have been obtained by keeping the non-linearity of the behavior of the dampers. In order to get a linear formulation of the problem, that is possible to solve by using the well-known methods of the dynamics of structures, as we did before for the iterative methods by introducing the equivalent damping ratio, it is shown how the equivalent damping ratio can be evaluated from knowing the value of ε. Operating in this way, once the parameter ε is known, it is quite easy to estimate the equivalent damping ratio and to proceed with a classic linear analysis. In the last section it is shown how the parameter ε could be taken as reference for the evaluation of the convenience of using non-linear dampers instead of linear ones on the basis of the type of external force and the characteristics of the system. CHAPTER 4: MULTI-DEGREE OF FREEDOM SYSTEMS In this chapter the design methods of a elastic-linear mdf system equipped with non-linear fluidviscous dampers are introduced. It has already been shown that, in the sdf systems, the response of the structure can be evaluated through the estimation of the equivalent damping ratio (ξsd) assuming the behavior of the structure elastic-linear. We would to mention that some adjusting coefficients, to be applied to the equivalent damping ratio in order to consider the actual behavior of the structure (that is non-linear), have already been proposed in literature; such coefficients are usually expressed in terms of ductility, but their treatment is over the aims of this thesis and we does not go into further. The method usually proposed in literature is based on energy equivalence: even though this procedure has solid theoretical basis, it must necessary include some iterative process, because the expression of the equivalent damping ratio contains a term of the response. This procedure has been introduced primarily by Ramirez, Constantinou et al. in 2000. This procedure is reported in the first section and it is defined “Iterative Method”. Following the guide lines about sdf systems reported in the previous chapters, it is introduced a procedure for the assessment of the parameter ε in the case of mdf systems. Operating in this way the evaluation of the equivalent damping ratio (ξsd) can be done directly without implementing iterative processes. This procedure is defined “Direct Method” and it is reported in the second section. In the third section the two methods are analyzed by studying 4 cases of two moment-resisting steel frames undergoing real accelerogramms: the response of the system calculated by using the two methods is compared with the numerical response obtained from the software called SAP2000-NL, CSI product. In the last section a procedure to create spectra of the equivalent damping ratio, affected by the parameter ε and the natural period of the system for a fixed value of exponent α, starting from the elasticresponse spectra provided by any international code, is introduced.

The rupture process of recent tsunamigenic earthquakes by geophysical data inversion

Subduction zones are the favorite places to generate tsunamigenic earthquakes, where friction between oceanic and continental plates causes the occurrence of a strong seismicity. The topics and the methodologies discussed in this thesis are focussed to the understanding of the rupture process of the seismic sources of great earthquakes that generate tsunamis. The tsunamigenesis is controlled by several kinematical characteristic of the parent earthquake, as the focal mechanism, the depth of the rupture, the slip distribution along the fault area and by the mechanical properties of the source zone. Each of these factors plays a fundamental role in the tsunami generation. Therefore, inferring the source parameters of tsunamigenic earthquakes is crucial to understand the generation of the consequent tsunami and so to mitigate the risk along the coasts. The typical way to proceed when we want to gather information regarding the source process is to have recourse to the inversion of geophysical data that are available. Tsunami data, moreover, are useful to constrain the portion of the fault area that extends offshore, generally close to the trench that, on the contrary, other kinds of data are not able to constrain. In this thesis I have discussed the rupture process of some recent tsunamigenic events, as inferred by means of an inverse method. I have presented the 2003 Tokachi-Oki (Japan) earthquake (Mw 8.1). In this study the slip distribution on the fault has been inferred by inverting tsunami waveform, GPS, and bottom-pressure data. The joint inversion of tsunami and geodetic data has revealed a much better constrain for the slip distribution on the fault rather than the separate inversions of single datasets. Then we have studied the earthquake occurred on 2007 in southern Sumatra (Mw 8.4). By inverting several tsunami waveforms, both in the near and in the far field, we have determined the slip distribution and the mean rupture velocity along the causative fault. Since the largest patch of slip was concentrated on the deepest part of the fault, this is the likely reason for the small tsunami waves that followed the earthquake, pointing out how much the depth of the rupture plays a crucial role in controlling the tsunamigenesis. Finally, we have presented a new rupture model for the great 2004 Sumatra earthquake (Mw 9.2). We have performed the joint inversion of tsunami waveform, GPS and satellite altimetry data, to infer the slip distribution, the slip direction, and the rupture velocity on the fault. Furthermore, in this work we have presented a novel method to estimate, in a self-consistent way, the average rigidity of the source zone. The estimation of the source zone rigidity is important since it may play a significant role in the tsunami generation and, particularly for slow earthquakes, a low rigidity value is sometimes necessary to explain how a relatively low seismic moment earthquake may generate significant tsunamis; this latter point may be relevant for explaining the mechanics of the tsunami earthquakes, one of the open issues in present day seismology. The investigation of these tsunamigenic earthquakes has underlined the importance to use a joint inversion of different geophysical data to determine the rupture characteristics. The results shown here have important implications for the implementation of new tsunami warning systems – particularly in the near-field – the improvement of the current ones, and furthermore for the planning of the inundation maps for tsunami-hazard assessment along the coastal area.

Assembly and characterization of supramolecular architectures for biosensor applications

The research has included the efforts in designing, assembling and structurally and functionally characterizing supramolecular biofunctional architectures for optical biosensing applications. In the first part of the study, a class of interfaces based on the biotin-NeutrAvidin binding matrix for the quantitative control of enzyme surface coverage and activity was developed. Genetically modified ß-lactamase was chosen as a model enzyme and attached to five different types of NeutrAvidin-functionalized chip surfaces through a biotinylated spacer. All matrices are suitable for achieving a controlled enzyme surface density. Data obtained by SPR are in excellent agreement with those derived from optical waveguide measurements. Among the various protein-binding strategies investigated in this study, it was found that stiffness and order between alkanethiol-based SAMs and PEGylated surfaces are very important. Matrix D based on a Nb2O5 coating showed a satisfactory regeneration possibility. The surface-immobilized enzymes were found to be stable and sufficiently active enough for a catalytic activity assay. Many factors, such as the steric crowding effect of surface-attached enzymes, the electrostatic interaction between the negatively charged substrate (Nitrocefin) and the polycationic PLL-g-PEG/PEG-Biotin polymer, mass transport effect, and enzyme orientation, are shown to influence the kinetic parameters of catalytic analysis. Furthermore, a home-built Surface Plasmon Resonance Spectrometer of SPR and a commercial miniature Fiber Optic Absorbance Spectrometer (FOAS), served as a combination set-up for affinity and catalytic biosensor, respectively. The parallel measurements offer the opportunity of on-line activity detection of surface attached enzymes. The immobilized enzyme does not have to be in contact with the catalytic biosensor. The SPR chip can easily be cleaned and used for recycling. Additionally, with regard to the application of FOAS, the integrated SPR technique allows for the quantitative control of the surface density of the enzyme, which is highly relevant for the enzymatic activity. Finally, the miniaturized portable FOAS devices can easily be combined as an add-on device with many other in situ interfacial detection techniques, such as optical waveguide lightmode spectroscopy (OWLS), the quartz crystal microbalance (QCM) measurements, or impedance spectroscopy (IS). Surface plasmon field-enhanced fluorescence spectroscopy (SPFS) allows for an absolute determination of intrinsic rate constants describing the true parameters that control interfacial hybridization. Thus it also allows for a study of the difference of the surface coupling influences between OMCVD gold particles and planar metal films presented in the second part. The multilayer growth process was found to proceed similarly to the way it occurs on planar metal substrates. In contrast to planar bulk metal surfaces, metal colloids exhibit a narrow UV-vis absorption band. This absorption band is observed if the incident photon frequency is resonant with the collective oscillation of the conduction electrons and is known as the localized surface plasmon resonance (LSPR). LSPR excitation results in extremely large molar extinction coefficients, which are due to a combination of both absorption and scattering. When considering metal-enhanced fluorescence we expect the absorption to cause quenching and the scattering to cause enhancement. Our further study will focus on the developing of a detection platform with larger gold particles, which will display a dominant scattering component and enhance the fluorescence signal. Furthermore, the results of sequence-specific detection of DNA hybridization based on OMCVD gold particles provide an excellent application potential for this kind of cheap, simple, and mild preparation protocol applied in this gold fabrication method. In the final chapter, SPFS was used for the in-depth characterizations of the conformational changes of commercial carboxymethyl dextran (CMD) substrate induced by pH and ionic strength variations were studied using surface plasmon resonance spectroscopy. The pH response of CMD is due to the changes in the electrostatics of the system between its protonated and deprotonated forms, while the ionic strength response is attributed from the charge screening effect of the cations that shield the charge of the carboxyl groups and prevent an efficient electrostatic repulsion. Additional studies were performed using SPFS with the aim of fluorophore labeling the carboxymethyl groups. CMD matrices showed typical pH and ionic strength responses, such as high pH and low ionic strength swelling. Furthermore, the effects of the surface charge and the crosslink density of the CMD matrix on the extent of stimuli responses were investigated. The swelling/collapse ratio decreased with decreasing surface concentration of the carboxyl groups and increasing crosslink density. The study of the CMD responses to external and internal variables will provide valuable background information for practical applications.

Bewertungsportale im Internet – Meinungsfreiheit versus Datenschutz und Haftungsfragen der Portalbetreiber

Die vorliegende Arbeit beschäftigt sich mit rechtlichen Fragestellungen rund um Bewertungs-portale im Internet. Zentrale Themen der Arbeit sind dabei die Zulässigkeit der Veröffentlichung der von den Nutzern abgegebenen Bewertungen vor dem Hintergrund möglicherweise entgegenstehender datenschutzrechtlicher Bestimmungen und der Persönlichkeitsrechte der Betroffenen. Des weiteren wird der Rechtsschutz der Betroffenen erörtert und in diesem Zusammenhang die haftungsrechtlichen Risiken der Forenbetreiber untersucht. Gegenstand der Arbeit sind dabei sowohl Online-Marktplätze wie eBay, auf denen sowohl der Bewertende als auch der Bewertete registriert und mit dem Bewertungsverfahren grundsätz-lich einverstanden sind (geschlossene Portale), als auch Portale, auf denen – oftmals unter einem Pseudonym und ohne vorherige Anmeldung – eine freie Bewertungsabgabe, zu Pro-dukteigenschaften, Dienstleistungen bis hinzu Persönlichkeitsmerkmalen des Bewerteten möglich ist (offene Portale). Einleitung und Erster Teil Nach einer Einleitung und Einführung in die Problematik werden im ersten Teil die verschie-denen Arten der Bewertungsportale kurz vorgestellt. Die Arbeit unterscheidet dabei zwischen so genannten geschlossenen Portalen (transaktionsbegleitende Portale wie eBay oder Ama-zon) auf der einen Seite und offenen Portalen (Produktbewertungsportale, Hotelbewertungs-portale und Dienstleistungsbewertungsportale) auf der anderen Seite. Zweiter Teil Im zweiten Teil geht die Arbeit der Frage nach, ob die Veröffentlichung der durch die Nutzer abgegebenen Bewertungen auf den offenen Portalen überhaupt erlaubt ist oder ob hier mögli-cherweise das Persönlichkeitsrecht der Betroffenen und hier insbesondere das Recht auf in-formationelle Selbstbestimmung in Form der datenschutzrechtlichen Bestimmungen die freie Bewertungsabgabe unzulässig werden lässt. Untersucht werden in diesem Zusammenhang im einzelnen Löschungs- bzw. Beseitigungsan-sprüche der Betroffenen aus § 35 Abs. 2 Satz 2 Nr. 1 BDSG bzw. §§ 1004 i. V. m. 823 Abs. 1 BGB (allgemeines Persönlichkeitsrecht). Die Arbeit kommt in datenschutzrechtlicher Hinsicht zu dem Schluss, dass die Bewertungen personenbezogene Daten darstellen, die den datenschutzrechtlichen Bestimmungen unterlie-gen und eine Veröffentlichung der Bewertungen nach dem im deutschen Recht geltenden da-tenschutzrechtlichen Erlaubnisvorbehalt grundsätzlich nicht in Betracht kommt. Vor dem Hintergrund dieser den tatsächlichen Gegebenheiten und Interessenlagen im Internet nicht mehr gerecht werdenden Gesetzeslage diskutiert der Autor sodann die Frage, ob die datenschutzrechtlichen Bestimmungen in diesen Fällen eine Einschränkung durch die grund-gesetzlich garantierten Informationsfreiheiten erfahren müssen. Nach einer ausführlichen Diskussion der Rechtslage, in der auf die Besonderheiten der ein-zelnen Portale eingegangen wird, kommt die Arbeit zu dem Schluss, dass die Frage der Zuläs-sigkeit der Veröffentlichung der Bewertungen von einer Interessenabwägung im Einzelfall abhängt. Als Grundsatz kann jedoch gelten: Ist die bewertete Tätigkeit oder Person in Bezug auf die bewertete Eigenschaft ohnehin einer breiten Öffentlichkeit zugänglich, erscheint eine Veröffentlichung der Daten nicht bedenklich. Dagegen wird man einen Löschungs- bzw. Be-seitigungsanspruch bejahen müssen für die Bewertungen, die Tätigkeiten oder Eigenschaften des Bewerteten, die in keinem Zusammenhang mit ihm als öffentlicher Person stehen, betref-fen. Anschließend geht die Arbeit auf die Persönlichkeitsrechte der Betroffenen und der sich hier-aus ergebenden Beseitigungs- und Unterlassungsansprüchen gemäß der §§ 1004 Abs. 1, 823 Abs. 1 BGB ein, verneint jedoch wegen dem Vorrang der spezialgesetzlichen Bestimmungen aus dem Bundesdatenschutzgesetz letztlich eine Anwendbarkeit der Anspruchsgrundlagen. Schließlich wird in diesem Teil noch kurz auf die Zulässigkeit der Bewertung juristischer Per-sonen eingegangen, die im Grundsatz bejaht wird. Dritter Teil Sofern der zweite Teil der Arbeit zu dem Schluss kommt, dass die Veröffentlichung der Be-wertungen zulässig ist, stellt sich im dritten Teil die Frage, welche Möglichkeiten das Recht dem Bewerteten bietet, gegen negative Bewertungen vorzugehen. Untersucht werden, dabei datenschutzrechtliche, deliktsrechtliche, vertragliche und wettbe-werbsrechtliche Ansprüche. Ein Schwerpunkt dieses Teils liegt in der Darstellung der aktuellen Rechtsprechung zu der Frage wann eine Bewertung eine Tatsachenbehauptung bzw. ein Werturteil darstellt und den sich hieraus ergebenden unterschiedlichen Konsequenzen für den Unterlassungsanspruch des Betroffenen. Diejenigen Bewertungen, die eine Meinungsäußerung darstellen, unterstehen dem starken Schutz der Meinungsäußerungsfreiheit. Grenze der Zulässigkeit sind hier im wesentlichen nur die Schmähkritik und Beleidigung. An Tatsachenbehautpungen dagegen sind schärfere Maßstäbe anzulegen. In diesem Zusammenhang wird der Frage nachgegangen, ob vertragliche Beziehungen zwischen den Beteiligten (Bewertenden, Bewertete und Portalbetreiber) die Meinungsäußerungsfreiheit einschränkt, was jedenfalls für die geschlossenen Portale bejaht wird. Vierter Teil Der vierte Teil der Arbeit beschäftigt sich mit den „Zu-gut-Bewertungen“. Es geht dabei um wettbewerbsrechtliche Ansprüche im Falle verdeckter Eigenbewertungen. Solche Eigenbewertungen, die unter dem Deckmantel der Pseudonymität als Werbemittel zur Imageverbesserung in entsprechenden Bewertungsportale verbreitet werden ohne den wahren Autor erkennen zu lassen, sind in wettbewerbsrechtlicher Hinsicht grundsätzlich unzulässig. Fünfter Teil Im letzten Teil der Arbeit wird schließlich der Frage nach der Verantwortlichkeit der Portal-betreiber für rechtswidrige Bewertungen nachgegangen. Zunächst wird die Feststellung getroffen, dass es sich bei den von den Nutzern abgegebenen Bewertungen um fremde Inhalte handelt und somit die Haftungsprivilegierungen der § 11 Abs. 1 TDG, § 9 Abs. 1 MDStV eingreifen, wonach die Forenbetreiber für die rechtswidrigen Bewertungen jedenfalls so lange nicht verantwortlich sind, solange sie hiervon keine Kenntnis haben. Da von dieser Haftungsprivilegierung nach der Rechtsprechung des Bundesgerichtshofs die Störerhaftung nicht umfasst ist, wird die Reichweite die Forenbetreiber aus der Störerhaftung treffenden Überwachungspflichten diskutiert. Die Arbeit kommt hier zu dem Ergebnis, dass in den Fällen, in denen dem Adressaten der Bewertung die Identität des Verfassers bekannt ist, sich die Verpflichtungen der Forenbetrei-ber auf die Beseitigung bzw. Sperrung der rechtswidrigen Bewertung beschränken. Sofern die Identität des Bewertenden unbekannt ist, haften die Forenbetreiber als Mitstörer und dem Be-troffenen stehen Unterlassungsansprüche auch gegen die Forenbetreiber zu.

Stock boundaries of Parapenaeus longirostris (Lucas, 1846) populations in the Italian seas: Development of genomic 2b-RAD markers and biological variation analysis.

This thesis is developed in the contest of Ritmare project WP1, which main objective is the development of a sustainable fishery through the identification of populations boundaries in commercially important species in Italian Seas. Three main objectives are discussed in order to help reach the main purpose of identification of stock boundaries in Parapenaeus longirostris: 1 -Development of a representative sampling design for Italian seas; 2 -Evaluation of 2b-RAD protocol; 3 -Investigation of populations through biological data analysis. First of all we defined and accomplished a sampling design which properly represents all Italian seas. Then we used information and data about nursery areas distribution, abundance of populations and importance of P. longirostris in local fishery, to develop an experimental design that prioritize the most important areas to maximize the results with actual project funds. We introduced for the first time the use of 2b-RAD on this species, a genotyping method based on sequencing the uniform fragments produced by type IIB restriction endonucleases. Thanks to this method we were able to move from genetics to the more complex genomics. In order to proceed with 2b-RAD we performed several tests to identify the best DNA extraction kit and protocol and finally we were able to extract 192 high quality DNA extracts ready to be processed. We tested 2b-RAD with five samples and after high-throughput sequencing of libraries we used the software “Stacks” to analyze the sequences. We obtained positive results identifying a great number of SNP markers among the five samples. To guarantee a multidisciplinary approach we used the biological data associated to the collected samples to investigate differences between geographical samples. Such approach assures continuity with other project, for instance STOCKMED, which utilize a combination of molecular and biological analysis as well.

Atmospheric heterogeneous reactions of N 2 O 5 and NO 3 radicals with mineral dust particles

Die heterogenen Reaktionen von N2O5 bzw. NO3 auf mineralischen Staubpartikeln wurden untersucht, um deren Einfluss auf den Abbau atmosphärischer Stickoxide (NOx) sowie auf die chemische Veränderung der Staubpartikel während ihres Transportes durch die Atmosphäre besser verstehen zu können. Die experimentellen Studien wurden bei Atmosphärendruck, Raumtemperatur und unterschiedlichen relativen Luftfeuchten durchgeführt. Der Aufnahmekoeffizient γ(N2O5) von N2O5 auf dispergiertem Staub aus der Sahara wurde zu 0,020 ± 0,002 (1σ) bestimmt, unabhängig von der relativen Feuchte (0 - 67 %) sowie der N2O5-Konzentration (5x1011 - 3x1013 Moleküle cm-3).rnDie Analyse der Reaktionsprodukte in der Gasphase sowie auf der Partikeloberfläche führt zu der Annahme, dass N2O5 auf der Staubpartikeloberfläche zu Nitrat hydrolysiert wird. Es konnte kein Einfluss der relativen Feuchte auf den Aufnahmekoeffizienten ermittelt werden, was durch das vorhandene interlamellare Wasser, welches bis zu 10 % der Partikelmasse betragen kann, erklärbar ist. Der gemessene Wert des Aufnahmekoeffizienten ist unabhängig von der Eingangs-N2O5-Konzentration, was sich über die sehr große innere Oberfläche der Partikel erklären lässt. Dennoch ließ sich durch eine vorherige Konditionierung der Partikel mit gasförmigem HNO3, was eine Nitratanreicherung an der Oberfläche bewirkt, die Effizienz der N2O5-Aufnahme auf die Staubpartikel reduzieren. Zusätzliche Studien befassten sich mit der Bestimmung des Aufnahmekoeffizienten von N2O5 auf Illit-Partikeln und auf Teststaub aus Arizona. Bei einer relativen Luftfeuchte von 0 % wurden für γ(N2O5) Werte von 0,084 ± 0,019 (1σ) für Illit und von 0,010 ± 0,001 (1σ) für Arizona Teststaub ermittelt.rnUnter Anwendung einer neuartigen Messmethode, die auf der zeitgleichen Messung der Konzentrationsabnahme von NO3 und N2O5 relativ zueinander beruht, wurde das Verhältnis γ(NO3)/γ(N2O5) der Aufnahmekoeffizienten von NO3 und N2O5 auf Saharastaub zu 0,9 ± 0,4 (1σ) bestimmt. Dieser Wert war unabhängig von der relativen Feuchte, den NO3- und N2O5-Konzentrationen sowie der Reaktionszeit, obwohl eine Oberflächendeaktivierung für beide Spurenstoffe beobachtet wurde.

Na +-coupled betaine symporters involved in osmotic stress response in prokaryotes and eukaryotes

The betaine/GABA transporter BGT1 is one of the most important osmolyte transporters in the kidney. BGT1 is a member of the neurotransmitter sodium symporter (NSS) family, facilitates Na+/Cl--coupled betaine uptake to cope with hyperosmotic stress. Betaine transport in kidney cells is upregulated under hypertonic conditions by a yet unknown mechanism when increasing amounts of intracellular BGT1 are inserted into the plasma membrane. Re-establishing isotonicity results in ensuing depletion of BGT1 from the membrane. BGT1 phosphorylation on serines and threonines might be a regulation mechanism. In the present study, four potential PKC phosphorylation sites were mutated to alanines and the responses to PKC activators, phorbol 12-myristate acetate (PMA) and dioctanoyl-sn-glycerol (DOG) were determined. GABA-sensitive currents were diminished after 30 min preincubation with these PKC activators. Staurosporine blocked the response to DOG. Three mutants evoked normal GABA-sensitive currents but currents in oocytes expressing the mutant T40A were greatly diminished. [3H]GABA uptake was also determined in HEK-293 cells expressing EGFP-tagged BGT1 with the same mutations. Three mutants showed normal upregulation of GABA uptake after hypertonic stress, and downregulation by PMA was normal compared to EGFP-BGT1. In contrast, GABA uptake by the T40A mutant showed no response to hypertonicity or PMA. Confocal microscopy of the EGFP-BGT1 mutants expressed in MDCK cells, grown on glass or filters, revealed that T40A was present in the cytoplasm after 24 h hypertonic stress while the other mutants and EGFP-BGT1 were predominantely present in the plasma membrane. All four mutants co-migrated with EGFP-BGT1 on Western blots suggesting they are full-length proteins. In conclusion, T235, S428, and S564 are not involved in downregulation of BGT1 due to phosphorylation by PKC. However, T40 near the N-terminus may be part of a hot spot important for normal trafficking or insertion of BGT1 into the plasma membrane. Additionally, a link between substrate transport regulation, insertion of BGT1 into the plasma membrane and N-glycosylation in the extracellular loop 2 (EL2) could be revealed. The functional importance of two predicted N-glycosylation sites, which are conserved in EL2 within the NSS family were investigated for trafficking, transport and regulated plasma membrane insertion by immunogold-labelling, electron microscopy, mutagenesis, two-electrode voltage clamp measurements in Xenopus laevis oocytes and uptake of radioactive-labelled substrate into MDCK cells. Trafficking and plasma membrane insertion of BGT1 was clearly promoted by proper N-glycosylation in both, oocytes and MDCK cells. De-glycosylation with PNGase F or tunicamycin led to a decrease in substrate affinity and transport rate. Mutagenesis studies revealed that in BGT1 N183 is the major N-glycosylation site responsible for full protein activity. Replacement of N183 with aspartate resulted in a mutant, which was not able to bind N-glycans suggesting that N171 is a non-glycosylated site in BGT1. N183D exhibited close to WT transport properties in oocytes. Surprisingly, in MDCK cells plasma membrane insertion of the N183D mutant was no longer regulated by osmotic stress indicating unambiguously that association with N-glycans at this position is linked to osmotic stress-induced transport regulation in BGT1. The molecular transport mechanism of BGT1 remains largely unknown in the absence of a crystal structure. Therefore investigating the structure-function relationship of BGT1 by a combination of structural biology (2D and 3D crystallization) and membrane protein biochemistry (cell culture, substrate transport by radioactive labeled GABA uptake into cells and proteoliposomes) was the aim of this work. While the functional assays are well established, structure determination of eukaryotic membrane transporters is still a challenge. Therefore, a suitable heterologous expression system could be defined, starting with cloning and overexpression of an optimized gene. The achieved expression levels in P. pastoris were high enough to proceed with isolation of BGT1. Furthermore, purification protocols could be established and resulted in pure protein, which could even be reconstituted in an active form. The quality and homogeneity of the protein allowed already 2D and 3D crystallization, in which initial crystals could be obtained. Interestingly, the striking structural similarity of BGT1 to the bacterial betaine transporter BetP, which became a paradigm for osmoregulated betaine transport, provided information on substrate coordination in BGT1. The structure of a BetP mutant that showed activity for GABA was solved to 3.2Å in complex with GABA in an inward facing open state. This structure shed some light into the molecular transport mechanisms in BGT1 and might help in future to design conformationally locked BGT1 to enforce the on-going structure determination.

The influence of pulmonary surfactant on nanoparticulate drug delivery systems

The pulmonary route is very attractive for drug delivery by inhalation. In this regard, nanoparticulate drug delivery systems, designed as multifunctional engineered nanoparticles, are very promising since they combine several opportunities like a rather uniform distribution of drug dose among all ventilated alveoli allowing for uniform cellular drug internalization. However, although the field of nanomedicine offers multiple opportunities, it still is in its infancy and the research has to proceed in order to obtain a specific targeting of the drug combined with minimum side effects. If inhaled nanoparticulate drug delivery systems are deposited on the pulmonary surfactant, they come into contact with phospholipids and surfactant proteins. It is highly likely that the interaction of nanoparticulate drug delivery systems with surfactant phospholipids and proteins will be able to mediate/modulate the further fate of this specific drug delivery system. In the present comment, we discuss the potential interactions of nanoparticulate drug delivery systems with pulmonary surfactant as well as the potential consequences of this interaction.

Glycogen-rich pleomorphic xanthoastrocytoma with clear-cell features: confirmatory report of a rare variant with implications for differential diagnosis

Central nervous system space-occupying lesions with clear-cell features encompass a nosologically heterogeneous array, ranging from reactive histiocytic proliferations to neuroepithelial or meningothelial neoplasms of various grades and to metastases. In the face of such differential diagnostic breadth, recognizing cytoplasmic lucency as part of the morphological spectrum of some low grade gliomas will directly have an impact on patient care. We describe a prevailing clear-cell change in an epileptogenic left temporal pleomorphic xanthoastrocytoma surgically resected from a 36-year-old man. Mostly subarachnoid and focally calcified, the tumor was composed of fascicles of moderately atypical spindle cells with optically lucent cytoplasm that tended to intermingle with a desmoplastic mesh of reticulin fibers. Immunohistochemically, coexpression of S100 protein, vimentin, GFAP, and CD34 was noted. Conversely, neither punctate staining for EMA nor positivity for CD68 was seen. Mitotic activity was absent, and the MIB1 labeling index was 2-3% on average. Diastase-sensitive PAS-positive granula indicated clear-cell change to proceed from glycogen storage. Electron microscopy showed tumor cell cytoplasm to be largely obliterated by non-lysosomal-bound pools of glycogen, while hardly any fat vacuole was encountered. Neither ependymal-derived organelles nor annular lamellae suggesting oligodendroglial differentiation were detected. The latter differential diagnosis was further invalidated by lack of codeletion of chromosomal regions 1p36 and 19q13 on molecular genetic testing. By significantly interfering with pattern recognition as an implicit approach in histopathology, clear-cell change in pleomorphic xanthoastrocytoma is likely to suspend its status as a "classic", and to prompt more deductive differential diagnostic strategies to exclude look-alikes, especially clear-cell ependymoma and oligodendroglioma.

Experimental and Theoretical Study of the OH Vibrational Spectra and Overtone Chemistry of Gas-Phase Vinylacetic Acid

In this study we present the gas-phase vibrational spectrum of vinylacetic acid with a focus on the ν = 1−5 vibrational states of the OH stretching transitions. Cross sections for ν = 1, 2, 4 and 5 of the OH stretching vibrational transitions are derived on the basis of the vapor pressure data obtained for vinylacetic acid. Ab initio calculations are used to assist in the band assignments of the experimental spectra, and to determine the threshold for the decarboxylation of vinylacetic acid. When compared to the theoretical energy barrier to decarboxylation, it is found that the νOH = 4 transition with thermal excitation of low frequency modes or rotational motion and νOH = 5 transitions have sufficient energy for the reaction to proceed following overtone excitation.

The Synthesis of Macrocyclic Polystyrene by Sequential Atom Transfer Radical Reactions

A method for the production of macrocyclic polystyrene via ring closing of a linear !,"-dibrominated polystyrene by an Atom Transfer Radical Coupling (ATRC) reaction is described. The dibrominated polystyrene chain was produced from two simultaneous atom transfer radical polymerizations (ATRPs) originating from a dibrominated benzal bromide initiator. To ensure the retention of the halogen end groups polymerization was allowed to proceed to less than 50% conversion. Using this precursor in an intramolecular ATRC (ring closing) reaction was found to yield in excess of 90% cyclic product based on refractive index-gel permeation chromatography (GPC) analysis. The cyclic architecture of the polymer was verified by GPC, Nuclear Magnetic Resonance (NMR), and mass spectrometry analysis. The utility of this method has been expanded by the addition of 2-methyl-2-nitrosopropane to the coupling reaction, which allows for the coupling to proceed at a faster rate and to yield macrocycles with incorporated alkoxyamine functionality. The alkoxyamine functionality allows for degradation of the cycles at high temperatures (>125° C) and we hypothesize that it may allow the macrocycles to act as a macroinitiator for a ring expansion polymerization in future studies.

State Pharmaceutical Assisstance for the Elderly and Disabled: Planning Issues for Program and Non-Program States

The Medicare Catastrophic Coverage Act (MCCA) would have mandated federal assistance for Medicare beneficiaries who have high annual prescription medication costs, High national expenditures for such drugs have encouraged the development of private and state insurance programs to help with these costs. Ten state pharmaceutical assistance programs (SPAPs), designed to help certain elderly, low income, or disabled people, exist for those ineligible for Medicaid or unable to purchase coverage privately. Coordination of state and federal benefits was a consideration for established programs, and programs being planned needed to determine the feasibity of integration of federal assistance. But the enactment and subsequent appeal of the Act affected both planning and policy implications for these SPAPs. All U.S. states and territories were surveyed before the bill's repeal to collect data on the effects of MCCA for those with prescription drug programs and those without. The repeal of the federal program places pressure on the nonprogram states to proceed, perhaps more cautiously, to initiate program; for their own residents, given increasing out-of-pocket and insurance costs, and no federal program.

Leaf Asymmetry as a Developmental Constraint Imposed by Auxin-Dependent Phyllotactic Patterning

In a majority of species, leaf development is thought to proceed in a bilaterally symmetric fashion without systematic asymmetries. This is despite the left and right sides of an initiating primordium occupying niches that differ in their distance from sinks and sources of auxin. Here, we revisit an existing model of auxin transport sufficient to recreate spiral phyllotactic patterns and find previously overlooked asymmetries between auxin distribution and the centers of leaf primordia. We show that it is the direction of the phyllotactic spiral that determines the side of the leaf these asymmetries fall on. We empirically confirm the presence of an asymmetric auxin response using a DR5 reporter and observe morphological asymmetries in young leaf primordia. Notably, these morphological asymmetries persist in mature leaves, and we observe left-right asymmetries in the superficially bilaterally symmetric leaves of tomato (Solanum lycopersicum) and Arabidopsis thaliana that are consistent with modeled predictions. We further demonstrate that auxin application to a single side of a leaf primordium is sufficient to recapitulate the asymmetries we observe. Our results provide a framework to study a previously overlooked developmental axis and provide insights into the developmental constraints imposed upon leaf morphology by auxin-dependent phyllotactic patterning.

Traumatic free wall and ventricular septal rupture - 'hybrid' management in a child

A 8-year-old boy showed a traumatic ventricular septal rupture following a blunt chest trauma, and was scheduled for elective catheter closure. Two weeks later, a follow-up echocardiogram revealed a pseudoaneurysm of the anterior wall of the left ventricle. Because of the apical location of the VSD, it was decided to proceed with transcatheter occlusion. After successful VSD closure, the patient was taken to the operation room for surgical repair of the left ventricular pseudoaneurysm. Symptoms and signs seen in patients with ventricular pseudoaneurysms appear to be discrete and variable, and a high clinical index of suspicion with a very close echocardiographic follow-up is strongly recommended after occurrence of a blunt cardiac trauma. The combined 'hybrid' approach of transcatheter closure of the intraventricular rupture followed by surgical closure of the pseudoaneurysm allows for a less invasive and efficient management of this rare combination of post-traumatic ventricular free wall and septal rupture in a child.