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.

Theoretical studies of microfluidics: "walking" drops and "melting" snowflakes.

The present PhD thesis summarizes two examples of research in microfluidics. Both times water was the subject of interest, once in the liquid state (droplets adsorbed on chemically functionalized surfaces), the other time in the solid state (ice snowflakes and their fractal behaviour). The first problem deals with a slipping nano-droplet of water adsorbed on a surface with photo-switchable wettability characteristics. Main focus was on identifying the underlying driving forces and mechanical principles at the molecular level of detail. Molecular Dynamics simulation was employed as investigative tool owing to its record of successfully describing the microscopic behaviour of liquids at interfaces. To reproduce the specialized surface on which a water droplet can effectively “walk”, a new implicit surface potential was developed. Applying this new method the experimentally observed droplet slippage could be reproduced successfully. Next the movement of the droplet was analyzed at various conditions emphasizing on the behaviour of the water molecules in contact with the surface. The main objective was to identify driving forces and molecular mechanisms underlying the slippage process. The second part of this thesis is concerned with theoretical studies of snowflake melting. In the present work snowflakes are represented by filled von Koch-like fractals of mesoscopic beads. A new algorithm has been developed from scratch to simulate the thermal collapse of fractal structures based on Monte Carlo and Random Walk Simulations (MCRWS). The developed method was applied and compared to Molecular Dynamics simulations regarding the melting of ice snowflake crystals and new parameters were derived from this comparison. Bigger snow-fractals were then studied looking at the time evolution at different temperatures again making use of the developed MCRWS method. This was accompanied by an in-depth analysis of fractal properties (border length and gyration radius) in order to shed light on the dynamics of the melting process.

Analisi sperimentale dell'influenza dei parametri di processo sulla resistenza di contatto tra polimero e stampo durante la formatura

Con gli strumenti informatici disponibili oggi per le industrie, in particolar modo coi software CAE, le possibile simulare in maniera più che soddisfacente i fenomeni fisici presenti in natura. Anche il raffreddamento di un manufatto in polimero può venire simulato, a patto che si conoscano tutti i dati dei materiali e delle condizioni al contorno. Per quanto riguarda i dati dei materiali, i produttori di polimeri sono molto spesso in grado di fornirli, mentre le condizioni al contorno devono essere padroneggiate dal detentore della tecnologia. Nella pratica, tale conoscenza è al più incompleta, quindi si fanno ipotesi per colmare le lacune. Una tra le ipotesi più forti fatte è quella di una perfetta conduzione all'interfaccia tra due corpi. Questo è un vincolo troppo forte, se paragonato alla precisione di tutti gli altri dati necessari alla simulazione, e quindi si è deciso di eseguire una campagna sperimentale per stimare la resistenza al passaggio flusso termico all'interfaccia polimero-stampo ovvero determinare la conduttanza termica di contatto. L'attività svolta in questa tesi di dottorato ha come scopo quello di fornire un contributo significativo allo sviluppo e al miglioramento dell'efficienza termica degli stampi di formatura dei polimeri termoplastici con tecnologia a compressione.