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.

L’espace urbain indien dans la littérature européenne au XXème siecle. Pour une perspective post-orientaliste.

L'affermarsi della teoria della « imaginative geography » di Edward Saïd (Orientalism, 1978), nell'arco degli ultimi trent'anni, ha imposto un orientamento prettamente sociopolitico, gramsciano e foucaultiano alla critica del testo, proponendo un'unica soluzione interpretativa per un corpus eterogeneo di testi (scientifici e artistici, antichi e moderni) accomunati dal fatto di « rappresentare l'Oriente ». La costruzione europea dello spazio orientale, dice Saïd, non rappresenta solo un misconoscimento dell'Altro, ma una sua rappresentazione tendenziosa e finalizzata a sostenere la macchina dell'imperialismo occidentale. In particolare, la rappresentazione « femminilizzata » della geografia orientale (come luogo dell'exploit del maschio bianco) preparebbe e accompagnerebbe l'impresa di assoggettamento politico e di sfruttamento economico dei paesi ad Est dell'Europa. Se Orientalism ha conosciuto fortune alterne dall'anno della sua apparizione, negli ultimi anni una vera e propria corrente anti-saidiana ha preso forza, soprattutto in ambito francese. Attraverso l'analisi di circa trenta opere francesi, belga, inglesi e italiane del Novecento, questa tesi cerca di visualizzare i limiti teorici della prospettiva saidiana rivolgendosi a un esame della rappresentazione dello spazio urbano indiano nella letteratura europea contemporanea. Nello specifico, uno studio delle nuove strutture e dei nuovi modelli della femminilizzazione dello spazio orientale indiano cercherà di completare – superandolo in direzione di un « post-orientalismo » – il riduzionismo della prospettiva saidiana.

Variety, flexibility, and use of abstract concepts. A multiple grounded perspective.

The nature of concepts is a matter of intense debate in cognitive sciences. While traditional views claim that conceptual knowledge is represented in a unitary symbolic system, recent Embodied and Grounded Cognition theories (EGC) submit the idea that conceptual system is couched in our body and influenced by the environment (Barsalou, 2008). One of the major challenges for EGC is constituted by abstract concepts (ACs), like fantasy. Recently, some EGC proposals addressed this criticism, arguing that the ACs comprise multifaced exemplars that rely on different grounding sources beyond sensorimotor one, including interoception, emotions, language, and sociality (Borghi et al., 2018). However, little is known about how ACs representation varies as a function of life experiences and their use in communication. The theoretical arguments and empirical studies comprised in this dissertation aim to provide evidence on multiple grounding of ACs taking into account their varieties and flexibility. Study I analyzed multiple ratings on a large sample of ACs and identified four distinct subclusters. Study II validated this classification with an interference paradigm involving motor/manual, interoceptive, and linguistic systems during a difficulty rating task. Results confirm that different grounding sources are activated depending on ACs kind. Study III-IV investigate the variability of institutional concepts, showing that the higher the law expertise level, the stronger the concrete/emotional determinants in their representation. Study V introduced a novel interactive task in which abstract and concrete sentences serve as cues to simulate conversation. Analysis of language production revealed that the uncertainty and interactive exchanges increase with abstractness, leading to generating more questions/requests for clarifications with abstract than concrete sentences. Overall, results confirm that ACs are multidimensional, heterogeneous, and flexible constructs and that social and linguistic interactions are crucial to shaping their meanings. Investigating ACs in real-time dialogues may be a promising direction for future research.