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.

"Narrativa di frontiera". Fenomenologia di una forma aperta.

«Fiction of frontier». Phenomenology of an open form/voice. Francesco Giustini’s PhD dissertation fits into a genre of research usually neglected by the literary criticism which nevertheless is arousing much interest in recent years: the relationship between Literature and Space. In this context, the specific issue of his work consists in the category of the Frontier including its several implications for the XX century fiction. The preliminary step, at the beginning of the first section of the dissertation, is a semantic analysis: with precision, Giustini describes the meaning of the word “frontier” here declined in a multiplicity of cultural, political and geographical contexts, starting from the American frontier of the pioneers who headed for the West, to the exotic frontiers of the world, with whose the imperialistic colonization has come into contact; from the semi-uninhabited areas like deserts, highlands and virgin forests, to the ethnic frontiers between Indian and white people in South America, since the internal frontiers of the Countries like those ones between the District and the Capital City, the Centre and the Outskirts. In the next step, Giustini wants to focus on a real “ myth of the frontier”, able to nourish cultural and literary imagination. Indeed, the literature has told and chosen the frontier as the scenery for many stories; especially in the 20th Century it made the frontier a problematic space in the light of events and changes that have transformed the perception of space and our relationship with it. Therefore, the dissertation proposes a critical category, it traces the hallmarks of a specific literary phenomenon defined “ Fiction of the frontier” ,present in many literary traditions during the 20th Century. The term “Fiction” (not “Literature” or “Poetics”) does not define a genre but rather a “procedure”, focusing on a constant issue pointed out from the texts examined in this work : the strong call to the act of narration and to its oral traditions. The “Fiction of the Frontier” is perceived as an approach to the world, a way of watching and feeling the objects, an emotion that is lived and told through the story- a story where the narrator ,through his body and his voice, takes the rule of the witness. The following parts, that have an analytic style, are constructed on the basis of this theoretical and methodological reflection. The second section gives a wide range of examples into we can find the figure and the myth of the frontier through the textual analysis which range over several literary traditions. Starting from monographic chapters (Garcia Marquez, Callado, McCarthy), to the comparative reading of couples of texts (Calvino and Verga Llosa, Buzzati and Coetzee, Arguedas and Rulfo). The selection of texts is introduced so as to underline a particular aspect or a form of the frontier at every reading. This section is articulated into thematic voices which recall some actions that can be taken into the ambiguous and liminal space of the frontier (to communicate, to wait, to “trans-culturate”, to imagine, to live in, to not-live in). In this phenomenology, the frontier comes to the light as a physical and concrete element or as a cultural, imaginary, linguistic, ethnic and existential category. In the end, the third section is centered on a more defined and elaborated analysis of two authors, considered as fundamental for the comprehension of the “Fiction of the frontier”: Joseph Conrad and João Guimarães Rosa. Even if they are very different, being part of unlike literary traditions, these two authors show many connections which are pointed by the comparative analysis. Maybe Conrad is the first author that understand the feeling of the frontier , freeing himself from the adventure romance and from the exotic nineteenthcentury tradition. João Guimarães Rosa, in his turn, is the great narrator of Brazilian and South American frontier, he is the man of sertão and of endless spaces of the Centre of Brazil. His production is strongly linked to that one belonged to the author of Heart of Darkness.

Cooperative Wireless Networks for Localization

This thesis adresses the problem of localization, and analyzes its crucial aspects, within the context of cooperative WSNs. The three main issues discussed in the following are: network synchronization, position estimate and tracking. Time synchronization is a fundamental requirement for every network. In this context, a new approach based on the estimation theory is proposed to evaluate the ultimate performance limit in network time synchronization. In particular the lower bound on the variance of the average synchronization error in a fully connected network is derived by taking into account the statistical characterization of the Message Delivering Time (MDT) . Sensor network localization algorithms estimate the locations of sensors with initially unknown location information by using knowledge of the absolute positions of a few sensors and inter-sensor measurements such as distance and bearing measurements. Concerning this issue, i.e. the position estimate problem, two main contributions are given. The first is a new Semidefinite Programming (SDP) framework to analyze and solve the problem of flip-ambiguity that afflicts range-based network localization algorithms with incomplete ranging information. The occurrence of flip-ambiguous nodes and errors due to flip ambiguity is studied, then with this information a new SDP formulation of the localization problem is built. Finally a flip-ambiguity-robust network localization algorithm is derived and its performance is studied by Monte-Carlo simulations. The second contribution in the field of position estimate is about multihop networks. A multihop network is a network with a low degree of connectivity, in which couples of given any nodes, in order to communicate, they have to rely on one or more intermediate nodes (hops). Two new distance-based source localization algorithms, highly robust to distance overestimates, typically present in multihop networks, are presented and studied. The last point of this thesis discuss a new low-complexity tracking algorithm, inspired by the Fano’s sequential decoding algorithm for the position tracking of a user in a WLAN-based indoor localization system.

Strategy as a matter of beliefs: the recorded music industry reinventing itself by rethinking itself

Managerial and organizational cognition studies the ways cognitions of managers in groups, organizations and industries shape their strategies and actions. Cognitions refer to simplified representations of managers’ internal and external environments, necessary to cope with the rich, ambiguous information requirements that characterize strategy making. Despite the important achievements in the field, many unresolved puzzles remain as to this process, particular as to the cognitive factors that condition actors in framing a response to a discontinuity, how actors can change their models in the face of a discontinuity, and the reciprocal relation between cognition and action. I leverage on the recent case of the recorded music industry in the face of the digital technology to study these issues, through a strategy-oriented study of the way early response to the discontinuity was constructed and of the subsequent evolution of this response. Through a longitudinal historical and cognitive analysis of actions and cognitions at both the industry and firm-level during the period in which the response took place (1999-2010), I gain important insights on the way historical beliefs in the industry shaped early response to the digital disruption, on the role of outsiders in promoting change through renewed vision about important issues, and on the reciprocal relationship between cognitive and strategic change.

"Tracciature Digitali": la conoscenza nell'era informazionale

La specificità dell'acquisizione di contenuti attraverso le interfacce digitali condanna l'agente epistemico a un'interazione frammentata, insufficiente da un punto di vista computazionale, mnemonico e temporale, rispetto alla mole informazionale oggi accessibile attraverso una qualunque implementazione della relazione uomo-computer, e invalida l'applicabilità del modello standard di conoscenza, come credenza vera e giustificata, sconfessando il concetto di credenza razionalmente fondata, per formare la quale, sarebbe invece richiesto all'agente di poter disporre appunto di risorse concettuali, computazionali e temporali inaccessibili. La conseguenza è che l'agente, vincolato dalle limitazioni ontologiche tipiche dell'interazione con le interfacce culturali, si vede costretto a ripiegare su processi ambigui, arbitrari e spesso più casuali di quanto creda, di selezione e gestione delle informazioni che danno origine a veri e propri ibridi (alla Latour) epistemologici, fatti di sensazioni e output di programmi, credenze non fondate e bit di testimonianze indirette e di tutta una serie di relazioni umano-digitali che danno adito a rifuggire in una dimensione trascendente che trova nel sacro il suo più immediato ambito di attuazione. Tutto ciò premesso, il presente lavoro si occupa di costruire un nuovo paradigma epistemologico di conoscenza proposizionale ottenibile attraverso un'interfaccia digitale di acquisizione di contenuti, fondato sul nuovo concetto di Tracciatura Digitale, definito come un un processo di acquisizione digitale di un insieme di tracce, ossia meta-informazioni di natura testimoniale. Tale dispositivo, una volta riconosciuto come un processo di comunicazione di contenuti, si baserà sulla ricerca e selezione di meta-informazioni, cioè tracce, che consentiranno l'implementazione di approcci derivati dall'analisi decisionale in condizioni di razionalità limitata, approcci che, oltre ad essere quasi mai utilizzati in tale ambito, sono ontologicamente predisposti per una gestione dell'incertezza quale quella riscontrabile nell'istanziazione dell'ibrido informazionale e che, in determinate condizioni, potranno garantire l'agente sulla bontà epistemica del contenuto acquisito.

Tracce di cinefilia su Facebook

La mia tesi approfondisce le dinamiche della cinefilia su Facebook: quali relazioni s'instaurano tra lo spettatore cinefilo, e dunque il suo particolare sguardo, e la moltitudine di frammenti di cinema dispersi nella rete; come si sono modificati i rapporti, gli atteggiamenti, i processi di negoziazione, le abitudini e soprattutto i discorsi dei cinefili al cospetto di tracce di cinema sui social network e in particolare su Facebook. Inoltreprovo a dimostrare che la cinefilia è un'esperienza costitutivamente autobiografica, cui il web permette il perpetuare potenzialmente infinito della (auto)narrazione di sé.

Exploring the biofilm of Streptococcus agalactiae to identify virulence factors

Streptococcus agalactiae, also known as Group B Streptococcus (GBS) is the primary colonizer of the anogenital mucosa of up to 40% of healthy women and an important cause of invasive neonatal infections worldwide. Among the 10 known capsular serotypes, GBS type III accounts for 30-76% of the cases of neonatal meningitis. Biofilms are dense aggregates of surface-adherent microorganisms embedded in an exopolysaccharide matrix. Centers for Disease Control and Prevention estimate that 65% of human bacterial infections involve biofilms (Post et al., 2004). In recent years, the ability of GBS to form biofilm attracted attention for its possible role in fitness and/or virulence. Here, a new in vitro biofilm formation protocol was developed to guarantee more stringent conditions, to better discriminate between strong-, low- and non- biofilm forming strains and reduce ambiguous data interpretation. This protocol was applied to screen the in vitro biofilm formation ability of more than 350 GBS clinical isolates from pregnant women and neonatal infections belonging to different serotype, in relation to media composition and pH. The results showed the enhancement of GBS biofilm formation in acidic condition and identified a subset of isolates belonging to serotypes III and V that forms strong biofilms in these conditions. Interestingly, the best biofilm formers belonged to the serotype III hypervirulent clone ST-17.It was also found that pH 5.0 induces down-regulation of the capsule but that this reduction is not enough by itself to ensure biofilm formation. Moreover, the ability of proteinase K to strongly inhibit biofilm formation and to disaggregate mature biofilms suggested that proteins play an essential role in promoting GBS biofilm formation and contribute to the biofilm structural stability. Finally, a set of proteins potentially expressed during the GBS in vitro biofilm formation were identified by mass spectrometry.

Expériences du sacré et (dé)figurations du Christ. Artaud, Beckett, Pasolini

« Dieu est mort » proclame à l’envi le fou nietzschéen. C’est sous l’égide inquiète de cette assertion paroxystique, traduisant ce «malaise de la culture» qu’évoquait Freud, que la pensée, la littérature et l’art du XXe siècle européen évoluent. Cependant, le christianisme dont ce cri signe l’extrême décadence, n’est pas seul à imprégner les productions artistiques de ce siècle, même les plus prétendument athées, mais avant tout la figure du Christ - autour de laquelle sont structurés tant cette religion que son système de croyance – semble, littéralement et paradoxalement, infester l’imaginaire du XXe siècle, sous des formes plus ou moins fantasmatiques. Ce travail se propose ainsi précisément d’étudier, dans une optique interdisciplinaire entre littérature, art et cinéma, cette dynamique controversée, ses causes, les processus qui la sous-tendent ainsi que ses effets, à partir des œuvres de trois auteurs : Artaud, Beckett et Pasolini. L’objectif est de fournir une clé de lecture de cette problématique qui mette en exergue comment « la conversion de la croyance », comme la définit Deleuze, à laquelle ces auteurs participent, n’engendre pas un rejet purement profanatoire du christianisme mais, à l’inverse, la mise en œuvre d’un mouvement aussi violent que libératoire qualifié par Nancy de « déconstruction du christianisme ». Ce travail entend donc étudier tout d’abord à la lumière de l’expérience intérieure de Bataille, l’imaginaire christique qui sous-tend leurs productions ; puis, d’en analyser les mouvements et les effets en les questionnant sur la base de cette dynamique ambivalente que Grossman nomme la « défiguration de la forme christique ». Les excès délirants d’Artaud, l’ironie tranchante de Beckett et la passion ambiguë de Pasolini s’avèrent ainsi participer à un mouvement commun qui, oscillant entre reprise et rejet, débouche sur une attitude tout aussi destructive que revitalisante des fondements du christianisme.

Moduli consensuali nei rapporti tra Stato e autonomie territoriali e ruolo delle Conferenze

Ad oltre un decennio dalla riforma costituzionale del 2001, la non compiuta attuazione della stessa sembra condurre ad una nuova ed assai prossima revisione costituzionale. Nel mutato quadro costituzionale di quest’ultimo periodo l’attenzione e l’interesse sono stati richiamati da una grande quantità di accordi, di intese e di altri moduli consensuali, introdotti ed esitati nei rapporti tra Stato ed autonomie territoriali. Dall’esame del sistema delle Conferenze si è evidenziata la loro indispensabilità ai fini del coordinamento delle azioni politico –amministrative delle autonomie territoriali, ma è anche venuta fuori l’esigenza di ricorrere frequentemente ad altri tipi di moduli consensuali, spesso non tipizzati in ambito legislativo. I principi di sussidiarietà e di leale collaborazione inducono non di rado ad assumere, nella concretezza, forme eterogenee poco chiare e confuse (accordo, intesa, concerto, parere) che, pur considerati i contributi offerti dalla dottrina e dalla giurisprudenza, richiederebbero un intervento da parte del legislatore. L’approfondimento tematico ha rilevato, nel contesto di rapporti tra Stato ed autonomie territoriali, un movimento per così dire ondulatorio tra accese spinte autonomistiche e rimarcate esigenze centralistiche, lasciando ancora nella prospettiva una operativa ed efficiente armonia istituzionale.