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.

Methodological improvement of 3D fluoroscopic analysis for the robust quantification of 3D kinematics of human joints

3D video-fluoroscopy is an accurate but cumbersome technique to estimate natural or prosthetic human joint kinematics. This dissertation proposes innovative methodologies to improve the 3D fluoroscopic analysis reliability and usability. Being based on direct radiographic imaging of the joint, and avoiding soft tissue artefact that limits the accuracy of skin marker based techniques, the fluoroscopic analysis has a potential accuracy of the order of mm/deg or better. It can provide fundamental informations for clinical and methodological applications, but, notwithstanding the number of methodological protocols proposed in the literature, time consuming user interaction is exploited to obtain consistent results. The user-dependency prevented a reliable quantification of the actual accuracy and precision of the methods, and, consequently, slowed down the translation to the clinical practice. The objective of the present work was to speed up this process introducing methodological improvements in the analysis. In the thesis, the fluoroscopic analysis was characterized in depth, in order to evaluate its pros and cons, and to provide reliable solutions to overcome its limitations. To this aim, an analytical approach was followed. The major sources of error were isolated with in-silico preliminary studies as: (a) geometric distortion and calibration errors, (b) 2D images and 3D models resolutions, (c) incorrect contour extraction, (d) bone model symmetries, (e) optimization algorithm limitations, (f) user errors. The effect of each criticality was quantified, and verified with an in-vivo preliminary study on the elbow joint. The dominant source of error was identified in the limited extent of the convergence domain for the local optimization algorithms, which forced the user to manually specify the starting pose for the estimating process. To solve this problem, two different approaches were followed: to increase the optimal pose convergence basin, the local approach used sequential alignments of the 6 degrees of freedom in order of sensitivity, or a geometrical feature-based estimation of the initial conditions for the optimization; the global approach used an unsupervised memetic algorithm to optimally explore the search domain. The performances of the technique were evaluated with a series of in-silico studies and validated in-vitro with a phantom based comparison with a radiostereometric gold-standard. The accuracy of the method is joint-dependent, and for the intact knee joint, the new unsupervised algorithm guaranteed a maximum error lower than 0.5 mm for in-plane translations, 10 mm for out-of-plane translation, and of 3 deg for rotations in a mono-planar setup; and lower than 0.5 mm for translations and 1 deg for rotations in a bi-planar setups. The bi-planar setup is best suited when accurate results are needed, such as for methodological research studies. The mono-planar analysis may be enough for clinical application when the analysis time and cost may be an issue. A further reduction of the user interaction was obtained for prosthetic joints kinematics. A mixed region-growing and level-set segmentation method was proposed and halved the analysis time, delegating the computational burden to the machine. In-silico and in-vivo studies demonstrated that the reliability of the new semiautomatic method was comparable to a user defined manual gold-standard. The improved fluoroscopic analysis was finally applied to a first in-vivo methodological study on the foot kinematics. Preliminary evaluations showed that the presented methodology represents a feasible gold-standard for the validation of skin marker based foot kinematics protocols.

Enabling Human Centric Smart Campuses via Edge Computing and Connected Objects

Early definitions of Smart Building focused almost entirely on the technology aspect and did not suggest user interaction at all. Indeed, today we would attribute it more to the concept of the automated building. In this sense, control of comfort conditions inside buildings is a problem that is being well investigated, since it has a direct effect on users’ productivity and an indirect effect on energy saving. Therefore, from the users’ perspective, a typical environment can be considered comfortable, if it’s capable of providing adequate thermal comfort, visual comfort and indoor air quality conditions and acoustic comfort. In the last years, the scientific community has dealt with many challenges, especially from a technological point of view. For instance, smart sensing devices, the internet, and communication technologies have enabled a new paradigm called Edge computing that brings computation and data storage closer to the location where it is needed, to improve response times and save bandwidth. This has allowed us to improve services, sustainability and decision making. Many solutions have been implemented such as smart classrooms, controlling the thermal condition of the building, monitoring HVAC data for energy-efficient of the campus and so forth. Though these projects provide to the realization of smart campus, a framework for smart campus is yet to be determined. These new technologies have also introduced new research challenges: within this thesis work, some of the principal open challenges will be faced, proposing a new conceptual framework, technologies and tools to move forward the actual implementation of smart campuses. Keeping in mind, several problems known in the literature have been investigated: the occupancy detection, noise monitoring for acoustic comfort, context awareness inside the building, wayfinding indoor, strategic deployment for air quality and books preserving.

Specification, execution and verification of interaction protocols: an approach based on computational logic

Interaction protocols establish how different computational entities can interact with each other. The interaction can be finalized to the exchange of data, as in 'communication protocols', or can be oriented to achieve some result, as in 'application protocols'. Moreover, with the increasing complexity of modern distributed systems, protocols are used also to control such a complexity, and to ensure that the system as a whole evolves with certain features. However, the extensive use of protocols has raised some issues, from the language for specifying them to the several verification aspects. Computational Logic provides models, languages and tools that can be effectively adopted to address such issues: its declarative nature can be exploited for a protocol specification language, while its operational counterpart can be used to reason upon such specifications. In this thesis we propose a proof-theoretic framework, called SCIFF, together with its extensions. SCIFF is based on Abductive Logic Programming, and provides a formal specification language with a clear declarative semantics (based on abduction). The operational counterpart is given by a proof procedure, that allows to reason upon the specifications and to test the conformance of given interactions w.r.t. a defined protocol. Moreover, by suitably adapting the SCIFF Framework, we propose solutions for addressing (1) the protocol properties verification (g-SCIFF Framework), and (2) the a-priori conformance verification of peers w.r.t. the given protocol (AlLoWS Framework). We introduce also an agent based architecture, the SCIFF Agent Platform, where the same protocol specification can be used to program and to ease the implementation task of the interacting peers.

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.

Per un museo virtuale dell'informatica. Un supporto automatico per creare "visite museali"

The subject of the present research is related to the field of computer technology applied to support intellectual activities such as text translation, screenwriting and content organization of popular and education courses, especially concerning museum visits. The research has started with the deep analysis of the cognitive process which characterizes a screenwriter while working. This choice has been made because a screenplay is not only an aid to the realization of a show but, more in general, it can be considered as the planning of an education, popular and formative intellectual activity. After this analysis, the research has focused on the specific area of the planning, description and introduction of topics related to the history of science, and in particular, of computer science. To focus on this area it has been fundamental to analyse subjects concerning the didactics of museum visits organization. The aim was to find out the guide lines that a teacher should follow when planning the visit of a museum (virtual museum of the history of computer science). The consequent designing and realisation of an automatic support system for the description and the production of a formative, education and popular multimedia product (for the history of computer science), has been possible thanks to the results achieved through this research. The system obtained is provided by the following features: ·management of multimedia slides (such as texts, video, audio or images) which can be classified on the bases of the topic and of the profile of the user; ·automatic creation of a sequence of multimedia slides which introduce the topic; ·management of the interaction with the user to check and give validity to the product. The most innovative aspect of the present research is represented by the fact that the product is realised on the bases of the profile of the user.

Creazione e sviluppo di corpora multimediali. Nuove metodologie di ricerca nella traduzione audiovisiva

The construction and use of multimedia corpora has been advocated for a while in the literature as one of the expected future application fields of Corpus Linguistics. This research project represents a pioneering experience aimed at applying a data-driven methodology to the study of the field of AVT, similarly to what has been done in the last few decades in the macro-field of Translation Studies. This research was based on the experience of Forlixt 1, the Forlì Corpus of Screen Translation, developed at the University of Bologna’s Department of Interdisciplinary Studies in Translation, Languages and Culture. As a matter of fact, in order to quantify strategies of linguistic transfer of an AV product, we need to take into consideration not only the linguistic aspect of such a product but all the meaning-making resources deployed in the filmic text. Provided that one major benefit of Forlixt 1 is the combination of audiovisual and textual data, this corpus allows the user to access primary data for scientific investigation, and thus no longer rely on pre-processed material such as traditional annotated transcriptions. Based on this rationale, the first chapter of the thesis sets out to illustrate the state of the art of research in the disciplinary fields involved. The primary objective was to underline the main repercussions on multimedia texts resulting from the interaction of a double support, audio and video, and, accordingly, on procedures, means, and methods adopted in their translation. By drawing on previous research in semiotics and film studies, the relevant codes at work in visual and acoustic channels were outlined. Subsequently, we concentrated on the analysis of the verbal component and on the peculiar characteristics of filmic orality as opposed to spontaneous dialogic production. In the second part, an overview of the main AVT modalities was presented (dubbing, voice-over, interlinguistic and intra-linguistic subtitling, audio-description, etc.) in order to define the different technologies, processes and professional qualifications that this umbrella term presently includes. The second chapter focuses diachronically on various theories’ contribution to the application of Corpus Linguistics’ methods and tools to the field of Translation Studies (i.e. Descriptive Translation Studies, Polysystem Theory). In particular, we discussed how the use of corpora can favourably help reduce the gap existing between qualitative and quantitative approaches. Subsequently, we reviewed the tools traditionally employed by Corpus Linguistics in regard to the construction of traditional “written language” corpora, to assess whether and how they can be adapted to meet the needs of multimedia corpora. In particular, we reviewed existing speech and spoken corpora, as well as multimedia corpora specifically designed to investigate Translation. The third chapter reviews Forlixt 1's main developing steps, from a technical (IT design principles, data query functions) and methodological point of view, by laying down extensive scientific foundations for the annotation methods adopted, which presently encompass categories of pragmatic, sociolinguistic, linguacultural and semiotic nature. Finally, we described the main query tools (free search, guided search, advanced search and combined search) and the main intended uses of the database in a pedagogical perspective. The fourth chapter lists specific compilation criteria retained, as well as statistics of the two sub-corpora, by presenting data broken down by language pair (French-Italian and German-Italian) and genre (cinema’s comedies, television’s soapoperas and crime series). Next, we concentrated on the discussion of the results obtained from the analysis of summary tables reporting the frequency of categories applied to the French-Italian sub-corpus. The detailed observation of the distribution of categories identified in the original and dubbed corpus allowed us to empirically confirm some of the theories put forward in the literature and notably concerning the nature of the filmic text, the dubbing process and Italian dubbed language’s features. This was possible by looking into some of the most problematic aspects, like the rendering of socio-linguistic variation. The corpus equally allowed us to consider so far neglected aspects, such as pragmatic, prosodic, kinetic, facial, and semiotic elements, and their combination. At the end of this first exploration, some specific observations concerning possible macrotranslation trends were made for each type of sub-genre considered (cinematic and TV genre). On the grounds of this first quantitative investigation, the fifth chapter intended to further examine data, by applying ad hoc models of analysis. Given the virtually infinite number of combinations of categories adopted, and of the latter with searchable textual units, three possible qualitative and quantitative methods were designed, each of which was to concentrate on a particular translation dimension of the filmic text. The first one was the cultural dimension, which specifically focused on the rendering of selected cultural references and on the investigation of recurrent translation choices and strategies justified on the basis of the occurrence of specific clusters of categories. The second analysis was conducted on the linguistic dimension by exploring the occurrence of phrasal verbs in the Italian dubbed corpus and by ascertaining the influence on the adoption of related translation strategies of possible semiotic traits, such as gestures and facial expressions. Finally, the main aim of the third study was to verify whether, under which circumstances, and through which modality, graphic and iconic elements were translated into Italian from an original corpus of both German and French films. After having reviewed the main translation techniques at work, an exhaustive account of possible causes for their non-translation was equally provided. By way of conclusion, the discussion of results obtained from the distribution of annotation categories on the French-Italian corpus, as well as the application of specific models of analysis allowed us to underline possible advantages and drawbacks related to the adoption of a corpus-based approach to AVT studies. Even though possible updating and improvement were proposed in order to help solve some of the problems identified, it is argued that the added value of Forlixt 1 lies ultimately in having created a valuable instrument, allowing to carry out empirically-sound contrastive studies that may be usefully replicated on different language pairs and several types of multimedia texts. Furthermore, multimedia corpora can also play a crucial role in L2 and translation teaching, two disciplines in which their use still lacks systematic investigation.

Body ares networks for human motor assessment

Healthcare, Human Computer Interfaces (HCI), Security and Biometry are the most promising application scenario directly involved in the Body Area Networks (BANs) evolution. Both wearable devices and sensors directly integrated in garments envision a word in which each of us is supervised by an invisible assistant monitoring our health and daily-life activities. New opportunities are enabled because improvements in sensors miniaturization and transmission efficiency of the wireless protocols, that achieved the integration of high computational power aboard independent, energy-autonomous, small form factor devices. Application’s purposes are various: (I) data collection to achieve off-line knowledge discovery; (II) user notification of his/her activities or in case a danger occurs; (III) biofeedback rehabilitation; (IV) remote alarm activation in case the subject need assistance; (V) introduction of a more natural interaction with the surrounding computerized environment; (VI) users identification by physiological or behavioral characteristics. Telemedicine and mHealth [1] are two of the leading concepts directly related to healthcare. The capability to borne unobtrusiveness objects supports users’ autonomy. A new sense of freedom is shown to the user, not only supported by a psychological help but a real safety improvement. Furthermore, medical community aims the introduction of new devices to innovate patient treatments. In particular, the extension of the ambulatory analysis in the real life scenario by proving continuous acquisition. The wide diffusion of emerging wellness portable equipment extended the usability of wearable devices also for fitness and training by monitoring user performance on the working task. The learning of the right execution techniques related to work, sport, music can be supported by an electronic trainer furnishing the adequate aid. HCIs made real the concept of Ubiquitous, Pervasive Computing and Calm Technology introduced in the 1988 by Marc Weiser and John Seeley Brown. They promotes the creation of pervasive environments, enhancing the human experience. Context aware, adaptive and proactive environments serve and help people by becoming sensitive and reactive to their presence, since electronics is ubiquitous and deployed everywhere. In this thesis we pay attention to the integration of all the aspects involved in a BAN development. Starting from the choice of sensors we design the node, configure the radio network, implement real-time data analysis and provide a feedback to the user. We present algorithms to be implemented in wearable assistant for posture and gait analysis and to provide assistance on different walking conditions, preventing falls. Our aim, expressed by the idea to contribute at the development of a non proprietary solutions, driven us to integrate commercial and standard solutions in our devices. We use sensors available on the market and avoided to design specialized sensors in ASIC technologies. We employ standard radio protocol and open source projects when it was achieved. The specific contributions of the PhD research activities are presented and discussed in the following. • We have designed and build several wireless sensor node providing both sensing and actuator capability making the focus on the flexibility, small form factor and low power consumption. The key idea was to develop a simple and general purpose architecture for rapid analysis, prototyping and deployment of BAN solutions. Two different sensing units are integrated: kinematic (3D accelerometer and 3D gyroscopes) and kinetic (foot-floor contact pressure forces). Two kind of feedbacks were implemented: audio and vibrotactile. • Since the system built is a suitable platform for testing and measuring the features and the constraints of a sensor network (radio communication, network protocols, power consumption and autonomy), we made a comparison between Bluetooth and ZigBee performance in terms of throughput and energy efficiency. Test in the field evaluate the usability in the fall detection scenario. • To prove the flexibility of the architecture designed, we have implemented a wearable system for human posture rehabilitation. The application was developed in conjunction with biomedical engineers who provided the audio-algorithms to furnish a biofeedback to the user about his/her stability. • We explored off-line gait analysis of collected data, developing an algorithm to detect foot inclination in the sagittal plane, during walk. • In collaboration with the Wearable Lab – ETH, Zurich, we developed an algorithm to monitor the user during several walking condition where the user carry a load. The remainder of the thesis is organized as follows. Chapter I gives an overview about Body Area Networks (BANs), illustrating the relevant features of this technology and the key challenges still open. It concludes with a short list of the real solutions and prototypes proposed by academic research and manufacturers. The domain of the posture and gait analysis, the methodologies, and the technologies used to provide real-time feedback on detected events, are illustrated in Chapter II. The Chapter III and IV, respectively, shown BANs developed with the purpose to detect fall and monitor the gait taking advantage by two inertial measurement unit and baropodometric insoles. Chapter V reports an audio-biofeedback system to improve balance on the information provided by the use centre of mass. A walking assistant based on the KNN classifier to detect walking alteration on load carriage, is described in Chapter VI.

Bifidobacterium - Human Host Interaction: Role of Human Plasminogen

Bifidobacterium is an important genus of the human gastrointestinal microbiota, affecting several host physiological features. Despite the numerous Bifidobacterium related health-promoting activities, there is still a dearth of information about the molecular mechanisms at the basis of the interaction between this microorganism and the host. Bacterial surface associated proteins may play an important role in this interaction because of their ability to intervene with host molecules, as recently reported for the host protein plasminogen. Plasminogen is the zymogen of the trypsin-like serine protease plasmin, an enzyme with a broad substrate specificity. Aim of this thesis is to deepen the knowledge about the interaction between Bifidobacterium and the human plasminogen system and its role in the Bifidobacterium-host interaction process. As a bifidobacterial model, B. animalis subsp. lactis BI07 has been used because of its large usage in dairy and pharmaceutical preparations. We started from the molecular characterization of the interaction between plasminogen and one bifidobacterial plasminogen receptor, DnaK, a cell wall protein showing high affinity for plasminogen, and went on with the study of the impact of intestinal environmental factors, such as bile salts and inflammation, on the plasminogen-mediated Bifidobacterium-host interaction. According to our in vitro findings, by enhancing the activation of the bifidobacterial bound plasminogen to plasmin, the host inflammatory response results in the decrease of the bifidobacterial adhesion to the host enterocytes, favouring bacterial migration to the luminal compartment. Conversely, in the absence of inflammation, plasminogen acts as a molecular bridge between host enterocytes and bifidobacteria, enhancing Bifidobacterium adhesion. Furthermore, adaptation to physiological concentrations of bile salts enhances the capability of this microorganism to interact with the host plasminogen system. The host plasminogen system thus represents an important and flexible tool used by bifidobacteria in the cross-talk with the host.

Design, development and first evaluation of a client/server system for managing and querying linguistic corpora

This thesis is concerned with the role played by software tools in the analysis and dissemination of linguistic corpora and their contribution to a more widespread adoption of corpora in different fields. Chapter 1 contains an overview of some of the most relevant corpus analysis tools available today, presenting their most interesting features and some of their drawbacks. Chapter 2 begins with an explanation of the reasons why none of the available tools appear to satisfy the requirements of the user community and then continues with technical overview of the current status of the new system developed as part of this work. This presentation is followed by highlights of features that make the system appealing to users and corpus builders (i.e. scholars willing to make their corpora available to the public). The chapter concludes with an indication of future directions for the projects and information on the current availability of the software. Chapter 3 describes the design of an experiment devised to evaluate the usability of the new system in comparison to another corpus tool. Usage of the tool was tested in the context of a documentation task performed on a real assignment during a translation class in a master's degree course. In chapter 4 the findings of the experiment are presented on two levels of analysis: firstly a discussion on how participants interacted with and evaluated the two corpus tools in terms of interface and interaction design, usability and perceived ease of use. Then an analysis follows of how users interacted with corpora to complete the task and what kind of queries they submitted. Finally, some general conclusions are drawn and areas for future work are outlined.

Development of control-oriented models of Dual Clutch Transmission systems

A control-oriented model of a Dual Clutch Transmission was developed for real-time Hardware In the Loop (HIL) applications, to support model-based development of the DCT controller. The model is an innovative attempt to reproduce the fast dynamics of the actuation system while maintaining a step size large enough for real-time applications. The model comprehends a detailed physical description of hydraulic circuit, clutches, synchronizers and gears, and simplified vehicle and internal combustion engine sub-models. As the oil circulating in the system has a large bulk modulus, the pressure dynamics are very fast, possibly causing instability in a real-time simulation; the same challenge involves the servo valves dynamics, due to the very small masses of the moving elements. Therefore, the hydraulic circuit model has been modified and simplified without losing physical validity, in order to adapt it to the real-time simulation requirements. The results of offline simulations have been compared to on-board measurements to verify the validity of the developed model, that was then implemented in a HIL system and connected to the TCU (Transmission Control Unit). Several tests have been performed: electrical failure tests on sensors and actuators, hydraulic and mechanical failure tests on hydraulic valves, clutches and synchronizers, and application tests comprehending all the main features of the control performed by the TCU. Being based on physical laws, in every condition the model simulates a plausible reaction of the system. The first intensive use of the HIL application led to the validation of the new safety strategies implemented inside the TCU software. A test automation procedure has been developed to permit the execution of a pattern of tests without the interaction of the user; fully repeatable tests can be performed for non-regression verification, allowing the testing of new software releases in fully automatic mode.

Nanoscale surface properties and interaction with fundamental biomolecules of chlorite and phlogopite

The surface properties of minerals have important implications in geology, environment, industry and biotechnology and for certain aspects in the research on the origin of life. This research project aims to widen the knowledge on the nanoscale surface properties of chlorite and phlogopite by means of advanced methodologies, and also to investigate the interaction of fundamental biomolecules, such as nucleotides, RNA, DNA and amino acid glycine with the surface of the selected phyllosilicates. Multiple advanced and complex experimental approaches based on scanning probe microscopy and spatially resolved spectroscopy were used and in some cases specifically developed. The results demonstrate that chlorite exposes at the surface atomically flat terraces with 0.5 nm steps typically generated by the fragmentation of the octahedral sheet of the interlayer (brucitic-type). This fragmentation at the nanoscale generates a high anisotropy and inhomogeneity with surface type and isomorphous cationic substitutions determining variations of the effective surface potential difference, ranging between 50-100 mV and 400-500 mV, when measured in air, between the TOT surface and the interlayer brucitic sheet. The surface potential was ascribed to be the driving force of the observed high affinity of the surface with the fundamental biomolecules, like single molecules of nucleotides, DNA, RNA and amino acids. Phlogopite was also observed to present an extended atomically flat surface, featuring negative surface potential values of some hundreds of millivolts and no significant local variations. Phlogopite surface was sometimes observed to present curvature features that may be ascribed to local substitutions of the interlayer cations or the presence of a crystal lattice mismatch or structural defects, such as stacking faults or dislocation loops. Surface chemistry was found similar to the bulk. The study of the interaction with nucleotides and glycine revealed a lower affinity with respect to the brucite-like surface of chlorite.

Non-Covalent Interaction: Revealed by Rotational Spectroscopy

The pulsed jet Fourier transform microwave spectroscopy have been applied to several molecular complexes involving H2O, freons, methane, carboxylic acids, and rare gas. The obtained results showcase the suitability of this technique for studying the intermolecular interactions. The rotational spectra of three water adducts of halogenated organic molecules, i.e. chlorotrifluoroethylene, isoflurane and alfa,alfa,alfa,-trifluoroanisole, have been investigated. It has been found that, the halogenation of the partner molecules definitely changes the way in which water will link to the partner molecule. Quadrupole hyperfine structures and/or the tunneling splittings have been observed in the rotational spectra of difluoromethane-dichloromethane, chlorotrifluorometane-fluoromethane, difluoromethane-formaldehyde and trifluoromethane-benzene. These features have been useful to describe their intermolecular interactions (weak hydrogen bonds or halogen bonds), and to size the potential energy surfaces of their internal motions. The rotational spectrum of pyridine-methane pointed out that methane prefers to locate above the ring and link to pyridine through a C-H•••π weak hydrogen bond, rather than the C-H•••n interaction. This behavior, typical of complexes of pyridine with rare gases, suggests classifying CH4, in relation to its ability to form molecular complexes with aromatic molecules, as a pseudo rare gas. The conformational equilibria of three bi-molecules of carboxylic acids, acrylic acid-trifluoroacetic acid, difluoroacetic acid-formic acid and acrylic acid-fluoroacetic acid have been studied. The increase of the hydrogen bond length upon H→D isotopic substitution (Ubbelohde effect) has been deduced from the elongation of the carboxylic carbons C•••C distance. The van der Waals complex tetrahydrofuran-krypton shows that the systematic doubling of the rotational lines has been attributed to the residual pseudo-rotation of tetrahydrofuran in the complex, based on the values of the Coriolis coupling constants, and on the type (mu_b) of the interstate transitions.

Analysis of the immunological and functional features of the Neisserial Heparin Binding Antigen (NHBA)

Neisserial Heparin Binding Antigen (NHBA) is a surface-exposed lipoprotein ubiquitously expressed by genetically diverse Neisseria meningitidis strains and is an antigen of the multicomponent protein-based 4CMenB vaccine, able to induce bactericidal antibodies in humans and to bind heparin-like molecules. The aim of this study is to characterize the immunological and functional properties of NHBA. To evaluate immunogenicity and the contribution of aminoacid sequence variability to vaccine coverage, we constructed recombinant isogenic strains that are susceptible to bactericidal killing only by anti-NHBA antibodies and engineered them to express equal levels of selected NHBA peptides. In these recombinant strains, we observed different titres associated with the different peptide variants. These recombinant strains were then further engineered to express NHBA chimeric proteins to investigate the regions important for immunogenicity. In natural strains, anti-NHBA antibodies were found to be cross-protective against strains expressing different peptides. To investigate the functional properties of this antigen, the recombinant purified NHBA protein was tested in in vitro binding studies and was found to be able to bind epithelial cells. The binding was abolished when cells were treated specifically with heparinase III, suggesting that the interaction with the cells is mediated by heparan sulfate proteoglycans (HSPG). Mutation of the Arg-rich tract of NHBA abrogated the binding, confirming the importance of this region in mediating the binding to heparin-like molecules. In a panel of N. meningitidis strains, the deletion of nhba resulted in a reduction of adhesion with respect to each isogenic wild type strain. Furthermore, the adhesion of the wild-type strain was prevented by using anti-NHBA polyclonal sera, demonstrating the specificity of the interaction. These results suggest that NHBA could be a novel meningococcal adhesin contributing to host-cell interaction. Moreover, we analysed NHBA NalP-mediated cleavage in different NHBA peptides and showed that not all NHBA peptides are cleaved.

Evaluation of 3D cell culture systems for host-pathogen interaction studies

Traditional cell culture models have limitations in extrapolating functional mechanisms that underlie strategies of microbial virulence. Indeed during the infection the pathogens adapt to different tissue-specific environmental factors. The development of in vitro models resembling human tissue physiology might allow the replacement of inaccurate or aberrant animal models. Three-dimensional (3D) cell culture systems are more reliable and more predictive models that can be used for the meaningful dissection of host–pathogen interactions. The lung and gut mucosae often represent the first site of exposure to pathogens and provide a physical barrier against their entry. Within this context, the tracheobronchial and small intestine tract were modelled by tissue engineering approach. The main work was focused on the development and the extensive characterization of a human organotypic airway model, based on a mechanically supported co-culture of normal primary cells. The regained morphological features, the retrieved environmental factors and the presence of specific epithelial subsets resembled the native tissue organization. In addition, the respiratory model enabled the modular insertion of interesting cell types, such as innate immune cells or multipotent stromal cells, showing a functional ability to release pertinent cytokines differentially. Furthermore this model responded imitating known events occurring during the infection by Non-typeable H. influenzae. Epithelial organoid models, mimicking the small intestine tract, were used for a different explorative analysis of tissue-toxicity. Further experiments led to detection of a cell population targeted by C. difficile Toxin A and suggested a role in the impairment of the epithelial homeostasis by the bacterial virulence machinery. The described cell-centered strategy can afford critical insights in the evaluation of the host defence and pathogenic mechanisms. The application of these two models may provide an informing step that more coherently defines relevant molecular interactions happening during the infection.