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.

Seeing and feeling the body

Recognizing one’s body as separate from the external world plays a crucial role in detecting external events, and thus in planning adequate reactions to them. In addition, recognizing one’s body as distinct from others’ bodies allows remapping the experiences of others onto one’s sensory system, providing improved social understanding. In line with these assumptions, two well-known multisensory mechanisms demonstrated modulations of somatosensation when viewing both one’s own and someone else’s body: the Visual Enhancement of Touch (VET) and the Visual Remapping of Touch (VRT) effects. Vision of the body, in the former, and vision of the body being touched, in the latter, enhance tactile processing. The present dissertation investigated the multisensory nature of these mechanisms and their neural bases. Further experiments compared these effects for viewing one’s own body or viewing another person’s body. These experiments showed important differences in multisensory processing for one’s own body, and for other bodies, and also highlighted interactions between VET and VRT effects. The present experimental evidence demonstrated that a multisensory representation of one’s body – underlie by a high order fronto-parietal network - sends rapid modulatory feedback to primary somatosensory cortex, thus functionally enhancing tactile processing. These effects were highly spatially-specific, and depended on current body position. In contrast, vision of another person’s body can drive mental representations able to modulate tactile perception without any spatial constraint. Finally, these modulatory effects seem sometimes to interact with high order information, such as emotional content of a face. This allows one’s somatosensory system to adequately modulate perception of external events on the body surface, as a function of its interaction with the emotional state expressed by another individual.

Visual-somatosensory interactions in mental representations of the body and the face

The body is represented in the brain at levels that incorporate multisensory information. This thesis focused on interactions between vision and cutaneous sensations (i.e., touch and pain). Experiment 1 revealed that there are partially dissociable pathways for visual enhancement of touch (VET) depending upon whether one sees one’s own body or the body of another person. This indicates that VET, a seeming low-level effect on spatial tactile acuity, is actually sensitive to body identity. Experiments 2-4 explored the effect of viewing one’s own body on pain perception. They demonstrated that viewing the body biases pain intensity judgments irrespective of actual stimulus intensity, and, more importantly, reduces the discriminative capacities of the nociceptive pathway encoding noxious stimulus intensity. The latter effect only occurs if the pain-inducing event itself is not visible, suggesting that viewing the body alone and viewing a stimulus event on the body have distinct effects on cutaneous sensations. Experiment 5 replicated an enhancement of visual remapping of touch (VRT) when viewing fearful human faces being touched, and further demonstrated that VRT does not occur for observed touch on non-human faces, even fearful ones. This suggests that the facial expressions of non-human animals may not be simulated within the somatosensory system of the human observer in the same way that the facial expressions of other humans are. Finally, Experiment 6 examined the enfacement illusion, in which synchronous visuo-tactile inputs cause another’s face to be assimilated into the mental self-face representation. The strength of enfacement was not affected by the other’s facial expression, supporting an asymmetric relationship between processing of facial identity and facial expressions. Together, these studies indicate that multisensory representations of the body in the brain link low-level perceptual processes with the perception of emotional cues and body/face identity, and interact in complex ways depending upon contextual factors.

Giochi diplomatici. Sport e politica estera nell'Italia del secondo dopoguerra (1943-1953)

Questa tesi di dottorato, partendo dall’assunto teorico secondo cui lo sport, pur essendo un fenomeno periferico e non decisivo del sistema politico internazionale, debba considerarsi, in virtù della sua elevata visibilità, sia come un componente delle relazioni internazionali sia come uno strumento di politica estera, si pone l’obiettivo di investigare, con un approccio di tipo storico-politico, l’attività internazionale dello sport italiano nel decennio che va dal 1943 al 1953. Nello specifico viene dedicata una particolare attenzione agli attori e alle istituzioni della “politica estera sportiva”, al rientro dello sport italiano nel consesso internazionale e alla sua forza legittimante di attrazione culturale. Vengono approfonditi altresì alcuni casi relativi a «crisi politiche» che influirono sullo sport e a «crisi sportive» che influenzarono la politica. La ricerca viene portata avanti con lo scopo primario di far emergere, da un lato se e quanto coscientemente lo sport sia stato usato come strumento di politica estera da parte dei governi e della diplomazia dell’Italia repubblicana, dall’altro quanto e con quale intensità lo sviluppo dell’attività internazionale dello sport italiano abbia avuto significative ripercussioni sull’andamento e dai rapporti di forza della politica internazionale.