People semantic description and re-identification from point cloud geometry

The automatic extraction of biometric descriptors of anonymous people is a challenging scenario in camera networks. This task is typically accomplished making use of visual information. Calibrated RGBD sensors make possible the extraction of point cloud information. We present a novel approach for people semantic description and re-identification using the individual point cloud information. The proposal combines the use of simple geometric features with point cloud features based on surface normals.

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.

Semantic-based middleware solutions to support context-aware service provisioning in pervasive environments

The dynamicity and heterogeneity that characterize pervasive environments raise new challenges in the design of mobile middleware. Pervasive environments are characterized by a significant degree of heterogeneity, variability, and dynamicity that conventional middleware solutions are not able to adequately manage. Originally designed for use in a relatively static context, such middleware systems tend to hide low-level details to provide applications with a transparent view on the underlying execution platform. In mobile environments, however, the context is extremely dynamic and cannot be managed by a priori assumptions. Novel middleware should therefore support mobile computing applications in the task of adapting their behavior to frequent changes in the execution context, that is, it should become context-aware. In particular, this thesis has identified the following key requirements for novel context-aware middleware that existing solutions do not fulfil yet. (i) Middleware solutions should support interoperability between possibly unknown entities by providing expressive representation models that allow to describe interacting entities, their operating conditions and the surrounding world, i.e., their context, according to an unambiguous semantics. (ii) Middleware solutions should support distributed applications in the task of reconfiguring and adapting their behavior/results to ongoing context changes. (iii) Context-aware middleware support should be deployed on heterogeneous devices under variable operating conditions, such as different user needs, application requirements, available connectivity and device computational capabilities, as well as changing environmental conditions. Our main claim is that the adoption of semantic metadata to represent context information and context-dependent adaptation strategies allows to build context-aware middleware suitable for all dynamically available portable devices. Semantic metadata provide powerful knowledge representation means to model even complex context information, and allow to perform automated reasoning to infer additional and/or more complex knowledge from available context data. In addition, we suggest that, by adopting proper configuration and deployment strategies, semantic support features can be provided to differentiated users and devices according to their specific needs and current context. This thesis has investigated novel design guidelines and implementation options for semantic-based context-aware middleware solutions targeted to pervasive environments. These guidelines have been applied to different application areas within pervasive computing that would particularly benefit from the exploitation of context. Common to all applications is the key role of context in enabling mobile users to personalize applications based on their needs and current situation. The main contributions of this thesis are (i) the definition of a metadata model to represent and reason about context, (ii) the definition of a model for the design and development of context-aware middleware based on semantic metadata, (iii) the design of three novel middleware architectures and the development of a prototypal implementation for each of these architectures, and (iv) the proposal of a viable approach to portability issues raised by the adoption of semantic support services in pervasive applications.

Innovative treatments for shelf-life extension of whole and fresh-cut fruit

Maintaining the postharvest quality of whole and fresh-cut fruit during storage and distribution is the major challenge facing fruit industry. For this purpose, industry adopt a wide range of technologies to enable extended shelf-life. Many factors can lead to loss of quality in fresh product, hence the common description of these products as ‘perishable’. As a consequence normal factors such as transpiration and respiration lead ultimately to water loss and senescence of the product. Fruits and vegetables are living commodities and their rate of respiration is of key importance to maintenance of quality. It has been commonly observed that the greater the respiration rate of a product, the shorter the shelf-life. The principal problem for fresh-cut fruit industries is the relative shorter shelf-life of minimally processed fruit (MPF) compared to intact product. This fact is strictly connected with the higher ethylene production of fruit tissue stimulated during fresh-cut processing (peeling, cutting, dipping). 1-Methylcyclopropene (1-MCP) is an inhibitor of ethylene action and several researches have shown its effectiveness on the inhibition of ripening and senescence incidence for intact fruit and consequently on their shelf-life extension. More recently 1-MCP treatment has been tested also for shelf-life extension of MPF but discordant results have been obtained. Considering that in some countries 1-MCP is already a commercial product registered for the use on a number of horticultural products, the main aim of this actual study was to enhance our understanding on the effects of 1-MCP treatment on the quality maintenance of whole and fresh-cut climacteric and non-climacteric fruit (apple, kiwifruit and pineapple). Concerning the effects of 1-MCP on whole fruit, was investigated the effects of a semi-commercial postharvest treatment with 1-MCP on the quality of Pink Lady apples as functions of fruit ripening stage, 1-MCP dose, storage time and also in combination with controlled atmospheres storage in order to better understand what is the relationship among these parameters and if is possible to maximize the 1-MCP treatment to meet the market/consumer needs and then in order to put in the market excellent fruit. To achieve this purpose an incomplete three-level three-factor design was adopted. During the storage were monitored several quality parameters: firmness, ripening index, ethylene and carbon dioxide production and were also performed a sensory evaluations after 6 month of storage. In this study the higher retention of firmness (at the end of storage) was achieved by applying the greatest 1-MCP concentration to fruits with the lowest maturity stage. This finding means that in these semi-commercial conditions we may considerate completely blocked the fruit softening. 1-MCP was able to delay also the ethylene and CO2 production and the maturity parameters (soluble solids content and total acidity). Only in some cases 1-MCP generate a synergistic effect with the CA storage. The results of sensory analyses indicated that, the 1-MCP treatment did not affect the sweetness and whole fruit flavour while had a little effect on the decreasing cut fruit flavour. On the contrary the treated apple was more sour, crisp, firm and juicy. The effects of some treatment (dipping and MAP) on the nutrient stability were also investigated showing that in this case study the adopted treatments did not have drastic effects on the antioxidant compounds on the contrary the dipping may enhance the total antioxidant activity by the accumulation of ascorbic acid on the apple cut surface. Results concerning the effects of 1-MCP in combination with MAP on the quality parameters behaviour of the kiwifruit were not always consistent and clear: in terms of colour maintenance, it seemed to have a synergistic effect with N2O MAP; as far as ripening index is concerned, 1-MCP had a preservative effect, but just for sample packed in air.

Internal Model Principle: extension to the switching case and applications

This thesis deals with a novel control approach based on the extension of the well-known Internal Model Principle to the case of periodic switched linear exosystems. This extension, inspired by power electronics applications, aims to provide an effective design method to robustly achieve the asymptotic tracking of periodic references with an infinite number of harmonics. In the first part of the thesis the basic components of the novel control scheme are described and preliminary results on stabilization are provided. In the second part, advanced control methods for two applications coming from the world high energy physics are presented.

Registrazione e replicazione di procedure Web con una Firefox Extension

In questo lavoro di tesi è stata sviluppata una Firefox Extension per la registrazione e la replicazione di procedure sul Web. Si tratterà a fondo l’ambiente tecnologico nel quale è stata sviluppata l’applicazione e il contesto in cui si inserisce una Firefox Extension. Illustreremo il problema che intendiamo risolvere con la nostra estensione,il contesto applicativo in cui si inserisce e riporteremo una serie di lavori correlati che cercano, con diversi approcci, di risolvere il nostro stesso problema. Illustreremo il lavoro trattando approfonditamente l’approccio da noi utilizzato, mostrandone i vantaggi e i limiti.

Eocene nappe tectonics and late Alpine extension in the Central Anatolide belt, western Turkey

Strukturgeologische Untersuchungen belegen, daß die Anatoliden der Westtürkei im Eozän durch die Plazierung der Kykladischen Blauschiefereinheit entlang einer durchbrechenden Überschiebung auf die Menderes-Decken unter grünschieferfaziellen Metamorphosebedingungen entstanden.Die kykladischen Blauschiefer in der Westtürkei enthalten Relikte eines prograden alpinen Gefüges (DA1), welches hochruckmetamorph von Disthen und Chloritoid poikiloblastisch überwachsen wurde. Dieses Mineralstadium dauerte noch während des Beginns des nachfolgenden Deformationsereignisses (DA2) an, welches durch NE-gerichtete Scherung und Dekompression charakterisiert ist. Die nachfolgende Deformation (DA3) war das erste Ereignis, das beide Einheiten, sowohl die kykladische Blauschifereinheit als auch die Menderes-Decken, gemeinsam erfaßte. Der Überschiebungskontakt zwischen der kykladischen Blauschiefereinheit und den Menderes-Decken ist eine DA3-Scherzone: die ‘Cycladic-Menderes Thrust’ (CMT). Entlang der CMT-Überschiebungsbahn wurden die kykladischen Blauschiefer gegen veschiedene Einheiten der MN plaziert. Die CMT steigt nach S zum strukturell Hangenden hin an und kann daher als eine durchbrechende Überschiebung entlang einer nach S ansteigenden Rampe betrachtet werden. In den kykladischen Blauschiefern überprägen DA3-Strukturen, die im Zusammenhang mit der CMT stehen, hochdruckmentamorphe Gefüge.In den Menderes-Decken, dem Liegenden der CMT, wird DA3 durch regional vebreitete Gefügeelemente dokumentiert, die im Zusammenhang mit S-gerichteten Schersinnindikatoren stehen. DA3-Gefüge haben die Decken intern deformiert und bilden jene Scherzonen, welche die Decken untereinander abgrenzen. In der Çine-Decke können granitische Gesteine in Orthogneise und Metagranite unterteilt werden. Die Deformationsgeschichte dieser Gesteine dokumentiert zwei Ereignisse. Ein frühes amphibolitfazielles Ereignis erfaßte nur die Orthogneise, in denen vorwiegend NE-SW orientierte Lineare und NE-gerichtete Schersinnindikatoren entstanden. Die jüngeren Metagranite wurden sowohl durch vereinzelte DA3-Scherzonen, als auch in einer großmaßstäblichen DA3-Scherzone am Südrand des Çine-Massivs deformiert. In DA3-Scherzonen sind die Lineare N-S orientiert und die zugehörigen Schersinnindikatoren zeigen S-gerichtete Scherung unter grünschieferfaziellen Bedingungen an. Diese grünschieferfaziellen Scherzonen überprägen die amphibolitfaziellen Gefüge in den Orthogneisen. Magmatische Zirkone aus einem Metagranit, der einen Orthogneiss mit Top-NE Gefügen durchschlägt, ergaben ein 207Pb/206Pb-Alter von 547,2±1,0 Ma. Dies deutet darauf hin, daß DPA proterozoischen Alters ist. Dies wird auch durch die Tatsache gestützt, daß triassische Granite in der Çine- und der Bozdag-Decke keine DPA-Gefüge zeigen. Die jüngeren Top-S-Gefüge sind wahrscheinlich zur gleichen Zeit entstanden wie die ältesten Gefüge der Bayindir-Decke.Das Fehlen von Hochdruck-Gefügen im Liegenden der CMT impliziert eine Exhumierung der kykladischen Blauschiefer von mehr ca. 35 km, bevor diese im Eozän auf die Menderes-Decken aufgeschoben wurden. Die substantiellen Unterschiede bezüglich in der tektonometamorphen Geschichte der kykladischen Blauschiefer und der Menderes-Decken widersprechen der Modellvorstellung eines lateral kontinuierlichen Orogengürtels, nach der die Menderes-Decken als östliche Fortsezung der kykladischen Blauschiefer angesehen werden.Die Analyse spröder spätalpiner Deformationsstrukturen und das regionale Muster mit Hilfe von Spaltspurdatierung modellierter Abkühlalter deuten darauf hin, daß die Struktur des Eozänen Deckenstapels durch miozäne bis rezente Kernkomplex-Bildung stark modifiziert wurde. Eine großmaßstäbliche Muldenstruktur im zentralen Teil der Anatoliden hat sich als Folge zweier symmetrisch angeordneter Detachment-Systeme von initial steilen zu heute flachen Orientierungen im Einflußbreich von ’Rolling Hinges’ gebildet. Die Detachment-Störungen begrenzen den ‘Central Menderes metamorphic core complex’ (CMCC). Das Muster der Apatit-Spaltspuralter belegt, daß die Bildung des CMCC im Miozän begann. Durch die Rück-Deformierung von parallel zur Foliation konstruierten Linien gleicher Abkühlalter kann gezeigt werden, daß die Aufwölbung im Liegenden der Detachments zur Entstehung der Muldenstruktur führte. Das hohe topographische Relief im Bereich des CMCC ist eine Folge der Detachment-Störungen, was darauf hindeutet daß der obere Mantel in den Prozeß mit einbezogen gewesen ist.

Semantic coordination tuple centres for eHealth Systems

In questa tesi partendo dai limiti sintattici dello scambio di Electronic Patient Records (EHRs), si arriva alla creazione di un framework che supporti lo scambio di informazioni semantiche. Il framework creato si chiama Semantic TuCSoN ed è una estensione di TuCSoN (Tuple Centres Spread over the Network). Semantic TuCSoN viene modellato per il contesto eHealth definendo gli agenti e le politiche di coordinamento atte allo scambio di EHR. Questo framework vine infine testa per verificarne le performance allo scopo di valutare un suo ulteriore utilizzo.

Semantic Enrichment of Scientific Documents with Semantic Lenses – Developing methodologies, tools and prototypes for their concrete use

Con questa dissertazione di tesi miro ad illustrare i risultati della mia ricerca nel campo del Semantic Publishing, consistenti nello sviluppo di un insieme di metodologie, strumenti e prototipi, uniti allo studio di un caso d‟uso concreto, finalizzati all‟applicazione ed alla focalizzazione di Lenti Semantiche (Semantic Lenses).

Conversione per il Semantic Web di dati Turistico-Culturali: il progetto QRPlaces - Semantic Events

Il progetto QRPlaces - Semantic Events, oggetto di questo lavoro, focalizza l’attenzione sull’analisi, la progettazione e l’implementazione di un sistema che sia in grado di modellare i dati, relativi a diversi eventi facenti parte del patrimonio turistico - culturale della Regione Emilia Romagna 1, rendendo evidenti i vantaggi associati ad una rappresentazione formale incentrata sulla Semantica. I dati turistico - culturali sono intesi in questo ambito sia come una rappresentazione di “qualcosa che accade in un certo punto ad un certo momento” (come ad esempio un concerto, una sagra, una raccolta fondi, una rappresentazione teatrale e quant’altro) sia come tradizioni e costumi che costituiscono il patrimonio turistico-culturale e a cui si fa spesso riferimento con il nome di “Cultural Heritage”. Essi hanno la caratteristica intrinseca di richiedere una conoscenza completa di diverse informa- zioni correlata, come informazioni di geo localizzazione relative al luogo fisico che ospita l’evento, dati biografici riferiti all’autore o al soggetto che è presente nell’evento piuttosto che riferirsi ad informazioni che descrivono nel dettaglio tutti gli oggetti, come teatri, cinema, compagnie teatrali che caratterizzano l’evento stesso. Una corretta rappresentazione della conoscenza ad essi legata richiede, pertanto, una modellazione in cui i dati possano essere interconnessi, rivelando un valore informativo che altrimenti resterebbe nascosto. Il lavoro svolto ha avuto lo scopo di realizzare un dataset rispondente alle caratteristiche tipiche del Semantic Web grazie al quale è stato possibile potenziare il circuito di comunicazione e informazione turistica QRPlaces 2. Nello specifico, attraverso la conversione ontologica di dati di vario genere relativi ad eventi dislocati nel territorio, e sfruttando i principi e le tecnologie del Linked Data, si è cercato di ottenere un modello informativo quanto più possibile correlato e arricchito da dati esterni. L’obiettivo finale è stato quello di ottenere una sorgente informativa di dati interconnessi non solo tra loro ma anche con quelli presenti in sorgenti esterne, dando vita ad un percorso di collegamenti in grado di evidenziare una ricchezza informativa utilizzabile per la creazione di valore aggiunto che altrimenti non sarebbe possibile ottenere. Questo aspetto è stato realizzato attraverso un’in- terfaccia di MashUp che utilizza come sorgente il dataset creato e tutti i collegamenti con la rete del Linked Data, in grado di reperire informazioni aggiuntive multi dominio.