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.

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.

Strategie competitive nel settore dei videogiochi: Il caso di take-two interactive

Partendo da un’analisi di mercato che si sviluppa meglio con una segmentazione, andremo ad analizzare il settore degli editori di videogiochi, le loro quote di mercato e come si stanno evolvendo per rimanere al passo con la tecnologia in un settore con forte competizione. Lo scopo di questa tesi è spiegare il successo della Take Two Interactive descrivendo la sua storia, le strategia che ha adottato negli anni per arrivare a competere con altri grandi editori e come si sta approcciando alle nuove tecnologie, all’evoluzione dei comportamenti d’acquisto dei consumatori e ai nuovi mercati emergenti.

Software tools and efficient algorithms for the feature detection, feature tracking, event localization, and visualization of large sets of atmospheric data

Data sets describing the state of the earth's atmosphere are of great importance in the atmospheric sciences. Over the last decades, the quality and sheer amount of the available data increased significantly, resulting in a rising demand for new tools capable of handling and analysing these large, multidimensional sets of atmospheric data. The interdisciplinary work presented in this thesis covers the development and the application of practical software tools and efficient algorithms from the field of computer science, aiming at the goal of enabling atmospheric scientists to analyse and to gain new insights from these large data sets. For this purpose, our tools combine novel techniques with well-established methods from different areas such as scientific visualization and data segmentation. In this thesis, three practical tools are presented. Two of these tools are software systems (Insight and IWAL) for different types of processing and interactive visualization of data, the third tool is an efficient algorithm for data segmentation implemented as part of Insight.Insight is a toolkit for the interactive, three-dimensional visualization and processing of large sets of atmospheric data, originally developed as a testing environment for the novel segmentation algorithm. It provides a dynamic system for combining at runtime data from different sources, a variety of different data processing algorithms, and several visualization techniques. Its modular architecture and flexible scripting support led to additional applications of the software, from which two examples are presented: the usage of Insight as a WMS (web map service) server, and the automatic production of a sequence of images for the visualization of cyclone simulations. The core application of Insight is the provision of the novel segmentation algorithm for the efficient detection and tracking of 3D features in large sets of atmospheric data, as well as for the precise localization of the occurring genesis, lysis, merging and splitting events. Data segmentation usually leads to a significant reduction of the size of the considered data. This enables a practical visualization of the data, statistical analyses of the features and their events, and the manual or automatic detection of interesting situations for subsequent detailed investigation. The concepts of the novel algorithm, its technical realization, and several extensions for avoiding under- and over-segmentation are discussed. As example applications, this thesis covers the setup and the results of the segmentation of upper-tropospheric jet streams and cyclones as full 3D objects. Finally, IWAL is presented, which is a web application for providing an easy interactive access to meteorological data visualizations, primarily aimed at students. As a web application, the needs to retrieve all input data sets and to install and handle complex visualization tools on a local machine are avoided. The main challenge in the provision of customizable visualizations to large numbers of simultaneous users was to find an acceptable trade-off between the available visualization options and the performance of the application. Besides the implementational details, benchmarks and the results of a user survey are presented.

An interactive surgical planning tool for acetabular fractures: initial results

Background Acetabular fractures still are among the most challenging fractures to treat because of complex anatomy, involved surgical access to fracture sites and the relatively low incidence of these lesions. Proper evaluation and surgical planning is necessary to achieve anatomic reduction of the articular surface and stable fixation of the pelvic ring. The goal of this study was to test the feasibility of preoperative surgical planning in acetabular fractures using a new prototype planning tool based on an interactive virtual reality-style environment. Methods 7 patients (5 male and 2 female; median age 53 y (25 to 92 y)) with an acetabular fracture were prospectively included. Exclusion criterions were simple wall fractures, cases with anticipated surgical dislocation of the femoral head for joint debridement and accurate fracture reduction. According to the Letournel classification 4 cases had two column fractures, 2 cases had anterior column fractures and 1 case had a T-shaped fracture including a posterior wall fracture. The workflow included following steps: (1) Formation of a patient-specific bone model from preoperative computed tomography scans, (2) interactive virtual fracture reduction with visuo-haptic feedback, (3) virtual fracture fixation using common osteosynthesis implants and (4) measurement of implant position relative to landmarks. The surgeon manually contoured osteosynthesis plates preoperatively according to the virtually defined deformation. Screenshots including all measurements for the OR were available. The tool was validated comparing the preoperative planning and postoperative results by 3D-superimposition. Results Preoperative planning was feasible in all cases. In 6 of 7 cases superimposition of preoperative planning and postoperative follow-up CT showed a good to excellent correlation. In one case part of the procedure had to be changed due to impossibility of fracture reduction from an ilioinguinal approach. In 3 cases with osteopenic bone patient-specific prebent fixation plates were helpful in guiding fracture reduction. Additionally, anatomical landmark based measurements were helpful for intraoperative navigation. Conclusion The presented prototype planning tool for pelvic surgery was successfully integrated in a clinical workflow to improve patient-specific preoperative planning, giving visual and haptic information about the injury and allowing a patient-specific adaptation of osteosynthesis implants to the virtually reduced pelvis.

Disabling c-Myc in childhood medulloblastoma and atypical teratoid/rhabdoid tumor cells by the potent G-quadruplex interactive agent S2T1-6OTD

We investigated here the effects of S2T1-6OTD, a novel telomestatin derivative that is synthesized to target G-quadruplex-forming DNA sequences, on a representative panel of human medulloblastoma (MB) and atypical teratoid/rhabdoid (AT/RT) childhood brain cancer cell lines. S2T1-6OTD proved to be a potent c-Myc inhibitor through its high-affinity physical interaction with the G-quadruplex structure in the c-Myc promoter. Treatment with S2T1-6OTD reduced the mRNA and protein expressions of c-Myc and hTERT, which is transcriptionally regulated by c-Myc, and decreased the activities of both genes. In remarkable contrast to control cells, short-term (72-hour) treatment with S2T1-6OTD resulted in a dose- and time-dependent antiproliferative effect in all MB and AT/RT brain tumor cell lines tested (IC(50), 0.25-0.39 micromol/L). Under conditions where inhibition of both proliferation and c-Myc activity was observed, S2T1-6OTD treatment decreased the protein expression of the cell cycle activator cyclin-dependent kinase 2 and induced cell cycle arrest. Long-term treatment (5 weeks) with nontoxic concentrations of S2T1-6OTD resulted in a time-dependent (mainly c-Myc-dependent) telomere shortening. This was accompanied by cell growth arrest starting on day 28 followed by cell senescence and induction of apoptosis on day 35 in all of the five cell lines investigated. On in vivo animal testing, S2T1-6OTD may well represent a novel therapeutic strategy for childhood brain tumors.

Magnetic resonance imaging based determination of body compartments with the versatile, interactive sparse sampling (VISS) method

To investigate the inhomogeneity of radiofrequency fields at higher field strengths that can interfere with established volumetric methods, in particular for the determination of visceral (VAT) and subcutaneous adipose tissue (SCAT). A versatile, interactive sparse sampling (VISS) method is proposed to determine VAT, SCAT, and also total body volume (TBV).

A new model of interactive effects of alcohol and high-fat diet on hepatic fibrosis

Alcoholic steatohepatitis (ASH) and nonalcoholic steatohepatitis (NASH) are the most frequent conditions leading to elevated liver enzymes and liver cirrhosis, respectively, in the Western world. However, despite strong epidemiological evidence for combined effects on the progression of liver injury, the mutual interaction of the pathophysiological mechanisms is incompletely understood. The aim of this study was to establish and analyze an experimental murine model, where we combined chronic alcohol administration with a NASH-inducing high-fat (HF) diet.