Fiabilidad en la observación en fútbol sala a través de una herramienta de evaluación de los deportes de equipo (Team Sport Assessment Procedure)

[ES] El objeto de esta investigación es la obtención de parámetros de fiabilidad a partir de la aplicación de la herramienta validada Team Sport Assessment Procedure (TSAP).

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.

Architectures and design patterns for functional design of logic control and diagnostics in industrial automation

Recently in most of the industrial automation process an ever increasing degree of automation has been observed. This increasing is motivated by the higher requirement of systems with great performance in terms of quality of products/services generated, productivity, efficiency and low costs in the design, realization and maintenance. This trend in the growth of complex automation systems is rapidly spreading over automated manufacturing systems (AMS), where the integration of the mechanical and electronic technology, typical of the Mechatronics, is merging with other technologies such as Informatics and the communication networks. An AMS is a very complex system that can be thought constituted by a set of flexible working stations, one or more transportation systems. To understand how this machine are important in our society let considerate that every day most of us use bottles of water or soda, buy product in box like food or cigarets and so on. Another important consideration from its complexity derive from the fact that the the consortium of machine producers has estimated around 350 types of manufacturing machine. A large number of manufacturing machine industry are presented in Italy and notably packaging machine industry,in particular a great concentration of this kind of industry is located in Bologna area; for this reason the Bologna area is called “packaging valley”. Usually, the various parts of the AMS interact among them in a concurrent and asynchronous way, and coordinate the parts of the machine to obtain a desiderated overall behaviour is an hard task. Often, this is the case in large scale systems, organized in a modular and distributed manner. Even if the success of a modern AMS from a functional and behavioural point of view is still to attribute to the design choices operated in the definition of the mechanical structure and electrical electronic architecture, the system that governs the control of the plant is becoming crucial, because of the large number of duties associated to it. Apart from the activity inherent to the automation of themachine cycles, the supervisory system is called to perform other main functions such as: emulating the behaviour of traditional mechanical members thus allowing a drastic constructive simplification of the machine and a crucial functional flexibility; dynamically adapting the control strategies according to the different productive needs and to the different operational scenarios; obtaining a high quality of the final product through the verification of the correctness of the processing; addressing the operator devoted to themachine to promptly and carefully take the actions devoted to establish or restore the optimal operating conditions; managing in real time information on diagnostics, as a support of the maintenance operations of the machine. The kind of facilities that designers can directly find on themarket, in terms of software component libraries provides in fact an adequate support as regard the implementation of either top-level or bottom-level functionalities, typically pertaining to the domains of user-friendly HMIs, closed-loop regulation and motion control, fieldbus-based interconnection of remote smart devices. What is still lacking is a reference framework comprising a comprehensive set of highly reusable logic control components that, focussing on the cross-cutting functionalities characterizing the automation domain, may help the designers in the process of modelling and structuring their applications according to the specific needs. Historically, the design and verification process for complex automated industrial systems is performed in empirical way, without a clear distinction between functional and technological-implementation concepts and without a systematic method to organically deal with the complete system. Traditionally, in the field of analog and digital control design and verification through formal and simulation tools have been adopted since a long time ago, at least for multivariable and/or nonlinear controllers for complex time-driven dynamics as in the fields of vehicles, aircrafts, robots, electric drives and complex power electronics equipments. Moving to the field of logic control, typical for industrial manufacturing automation, the design and verification process is approached in a completely different way, usually very “unstructured”. No clear distinction between functions and implementations, between functional architectures and technological architectures and platforms is considered. Probably this difference is due to the different “dynamical framework”of logic control with respect to analog/digital control. As a matter of facts, in logic control discrete-events dynamics replace time-driven dynamics; hence most of the formal and mathematical tools of analog/digital control cannot be directly migrated to logic control to enlighten the distinction between functions and implementations. In addition, in the common view of application technicians, logic control design is strictly connected to the adopted implementation technology (relays in the past, software nowadays), leading again to a deep confusion among functional view and technological view. In Industrial automation software engineering, concepts as modularity, encapsulation, composability and reusability are strongly emphasized and profitably realized in the so-calledobject-oriented methodologies. Industrial automation is receiving lately this approach, as testified by some IEC standards IEC 611313, IEC 61499 which have been considered in commercial products only recently. On the other hand, in the scientific and technical literature many contributions have been already proposed to establish a suitable modelling framework for industrial automation. During last years it was possible to note a considerable growth in the exploitation of innovative concepts and technologies from ICT world in industrial automation systems. For what concerns the logic control design, Model Based Design (MBD) is being imported in industrial automation from software engineering field. Another key-point in industrial automated systems is the growth of requirements in terms of availability, reliability and safety for technological systems. In other words, the control system should not only deal with the nominal behaviour, but should also deal with other important duties, such as diagnosis and faults isolations, recovery and safety management. Indeed, together with high performance, in complex systems fault occurrences increase. This is a consequence of the fact that, as it typically occurs in reliable mechatronic systems, in complex systems such as AMS, together with reliable mechanical elements, an increasing number of electronic devices are also present, that are more vulnerable by their own nature. The diagnosis problem and the faults isolation in a generic dynamical system consists in the design of an elaboration unit that, appropriately processing the inputs and outputs of the dynamical system, is also capable of detecting incipient faults on the plant devices, reconfiguring the control system so as to guarantee satisfactory performance. The designer should be able to formally verify the product, certifying that, in its final implementation, it will perform itsrequired function guarantying the desired level of reliability and safety; the next step is that of preventing faults and eventually reconfiguring the control system so that faults are tolerated. On this topic an important improvement to formal verification of logic control, fault diagnosis and fault tolerant control results derive from Discrete Event Systems theory. The aimof this work is to define a design pattern and a control architecture to help the designer of control logic in industrial automated systems. The work starts with a brief discussion on main characteristics and description of industrial automated systems on Chapter 1. In Chapter 2 a survey on the state of the software engineering paradigm applied to industrial automation is discussed. Chapter 3 presentes a architecture for industrial automated systems based on the new concept of Generalized Actuator showing its benefits, while in Chapter 4 this architecture is refined using a novel entity, the Generalized Device in order to have a better reusability and modularity of the control logic. In Chapter 5 a new approach will be present based on Discrete Event Systems for the problemof software formal verification and an active fault tolerant control architecture using online diagnostic. Finally conclusive remarks and some ideas on new directions to explore are given. In Appendix A are briefly reported some concepts and results about Discrete Event Systems which should help the reader in understanding some crucial points in chapter 5; while in Appendix B an overview on the experimental testbed of the Laboratory of Automation of University of Bologna, is reported to validated the approach presented in chapter 3, chapter 4 and chapter 5. In Appendix C some components model used in chapter 5 for formal verification are reported.

Functional characterization of Streptococcus pyogenes pili

Group A Streptococcus is a Gram-positive human pathogen able to colonize both upper respiratory tract and skin. GAS is responsible for several acute diseases and autoimmune sequelae that account for half a million deaths worldwide every year (Cunningham et al., 2000). As other bacteria, GAS infections requires the capacity of the pathogen to adhere to host tissues and to form cell aggregates. The ability to persist in distinct host niches like the throat and the skin and to trigger infections is associated with the expression of different GAS virulence factors. GAS pili has been described as important virulence factors encoded by different FCT-operon regions. Based on this information, we decided to study the possible effect of environmental conditions that could regulate the pili expression. In this study we reported the influence of pH environment variations in biofilm formation for strains pertaining to a panel of different GAS FCT-types. The biofilm formation was promoted, excepted in the FCT-1 strains, by a changing in pH from physiological to acidic condition of growth in in vitro biofilm assay. By analyzing the possible association between biofilm formation and pH dependence, we have found that in FCT-2 and FCT-3 strains, the biofilm is promoted by pH reduction leading to an increase of pili expression. These data confirmed a direct link between pH dependent pilus expression and biofilm formation in GAS. As pili are a multi component structure we decided to investigate the functional role of one of its subunits, the AP-1 protein. AP-1 is highly conserved through the different FCT-types and suggests a possible essential role for the pili function. We focused our attention on the AP-1 protein encoded by the FCT-1 strains (M6). In particular this AP-1 protein contains the von Willebrand Factor A (VWFA) domain, which share an homology with the human VWFA domain that has been reported to be involved in adhesion process. We have demonstrated that the AP-1 protein binds to human epithelial cells by its VWFA domain, whereas the biofilm formation is mediated by the N-terminal region of AP-1 protein. Moreover, analyzing the importance of AP-1 in in vivo experiments we found a major capacity of tissue dissemination for the wild-type strain compared to the isogenic AP-1 deletion mutant. Pili have been also reported as potential vaccine candidates against Gram positive bacteria. For these reason we decided to investigate the relationship between cross reaction of sera raised against different GAS and GBS pilin subunits and the presence of a conserved Cna_B domain, in different pilin components. Our idea was to investigate if, using pilus conserved domains, a broad coverage vaccine against streptococcal infection could be possible.

Das neue digitale ‚Shakespeare-Bildarchiv Oppel-Hammerschmidt‘ an der Universitätsbibliothek Mainz : Reden und Beiträge anlässlich seiner öffentlichen Vorstellung am 17. November 2008 an der Johannes Gutenberg-Universität Mainz

On the basis of illustrations of Shakespeare's Hamlet, the new digital 'Oppel-Hammerschmidt Shakespeare Illustration Archive' at the Mainz University Library - together with a lavishly-constructed and multiply-linked Web interface version - was presented to the public on 17 November 2008. This e-book, edited by Andreas Anderhub and Hildegard Hammerschmidt-Hummel, contains the speeches and presentations given on the occasion of the opening ceremony of the electronic archive. The collection of the new archive, published here for the first time, holds about 3,500 images and is part of the only Shakespeare illustration archive in the world. The Shakespeare Illustration Archive was founded in 1946 by the internationally acclaimed Shakespeare and Goethe scholar, Prof. Horst Oppel. This part of the archive was donated to the Mainz University Library on condition that its holdings be digitalised and made available to the public. The collection has been named 'The Oppel-Hammerschmidt Shakespeare Illustration Archive' in accordance with the terms of the Agreement of Donation of 9, 15, and 16 September 2005, and honouring the 16 March 1988 Delegation of Authority and Declaration of Intent by Frau Ingeborg Oppel, Prof. Oppel's widow and legal assignee. Vice-President Prof. Jürgen Oldenstein opened the proceedings by noting that 2008 had been a good year for international Shakespeare scholarship. For, in London, the site of the 'Theatre' in Shoreditch, where Shakespeare's company performed, had been unearthed, and in Mainz the Shakespeare Archive had gone online with thousands of illustrations. The Dean of the Faculty of Philosophy and Philology, Prof. Mechthild Dreyer, who mentioned that she herself had long been successfully employing interdisciplinary research methods, took particular pleasure in the transdisciplinary approach to research resolutely pursued by Prof. Hammerschmidt-Hummel. Prof. Clemens Zintzen (Cologne), former President of the Mainz Academy of Literature and Sciences, recalled highlights from the more than sixty-year-long history of the Shakespeare Illustration Archive. Prof. Kurt Otten (Heidelberg and Cambridge) drew an impressive portrait of Horst Oppel's personality as an academic and praised his influential books on Goethe and Shakespeare. He pointed out that Oppel's Shakespeare Illustration Archive, the basis for many a dissertation, had enjoyed great popularity around the world. Prof. Otten also delineated the academic career of Prof. Hammerschmidt-Hummel and her new findings regarding Shakespeare's time, life and work. Prof. Rüdiger Ahrens OBE (Würzburg) drew attention to Prof. Hammerschmidt-Hummel's research results, directly or indirectly arising out of her work on the Shakespeare Illustration Archive. This research had centred on proving the authenticity of four visual representations of Shakespeare (the Chandos and Flower portraits, the Davenant bust and the Darmstadt Shakespeare death mask); solving the mystery around Shakespeare's 'Dark Lady'; and establishing the dramatist's Catholic religion. Prof. Hammerschmidt-Hummel reported on her 'Shakespeare Illustration' project, describing the nature, dimensions and significance of the Archive's pictorial material, which relates to all of Shakespeare's plays and stretches over five centuries. She explained that the digital 'Oppel-Hammerschmidt Illustration Archive' was an addition to the three-volume edition she had compiled, authored and edited for publication in 2003. Unlike the print version, however, the digital collection had only been partly editorially prepared. It represented source material and a basis for further work. Hammerschmidt-Hummel expressed her thanks to the Head of the Central University Library, Dr Andreas Anderhub, for his untiring commitment. After the initial donation had been made, he had entered enthusiastically into setting up the necessary contacts, getting all the work underway, and clearing the legal hurdles. Hammerschmidt-Hummel was especially grateful to University of Mainz librarian Heike Geisel, who had worked for nearly five years to carry out the large-scale digitalization of a total of 8,800 items. Frau Geisel was also extremely resourceful in devising ways of making the collection yield even more, e.g. by classifying and cross-linking the data, assembling clusters of individual topics that lend themselves to research, and (in collaboration with the art historian Dr Klaus Weber) making the archive's index of artists compatible with the data-bank of artists held by the University of Mainz Institute of Art History. In addition, she compiled an extremely helpful 'users' guide' to the new digital collection. Frau Geisel had enjoyed invaluable support from Dr Annette Holzapfel-Pschorn, the leading academic in the Central IT Department at the University, who set up an intelligent, most impressive Web interface using the latest application technologies. Frau Geisel and Dr Holzapfel-Pschorn were highly praised for their convincing demonstration, using illustrations to Hamlet, of how to access this well-devised and exceptionally user-friendly Web version. For legal reasons, Prof. Hammerschmidt-Hummel pointed out, the collection could not be released for open access on the internet. The media - as Dr Anderhub stressed in his foreword - had shown great interest in the new digital collection of thousands of Shakespearean illustrations (cf. Benjamin Cor's TV feature in "Tagesthemen", 17 November 2008, presented by Tom Buhrow). The ‘Oppel-Hammerschmidt Shakespeare Illustration Archive’ should also meet with particular interest not only among academic specialists, but also among the performers of the arts and persons active in the cultural realm in general, as well as theatre and film directors, literary managers, teachers, and countless Shakespeare enthusiasts.

Strategic decision making in international firms: effect of top management team internationalization on international strategic decision process

In this research project, I have integrated two research streams on international strategic decisions making in international firms: upper echelons or top management teams (TMT) internationalization research and international strategic decision making process research. Both research streams in international business literature have evolved independently, but there is a potential in combining these two streams of research. The first empirical paper “TMT internationalization and international strategic decision making process: a decision level analysis of rationality, speed, and performance” explores the influence of TMT internationalization on strategic decision rationality and speed and, subsequently, their effect on international strategic decision effectiveness (performance). The results show that the internationalization of TMT is positively related to decision effectiveness and this relationship is mediated by decision rationality while the hypotheses regarding the association between TMT internationalization and decision speed, and the mediating effect of speed were not supported. The second paper “TMT internationalization and international strategic decision rationality: the mediating role of international information” of my thesis is a simple but logical extension of first paper. The first paper showed that TMT Internationalization has a significant positive effect on international strategic decision rationality. The second paper explicitly showed that TMT internationalization affect on international strategic decision rationality comes from two sources: international experience (personal international knowledge and information) and international information collected from managerial international contacts. For this research project, I have collected data from international software firms in Pakistan. My research contributes to the literature on upper echelons theory and strategic decision making in context of international business and international firms by explicitly examining the link between TMT internationalization and characteristics of strategic decisions making process (i.e. rationality and speed) in international firms and their possible mediating effect on performance.

Measurement of the e + e - pi + pi - cross section using initial state radiation at BESIII

The future goal of modern physics is the discovery of physics beyond the Standard Model. One of the most significant hints for New Physics can be seen in the anomalous magnetic moment of the muon - one of the most precise measured variables in modern physics and the main motivation of this work. This variable is associated with the coupling of the muon, an elementary particle, to an external electromagnetic field and is defined as a = (g - 2)/2, whereas g is the gyromagnetic factor of the muon. The muon anomaly has been measured with a relative accuracy of 0.5·10-6. However, a difference between the direct measurement and the Standard Model prediction of 3.6 standard deviations can be observed. This could be a hint for the existence of New Physics. Unfortunately, it is, yet, not significant enough to claim an observation and, thus, more precise measurements and calculations have to be performed.rnThe muon anomaly has three contributions, whereas the ones from quantum electrodynamics and weak interaction can be determined from perturbative calculations. This cannot be done in case of the hadronic contributions at low energies. The leading order contribution - the hadronic vacuum polarization - can be computed via a dispersion integral, which needs as input hadronic cross section measurements from electron-positron annihilations. Hence, it is essential for a precise prediction of the muon anomaly to measure these hadronic cross sections, σ(e+e-→hadrons), with high accuracy. With a contribution of more than 70%, the final state containing two charged pions is the most important one in this context.rnIn this thesis, a new measurement of the σ(e+e-→π+π-) cross section and the pion form factor is performed with an accuracy of 0.9% in the dominant ρ(770) resonance region between 600 and rn900 MeV at the BESIII experiment. The two-pion contribution to the leading-order (LO) hadronic vacuum polarization contribution to (g - 2) from the BESIII result, obtained in this work, is computed to be a(ππ,LO,600-900 MeV) = (368.2±2.5stat±3.3sys)·10-10. With the result presented in this thesis, we make an important contribution on the way to solve the (g - 2) puzzle.

Progettazione di un applicativo di supporto al monitoraggio di team situati

Lo scopo della tesi e quello di giungere alla realizzazione di un prototipo, che si basi su tecnologie specifiche quali GPS, Android e Bluetooth, per l'infrastruttura di un sistema che può essere visto come l'unione di tre macro parti distinte, centrale di controllo, dispositivo mobile e pulsossimetro. Concentrandosi in particolare sugli ultimi due componenti citati e realizzando un sistema di comunicazione che si basa su un Web Service ispirato al modello REST, si giungerà, attraverso un attento processo logico dettato dai canoni dell'ingegneria del software, al prototipo finale. Il prototipo che sarà realizzato rappresenterà oltre che un primo sistema funzionante e operativo, un punto di partenza per estensioni future, con lo scopo di perfezionare le funzionalità già esistenti o di fornirne di aggiuntive.

Sviluppo di applicazioni mobile Cross-Platform: Flutter come caso di studio

L’obiettivo dell'elaborato è quello di dare una panoramica sullo stato dell'arte riguardo lo sviluppo di applicazioni mobile, descrivendo i vantaggi e gli svantaggi degli approcci nativo e cross-platform, ed analizzare un framework creato dal team Dart di Google per sviluppare applicazioni cross-platform per le piattaforme Android e iOS chiamato Flutter. Il framework Flutter verrà analizzato mediante lo sviluppo di un’applicazione concreta, e successivamente confrontato con la medesima app sviluppata utilizzando l’approccio nativo su piattaforma Android.

A multidisciplinary approach to the functional and esthetic rehabilitation of amelogenesis imperfecta and open bite deformity: a case report

The treatment of amelogenesis imperfecta (AI) with an anterior open bite (AOB) is a challenge for the clinician and often requires a multidisciplinary team of specialists. Most often, patients suffering from these conditions are young and a good functional and esthetic long-term result must be aspired. This clinical report illustrates the orthodontic, maxillofacial, restorative, and prosthodontic rehabilitation of a 20-year-old woman with a hypoplastic form of AI and an AOB malocclusion, having received treatment for the last 6 years. It included adhesive resin composite restorations, orthodontical and maxillofacial surgery with a one-piece Le Fort I osteotomy, and a genioplasty. Subsequent prosthodontic therapy consisted of 28 all-ceramic crowns whereby a solid interdigitation, a canine guidance, and consistent and regular contacts between tooth crowns could be achieved to assure a good functional and esthetic oral situation. The tooth preparation techniques guaranteed minimally invasive treatment. The patient was affected very positively. CLINICAL SIGNIFICANCE: This article describes an interdisciplinary approach to the successful treatment of a patient with a hypoplastic form of amelogenesis imperfecta over a period of 6 years. It starts with a discussion of the conservative steps taken during adolescence and concludes with the final prosthetic rehabilitation with all-ceramic crowns after reaching adulthood.