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.

Contributo dei sistemi di fusione d'immagine mediante ecografia combinata con TAC e o RMN nella diagnosi del piccolo epatocarcinoma (< 2 cm) in pazienti con epatopatia cronica

L’ecografia è la metodica diagnostica più utilizzata come screening e follow-up nei pazienti epatopatici con o senza lesioni focali e questo grazie alle sue peculiari caratteristiche, che sono date dall’essere real-time, maneggevole, priva di radiazioni ionizzanti e con bassi costi. Tuttavia tale metodica se confrontata con la TC o la RMN, può avere importanti limiti, quali l’impossibilità di visualizzare piccole lesioni localizzate in aree anatomicamente “difficili” o in pazienti obesi, che sono già state identificate con altre tecniche, come la TC o la RMN. Per superare queste limitazioni sono stati introdotti dei sistemi di “fusione d’immagine” che consentono di sincronizzare in tempo reale una metodica real time con bassa risoluzione spaziale come l’ecografia ed una statica ad alta risoluzione come la TC o la RMN. Ciò si ottiene creando attorno al paziente un piccolo campo elettromagnetico costituito da un generatore e da un rilevatore applicato al trasduttore ecografico ed introducendo in un computer abbinato all’ecografo il “volume rendering” dell’addome del paziente ottenuto mediante TC multistrato o RM. Il preciso “ appaiamento spaziale “ delle due metodiche si ottiene individuando in entrambe lo stesso piano assiale di riferimento e almeno 3-4 punti anatomici interni. Tale sistema di fusione d’immagine potrebbe essere molto utile in campo epatologico nella diagnostica non invasiva del piccolo epatocarcinoma, che secondo le ultime linee guida, nei noduli di dimensioni fra 1 e 2 cm, richiede una concordanza nel comportamento contrastografico della lesione in almeno due tecniche d’immagine. Lo scopo del nostro lavoro è stato pertanto quello di valutare, in pazienti epatopatici, il contributo che tale sistema può dare nell’identificazione e caratterizzazione di lesioni inferiori a 20 mm, che erano già state identificate alla TC o alla RMN come noduli sospetti per HCC, ma che non erano stati visualizzati in ecografia convenzionale. L’eventuale re-identificazione con l’ecografia convenzionale dei noduli sospetti per essere HCC, può permettere di evitare, alla luce dei criteri diagnostici non invasivi un’ ulteriore tecnica d’immagine ed eventualmente la biopsia. Pazienti e Metodi: 17 pazienti cirrotici (12 Maschi; 5 Femmine), con età media di 68.9 +/- 6.2 (SD) anni, in cui la TC e la RMN con mezzo di contrasto avevano identificato 20 nuove lesioni focali epatiche, inferiori a 20 mm (13,6 +/- 3,6 mm), sospette per essere epatocarcinomi (HCC), ma non identificate all’ecografia basale (eseguita in cieco rispetto alla TC o alla RMN) sono stati sottoposti ad ecografia senza e con mezzo di contrasto, focalizzata su una zona bersaglio identificata tramite il sistema di fusione d’immagini, che visualizza simultaneamente le immagini della TC e della RMN ricostruite in modalità bidimensionale ( 2D), tridimensionale ( 3 D) e real-time. La diagnosi finale era stata stabilita attraverso la presenza di una concordanza diagnostica, secondo le linee guida internazionali o attraverso un follow-up nei casi di discordanza. Risultati: Una diagnosi non invasiva di HCC è stata raggiunta in 15/20 lesioni, inizialmente sospettate di essere HCC. Il sistema di fusione ha identificato e mostrato un comportamento contrastografico tipico in 12/15 noduli di HCC ( 80%) mentre 3/15 HCC (20%) non sono stati identificati con il sistema di fusione d’immagine. Le rimanenti 5/20 lesioni non sono state visualizzate attraverso i sistemi di fusione d’immagine ed infine giudicate come falsi positivi della TC e della RMN, poiché sono scomparse nei successivi mesi di follow-up e rispettivamente dopo tre, sei, nove, dodici e quindici mesi. Conclusioni: I nostri risultati preliminari mostrano che la combinazione del sistema di fusione dell’immagine associata all’ecografia senza e con mezzo di contrasto (CEUS), migliora il potenziale dell’ecografia nell’identificazione e caratterizzazione dell’HCC su fegato cirrotico, permettendo il raggiungimento di una diagnosi, secondo criteri non invasivi e slatentizzazndo casi di falsi positivi della TC e della RMN.

Mental states monitoring through passive Brain-Computer Interface systems

The monitoring of cognitive functions aims at gaining information about the current cognitive state of the user by decoding brain signals. In recent years, this approach allowed to acquire valuable information about the cognitive aspects regarding the interaction of humans with external world. From this consideration, researchers started to consider passive application of brain–computer interface (BCI) in order to provide a novel input modality for technical systems solely based on brain activity. The objective of this thesis is to demonstrate how the passive Brain Computer Interfaces (BCIs) applications can be used to assess the mental states of the users, in order to improve the human machine interaction. Two main studies has been proposed. The first one allows to investigate whatever the Event Related Potentials (ERPs) morphological variations can be used to predict the users’ mental states (e.g. attentional resources, mental workload) during different reactive BCI tasks (e.g. P300-based BCIs), and if these information can predict the subjects’ performance in performing the tasks. In the second study, a passive BCI system able to online estimate the mental workload of the user by relying on the combination of the EEG and the ECG biosignals has been proposed. The latter study has been performed by simulating an operative scenario, in which the occurrence of errors or lack of performance could have significant consequences. The results showed that the proposed system is able to estimate online the mental workload of the subjects discriminating three different difficulty level of the tasks ensuring a high reliability.