Interactive application in spanish sign language for a public transport environment

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

User interaction widgets for interactive theorem proving

Matita (that means pencil in Italian) is a new interactive theorem prover under development at the University of Bologna. When compared with state-of-the-art proof assistants, Matita presents both traditional and innovative aspects. The underlying calculus of the system, namely the Calculus of (Co)Inductive Constructions (CIC for short), is well-known and is used as the basis of another mainstream proof assistant—Coq—with which Matita is to some extent compatible. In the same spirit of several other systems, proof authoring is conducted by the user as a goal directed proof search, using a script for storing textual commands for the system. In the tradition of LCF, the proof language of Matita is procedural and relies on tactic and tacticals to proceed toward proof completion. The interaction paradigm offered to the user is based on the script management technique at the basis of the popularity of the Proof General generic interface for interactive theorem provers: while editing a script the user can move forth the execution point to deliver commands to the system, or back to retract (or “undo”) past commands. Matita has been developed from scratch in the past 8 years by several members of the Helm research group, this thesis author is one of such members. Matita is now a full-fledged proof assistant with a library of about 1.000 concepts. Several innovative solutions spun-off from this development effort. This thesis is about the design and implementation of some of those solutions, in particular those relevant for the topic of user interaction with theorem provers, and of which this thesis author was a major contributor. Joint work with other members of the research group is pointed out where needed. The main topics discussed in this thesis are briefly summarized below. Disambiguation. Most activities connected with interactive proving require the user to input mathematical formulae. Being mathematical notation ambiguous, parsing formulae typeset as mathematicians like to write down on paper is a challenging task; a challenge neglected by several theorem provers which usually prefer to fix an unambiguous input syntax. Exploiting features of the underlying calculus, Matita offers an efficient disambiguation engine which permit to type formulae in the familiar mathematical notation. Step-by-step tacticals. Tacticals are higher-order constructs used in proof scripts to combine tactics together. With tacticals scripts can be made shorter, readable, and more resilient to changes. Unfortunately they are de facto incompatible with state-of-the-art user interfaces based on script management. Such interfaces indeed do not permit to position the execution point inside complex tacticals, thus introducing a trade-off between the usefulness of structuring scripts and a tedious big step execution behavior during script replaying. In Matita we break this trade-off with tinycals: an alternative to a subset of LCF tacticals which can be evaluated in a more fine-grained manner. Extensible yet meaningful notation. Proof assistant users often face the need of creating new mathematical notation in order to ease the use of new concepts. The framework used in Matita for dealing with extensible notation both accounts for high quality bidimensional rendering of formulae (with the expressivity of MathMLPresentation) and provides meaningful notation, where presentational fragments are kept synchronized with semantic representation of terms. Using our approach interoperability with other systems can be achieved at the content level, and direct manipulation of formulae acting on their rendered forms is possible too. Publish/subscribe hints. Automation plays an important role in interactive proving as users like to delegate tedious proving sub-tasks to decision procedures or external reasoners. Exploiting the Web-friendliness of Matita we experimented with a broker and a network of web services (called tutors) which can try independently to complete open sub-goals of a proof, currently being authored in Matita. The user receives hints from the tutors on how to complete sub-goals and can interactively or automatically apply them to the current proof. Another innovative aspect of Matita, only marginally touched by this thesis, is the embedded content-based search engine Whelp which is exploited to various ends, from automatic theorem proving to avoiding duplicate work for the user. We also discuss the (potential) reusability in other systems of the widgets presented in this thesis and how we envisage the evolution of user interfaces for interactive theorem provers in the Web 2.0 era.

Interactive theorem provers: issues faced as a user and tackled as a developer

Interactive theorem provers (ITP for short) are tools whose final aim is to certify proofs written by human beings. To reach that objective they have to fill the gap between the high level language used by humans for communicating and reasoning about mathematics and the lower level language that a machine is able to “understand” and process. The user perceives this gap in terms of missing features or inefficiencies. The developer tries to accommodate the user requests without increasing the already high complexity of these applications. We believe that satisfactory solutions can only come from a strong synergy between users and developers. We devoted most part of our PHD designing and developing the Matita interactive theorem prover. The software was born in the computer science department of the University of Bologna as the result of composing together all the technologies developed by the HELM team (to which we belong) for the MoWGLI project. The MoWGLI project aimed at giving accessibility through the web to the libraries of formalised mathematics of various interactive theorem provers, taking Coq as the main test case. The motivations for giving life to a new ITP are: • study the architecture of these tools, with the aim of understanding the source of their complexity • exploit such a knowledge to experiment new solutions that, for backward compatibility reasons, would be hard (if not impossible) to test on a widely used system like Coq. Matita is based on the Curry-Howard isomorphism, adopting the Calculus of Inductive Constructions (CIC) as its logical foundation. Proof objects are thus, at some extent, compatible with the ones produced with the Coq ITP, that is itself able to import and process the ones generated using Matita. Although the systems have a lot in common, they share no code at all, and even most of the algorithmic solutions are different. The thesis is composed of two parts where we respectively describe our experience as a user and a developer of interactive provers. In particular, the first part is based on two different formalisation experiences: • our internship in the Mathematical Components team (INRIA), that is formalising the finite group theory required to attack the Feit Thompson Theorem. To tackle this result, giving an effective classification of finite groups of odd order, the team adopts the SSReflect Coq extension, developed by Georges Gonthier for the proof of the four colours theorem. • our collaboration at the D.A.M.A. Project, whose goal is the formalisation of abstract measure theory in Matita leading to a constructive proof of Lebesgue’s Dominated Convergence Theorem. The most notable issues we faced, analysed in this part of the thesis, are the following: the difficulties arising when using “black box” automation in large formalisations; the impossibility for a user (especially a newcomer) to master the context of a library of already formalised results; the uncomfortable big step execution of proof commands historically adopted in ITPs; the difficult encoding of mathematical structures with a notion of inheritance in a type theory without subtyping like CIC. In the second part of the manuscript many of these issues will be analysed with the looking glasses of an ITP developer, describing the solutions we adopted in the implementation of Matita to solve these problems: integrated searching facilities to assist the user in handling large libraries of formalised results; a small step execution semantic for proof commands; a flexible implementation of coercive subtyping allowing multiple inheritance with shared substructures; automatic tactics, integrated with the searching facilities, that generates proof commands (and not only proof objects, usually kept hidden to the user) one of which specifically designed to be user driven.

Automatic initialization for facial analysis in interactive robotics

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

Il cinema in missione. La pratica cinematografica dei missionari italiani lungo il XX secolo tra apostolato e antropologia

The thesis reconstructs the cinema’s experience of Italian missionaries during the XX century in a historical-pragmatic key. Italian missionaries, who started producing movies around the Twenties, have used cinema as a helpful instrument for religious propaganda. They have considered the rules of the Catholic Church, the political and social context and the audience’s expectations. Each chapter (1-4) analyses the phenomenon inside the context constituted by the Italian colonial experiences, the relationship between Catholic Church and images during the Evangelization, the history of cinema and the history of missions. A specific chapter (chapter 5) is dedicated to the archives of missionary’s cinema and to the value to be assigned to this film production (in terms of social memory and archive’s memory). At the end of the first part, the thesis presents a proposal about the relationship between missionary’s cinema and visual anthropology. The second part of the thesis includes the film cards of the missionary’s movies preserved in Italy: 339 cards of Italian movies and 149 cards of foreign movies placed in different archives and bureaus.

Arte/Cinema. Dinamismo futurista e extra artisticità dadaista

La ricerca ha bene analizzato lo stretto rapporto che si instaura fra le Avanguardie Storiche e le tecnologie più innovative dei primi anni del Novecento. Con il Futurismo (argomento trattato nel primo anno di ricerca di dottorato) e, in seguito, con il Dadaismo (principale soggetto di studio del secondo anno di ricerca), la candidata sottolinea i rapporti fra le avanguardie artistiche e la neonata tecnica cinematografica (1895). Il primo capitolo si concentra sugli enormi cambiamenti, sia materiali sia culturali, vissuti dalla nuova società di inizio Novecento. I principali concetti analizzati sono: i molteplici sviluppi tecnologici, la disputa teorica sul cinematografo che, tra il 1905 e il 1907, acquista maggiore rilevanza e la nuova “visione” della realtà. In particolare modo nel primo capitolo si affronta anche il dibattito culturale di fine Ottocento che contribuirà alle avanguardistiche affermazioni futuriste. L’idea di confrontare, in perfetta omologia, la nuova “visione” del cinema e le più importanti scoperte materiali del tempo è un interessante apporto a tutta la ricerca dove l’utilizzo del mezzo cinematografico diventa un mezzo perfetto per analizzare i flussi temporali, non più diacronici bensì sincronici dei fenomeni artistici. Inoltre, si sottolinea come la crescente convergenza fra differenti forme artistiche e il cinema d’avanguardia diventino uno strumento culturale capace di aprire nuovi universi e prospettive. E’ con il Futurismo che si inizia a parlare di contaminazioni fra differenti mezzi di espressione non necessariamente legati alla “rappresentazione” pittorica o scultorea. E’ invece il movimento Dadaista a sviluppare il discorso iniziato dai Futuristi e a concretizzare il binomio arte/cinema al fine di condividere il tempo della registrazione filmica e l’intenzione artistica degli autori presi in esame. Una parte importante del lavoro è stata l’analisi e lo studio dei materiali filmici recuperati sia in ambito futurista sia in ambito dadaista. La stesura di un approfondito indice ragionato ha permesso importanti chiarimenti sull’argomento trattato. La ricerca predisposta dalla candidata si è avvalsa di strumenti metodologici differenti con l’intento di far emergere il complesso degli interventi dei principali artisti operanti all’interno dei due movimenti presi in esame, tracciandone le omologie con le principali innovazioni tecnologiche.