The Interactive Effect of GHR-Exon 3 and -202 A/C IGFBP3 Polymorphisms on rhGH Responsiveness and Treatment Outcomes in Patients with Turner Syndrome

Context: There is great interindividual variability in the response to recombinant human (rh) GH therapy in patients with Turner syndrome (TS). Ascertaining genetic factors can improve the accuracy of growth response predictions. Objective: The objective of the study was to assess the individual and combined influence of GHR-exon 3 and -202 A/C IGFBP3 polymorphisms on the short-and long-term outcomes of rhGH therapy in patients with TS. Design and Patients: GHR-exon 3 and -202 A/C IGFBP3 genotyping (rs2854744) was correlated with height data of 112 patients with TS who remained prepubertal during the first year of rhGH therapy and 65 patients who reached adult height after 5 +/- 2.5 yr of rhGH treatment. Main Outcome Measures: First-year growth velocity and adult height were measured. Results: Patients carrying at least one GHR-d3 or -202 A-IGFBP3 allele presented higher mean first-year growth velocity and achieved taller adult heights than those homozygous for GHR-fl or -202 C-IGFBP3 alleles, respectively. The combined analysis of GHR-exon 3 and -202 A/C IGFBP3 genotypes showed a clear nonadditive epistatic influence on adult height of patients with TS treated with rhGH (GHR-exon 3 alone, R-2 = 0.27; -202 A/C IGFBP3, R-2 = 0.24; the combined genotypes, R-2 = 0.37 at multiple linear regression). Together with clinical factors, these genotypes accounted for 61% of the variability in adult height of patients with TS after rhGH therapy. Conclusion: Homozygosity for the GHR-exon3 full-length allele and/or the -202C-IGFBP3 allele are associated with less favorable short-and long-term growth outcomes after rhGH treatment in patients with TS. (J Clin Endocrinol Metab 97: E671-E677, 2012)

Auditory brainstem implant outcomes and MAP parameters: Report of experiences in adults and children

The auditory brainstem implant (ABI) was first developed to help neurofibromatosis type 2 patients. Recently, its use has been recently extended to adults with non-tumor etiologies and children with profound hearing loss who were not candidates for a cochlear implant (Cl). Although the results has been extensively reported, the stimulation parameters involved behind the outcomes have received less attention. Objective: The aim of this study is to describe the audiologic outcomes and the MAP parameters in ABI adults and children at our center. Methods: Retrospective chart review. Five adults and four children were implanted with the ABI24M from September 2005 to June 2009. In the adult patients, four had Neurofibromatosis type 2, and one had postmeningitic deafness with complete ossification of both cochleae. Three of the children had cochlear malformation or dysplasia, and one had complete ossified cochlea due to meningitis. Map parameters as well as the intraoperative electrical auditory brainstem responses were collected. Evaluation was performed with at least six months of device use and included free-field hearing thresholds, speech perception tests in the adult patients and for the children, the Infant-Toddler Meaningful Auditory Integration Scale (IT-MAIS) and (ESP) were used to evaluate the development of auditory skills, besides the MUSS to evaluate. Results: The number of active electrodes that did not cause any non-auditory sensation varied from three to nineteen. All of them were programmed with SPEAK strategy, and the pulse widths varied from 100 to 300 mu s. Free-field thresholds with warble tones varied from very soft auditory sensation of 70 dBHL at 250 Hz to a pure tone average of 45 dBHL. Speech perception varied from none to 60% open-set recognition of sentences in silence in the adult population and from no auditory sensation at all to a slight improvement in the IT-MAIS/MAIS scores. Conclusion: We observed that ABI may be a good option for offering some hearing attention to both adults and children. In children, the results might not be enough to ensure oral language development. Programming the speech processor in children demands higher care to the audiologist. (C) 2011 Elsevier Ireland Ltd. All rights reserved.

Assessment of SNPs for linkage mapping in Eucalyptus: construction of a consensus SNP/microsatellite map from two unrelated pedigrees

Financial support. Brazilian Ministry of Science and Technology (CNPq Grant 577047-2008-6), FAP-DF NEXTREE Grant 193.000.570/2009 and EMBRAPA Macroprogram 2 project grant 02.07.01.004.

Canine heartworm disease in Porto Velho: first record, distribution map and occurrence of positive mosquitoes

The aim of this study was to make the first report on canine heartworm disease in the state of Rondônia and confirm its transmission in this state. Blood samples were randomly collected from 727 dogs in the city of Porto Velho. The samples were analyzed to search for microfilariae and circulating antigens, using three different techniques: optical microscopy on thick blood smears stained with Giemsa; immunochromatography; and PCR. Mosquitoes were collected inside and outside the homes of all the cases of positive dogs and were tested using PCR to search for DNA of Dirofilaria immitis. Ninety-three blood samples out of 727 (12.8%) were positive according to the immunoassay technique and none according to the thick smear method. Among the 93 positive dogs, 89 (95.7%) were born in Porto Velho. No difference in the frequency of infection was observed between dogs raised indoors and in the yard. PCR on the mosquitoes resulted in only one positive pool. This result shows that the transmission of canine heartworm disease is occurring in the city of Porto Velho and that there is moderate prevalence among the dogs. The techniques of immunochromatography and PCR were more effective for detecting canine heartworm than thick blood smears. The confirmation of canine heartworm disease transmission in Porto Velho places this disease in the ranking for differential diagnosis of pulmonary nodules in humans in Rondônia.

Dense disparity map estimation respecting image discontinuities

[EN] We present an energy based approach to estimate a dense disparity map from a set of two weakly calibrated stereoscopic images while preserving its discontinuities resulting from image boundaries. We first derive a simplified expression for the disparity that allows us to estimate it from a stereo pair of images using an energy minimization approach. We assume that the epipolar geometry is known, and we include this information in the energy model. Discontinuities are preserved by means of a regularization term based on the Nagel-Enkelmann operator. We investigate the associated Euler-Lagrange equation of the energy functional, and we approach the solution of the underlying partial differential equation (PDE) using a gradient descent method The resulting parabolic problem has a unique solution. In order to reduce the risk to be trapped within some irrelevant local minima during the iterations, we use a focusing strategy based on a linear scalespace. Experimental results on both synthetic and real images arere presented to illustrate the capabilities of this PDE and scale-space based method.

Interactive application in spanish sign language for a public transport environment

[ES] En este trabajo se presenta el diseño de una herramienta multimedia que traduce a la lengua de signos españolas los mensajes de avisos que puede proporcionar un sistema de megafonía. El objetivo del trabajo es proporcionar una herramienta que mejore la inclusión social de las personas con discapacidades auditivas. Con este propósito, se han seleccionado el entorno y los mensajes de audio habituales en un aeropuerto para desarrollar este proyecto piloto. Por último, los audios se han traducido a lengua de signos españolas sintetizando un avatar usando la técnica de animación de rotoscopía a partir de la grabación en vídeo de un traductor. Los resultados finales han sido evaluados por personas sordas.

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.

Automatic initialization for facial analysis in interactive robotics

[EN]This paper focuses on four different initialization methods for determining the initial shape for the AAM algorithm and their particular performance in two different classification tasks with respect to either the facial expression DaFEx database and to the real world data obtained from a robot’s point of view.

A novel map-matching procedure for low-sampling GPS data with applications to traffic flow analysis

An extensive sample (2%) of private vehicles in Italy are equipped with a GPS device that periodically measures their position and dynamical state for insurance purposes. Having access to this type of data allows to develop theoretical and practical applications of great interest: the real-time reconstruction of traffic state in a certain region, the development of accurate models of vehicle dynamics, the study of the cognitive dynamics of drivers. In order for these applications to be possible, we first need to develop the ability to reconstruct the paths taken by vehicles on the road network from the raw GPS data. In fact, these data are affected by positioning errors and they are often very distanced from each other (~2 Km). For these reasons, the task of path identification is not straightforward. This thesis describes the approach we followed to reliably identify vehicle paths from this kind of low-sampling data. The problem of matching data with roads is solved with a bayesian approach of maximum likelihood. While the identification of the path taken between two consecutive GPS measures is performed with a specifically developed optimal routing algorithm, based on A* algorithm. The procedure was applied on an off-line urban data sample and proved to be robust and accurate. Future developments will extend the procedure to real-time execution and nation-wide coverage.

Interactive simulation of flexible parts

Computer simulations play an ever growing role for the development of automotive products. Assembly simulation, as well as many other processes, are used systematically even before the first physical prototype of a vehicle is built in order to check whether particular components can be assembled easily or whether another part is in the way. Usually, this kind of simulation is limited to rigid bodies. However, a vehicle contains a multitude of flexible parts of various types: cables, hoses, carpets, seat surfaces, insulations, weatherstrips... Since most of the problems using these simulations concern one-dimensional components and since an intuitive tool for cable routing is still needed, we have chosen to concentrate on this category, which includes cables, hoses and wiring harnesses. In this thesis, we present a system for simulating one dimensional flexible parts such as cables or hoses. The modeling of bending and torsion follows the Cosserat model. For this purpose we use a generalized spring-mass system and describe its configuration by a carefully chosen set of coordinates. Gravity and contact forces as well as the forces responsible for length conservation are expressed in Cartesian coordinates. But bending and torsion effects can be dealt with more effectively by using quaternions to represent the orientation of the segments joining two neighboring mass points. This augmented system allows an easy formulation of all interactions with the best appropriate coordinate type and yields a strongly banded Hessian matrix. An energy minimizing process accounts for a solution exempt from the oscillations that are typical of spring-mass systems. The use of integral forces, similar to an integral controller, allows to enforce exactly the constraints. The whole system is numerically stable and can be solved at interactive frame rates. It is integrated in the DaimlerChrysler in-house Virtual Reality Software veo for use in applications such as cable routing and assembly simulation and has been well received by users. Parts of this work have been published at the ACM Solid and Physical Modeling Conference 2006 and have been selected for the special issue of the Computer-Aided-Design Journal to the conference.