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.

Biometanazione della frazione organica di rifiuti solidi urbani da raccolta indifferenziata mediante codigestione con refluo zootecnico o addizione di solfuro di sodio

Il presente elaborato è stato finalizzato allo sviluppo di un processo di digestione anaerobica della frazione organica dei rifiuti solidi urbani (FORSU oppure, in lingua inglese OFMSW, Organic Fraction of Municipal Solid Waste) provenienti da raccolta indifferenziata e conseguente produzione di biogas da impiegarsi per il recupero energetico. Questo lavoro rientra nell’ambito di un progetto, cofinanziato dalla Regione Emilia Romagna attraverso il Programma Regionale per la Ricerca Industriale, l’Innovazione e il Trasferimento Tecnologico (PRRIITT), sviluppato dal Dipartimento di Chimica Applicata e Scienza dei Materiali (DICASM) dell’Università di Bologna in collaborazione con la Facoltà di Ingegneria dell’Università di Ferrara e con la società Recupera s.r.l. che applicherà il processo nell’impianto pilota realizzato presso il proprio sito di biostabilizzazione e compostaggio ad Ostellato (FE). L’obiettivo è stato la verifica della possibilità di impiegare la frazione organica dei rifiuti indifferenziati per la produzione di biogas, e in particolare di metano, attraverso un processo di digestione anaerobica previo trattamento chimico oppure in codigestione con altri substrati organici facilmente fermentabili. E’ stata inoltre studiata la possibilità di impiego di reattori con biomassa adesa per migliorare la produzione specifica di metano e diminuire la lag phase. Dalla sperimentazione si può concludere che è possibile giungere allo sviluppo di metano dalla purea codigerendola assieme a refluo zootecnico. Per ottenere però produzioni significative la quantità di solidi volatili apportati dal rifiuto non deve superare il 50% dei solidi volatili complessivi. Viceversa, l’addizione di solfuri alla sola purea si è dimostrata ininfluente nel tentativo di sottrarre gli agenti inibitori della metanogenesi. Inoltre, l’impiego di supporti di riempimento lavorando attraverso processi batch sequenziali permette di eliminare, nei cicli successivi al primo, la lag phase dei batteri metanogeni ed incrementare la produzione specifica di metano.

Mixed Mode Fracture Behaviour of Piezoelectric Materials

Piezoelectrics present an interactive electromechanical behaviour that, especially in recent years, has generated much interest since it renders these materials adapt for use in a variety of electronic and industrial applications like sensors, actuators, transducers, smart structures. Both mechanical and electric loads are generally applied on these devices and can cause high concentrations of stress, particularly in proximity of defects or inhomogeneities, such as flaws, cavities or included particles. A thorough understanding of their fracture behaviour is crucial in order to improve their performances and avoid unexpected failures. Therefore, a considerable number of research works have addressed this topic in the last decades. Most of the theoretical studies on this subject find their analytical background in the complex variable formulation of plane anisotropic elasticity. This theoretical approach bases its main origins in the pioneering works of Muskelishvili and Lekhnitskii who obtained the solution of the elastic problem in terms of independent analytic functions of complex variables. In the present work, the expressions of stresses and elastic and electric displacements are obtained as functions of complex potentials through an analytical formulation which is the application to the piezoelectric static case of an approach introduced for orthotropic materials to solve elastodynamics problems. This method can be considered an alternative to other formalisms currently used, like the Stroh’s formalism. The equilibrium equations are reduced to a first order system involving a six-dimensional vector field. After that, a similarity transformation is induced to reach three independent Cauchy-Riemann systems, so justifying the introduction of the complex variable notation. Closed form expressions of near tip stress and displacement fields are therefore obtained. In the theoretical study of cracked piezoelectric bodies, the issue of assigning consistent electric boundary conditions on the crack faces is of central importance and has been addressed by many researchers. Three different boundary conditions are commonly accepted in literature: the permeable, the impermeable and the semipermeable (“exact”) crack model. This thesis takes into considerations all the three models, comparing the results obtained and analysing the effects of the boundary condition choice on the solution. The influence of load biaxiality and of the application of a remote electric field has been studied, pointing out that both can affect to a various extent the stress fields and the angle of initial crack extension, especially when non-singular terms are retained in the expressions of the electro-elastic solution. Furthermore, two different fracture criteria are applied to the piezoelectric case, and their outcomes are compared and discussed. The work is organized as follows: Chapter 1 briefly introduces the fundamental concepts of Fracture Mechanics. Chapter 2 describes plane elasticity formalisms for an anisotropic continuum (Eshelby-Read-Shockley and Stroh) and introduces for the simplified orthotropic case the alternative formalism we want to propose. Chapter 3 outlines the Linear Theory of Piezoelectricity, its basic relations and electro-elastic equations. Chapter 4 introduces the proposed method for obtaining the expressions of stresses and elastic and electric displacements, given as functions of complex potentials. The solution is obtained in close form and non-singular terms are retained as well. Chapter 5 presents several numerical applications aimed at estimating the effect of load biaxiality, electric field, considered permittivity of the crack. Through the application of fracture criteria the influence of the above listed conditions on the response of the system and in particular on the direction of crack branching is thoroughly discussed.

Algebraische Zyklen auf abelschen Varietäten der Dimension 4 mit Polarisierung von Typ (1,2,2,2)

Diese Arbeit besch"aftigt sich mit algebraischen Zyklen auf komplexen abelschen Variet"aten der Dimension 4. Ziel der Arbeit ist ein nicht-triviales Element in $Griff^{3,2}(A^4)$ zu konstruieren. Hier bezeichnet $A^4$ die emph{generische} abelsche Variet"at der Dimension 4 mit Polarisierung von Typ $(1,2,2,2)$. Die ersten drei Kapitel sind eine Wiederholung von elementaren Definitionen und Begriffen und daher eine Festlegung der Notation. In diesen erinnern wir an elementare Eigenschaften der von Saito definierten Filtrierungen $F_S$ und $Z$ auf den Chowgruppen (vgl. cite{Sa0} und cite{Sa}). Wir wiederholen auch eine Beziehung zwischen der $F_S$-Filtrierung und der Zerlegung von Beauville der Chowgruppen (vgl. cite{Be2} und cite{DeMu}), welche aus cite{Mu} stammt. Die wichtigsten Begriffe in diesem Teil sind die emph{h"ohere Griffiths' Gruppen} und die emph{infinitesimalen Invarianten h"oherer Ordnung}. Dann besch"aftigen wir uns mit emph{verallgemeinerten Prym-Variet"aten} bez"uglich $(2:1)$ "Uberlagerungen von Kurven. Wir geben ihre Konstruktion und wichtige geometrische Eigenschaften und berechnen den Typ ihrer Polarisierung. Kapitel ref{p-moduli} enth"alt ein Resultat aus cite{BCV} "uber die Dominanz der Abbildung $p(3,2):mathcal R(3,2)longrightarrow mathcal A_4(1,2,2,2)$. Dieses Resultat ist von Relevanz f"ur uns, weil es besagt, dass die generische abelsche Variet"at der Dimension 4 mit Polarisierung von Typ $(1,2,2,2)$ eine verallgemeinerte Prym-Variet"at bez"uglich eine $(2:1)$ "Uberlagerung einer Kurve vom Geschlecht $7$ "uber eine Kurve vom Geschlecht $3$ ist. Der zweite Teil der Dissertation ist die eigentliche Arbeit und ist auf folgende Weise strukturiert: Kapitel ref{Deg} enth"alt die Konstruktion der Degeneration von $A^4$. Das bedeutet, dass wir in diesem Kapitel eine Familie $Xlongrightarrow S$ von verallgemeinerten Prym-Variet"aten konstruieren, sodass die klassifizierende Abbildung $Slongrightarrow mathcal A_4(1,2,2,2)$ dominant ist. Desweiteren wird ein relativer Zykel $Y/S$ auf $X/S$ konstruiert zusammen mit einer Untervariet"at $Tsubset S$, sodass wir eine explizite Beschreibung der Einbettung $Yvert _Thookrightarrow Xvert _T$ angeben k"onnen. Das letzte und wichtigste Kapitel enth"ahlt Folgendes: Wir beweisen dass, die emph{ infinitesimale Invariante zweiter Ordnung} $delta _2(alpha)$ von $alpha$ nicht trivial ist. Hier bezeichnet $alpha$ die Komponente von $Y$ in $Ch^3_{(2)}(X/S)$ unter der Beauville-Zerlegung. Damit und mit Hilfe der Ergebnissen aus Kapitel ref{Cohm} k"onnen wir zeigen, dass [ 0neq [alpha ] in Griff ^{3,2}(X/S) . ] Wir k"onnen diese Aussage verfeinern und zeigen (vgl. Theorem ref{a4}) begin{theorem}label{maintheorem} F"ur $sin S$ generisch gilt [ 0neq [alpha _s ]in Griff ^{3,2}(A^4) , ] wobei $A^4$ die generische abelsche Variet"at der Dimension $4$ mit Polarisierung vom Typ $(1,2,2,2)$ ist. end{theorem}

Il trattato ‘Practica musice’ di Franchino Gaffurio (1496). Genesi, tradizione del testo, trascrizione interpretativa e traduzione.

La ricerca consiste nell’edizione e traduzione del trattato ‘Practica musice’ di Franchino Gaffurio corredata da apparati critici e storico-contestuali. Si inizia con la biografia dell’autore redatta secondo gli ultimi dati disponibili e si presenta una esposizione del contenuto del trattato con proposte di chiarimenti dei passi più oscuri. Segue quindi uno studio dei cambiamenti intercorsi tra le parti del trattato come trasmesse nei manoscritti preparatori e la sua versione finale a stampa, seguito da una indagine sulle edizioni successive all’editio princeps, con tabelle sulle varianti tra le edizioni. Vengono quindi offerte la trascrizione interpretativa del testo latino del trattato (che può essere considerata la più corretta attualmente disponibile ed è l’unica a riportare numeri di partizione testuale) seguita dalla sua traduzione in italiano, con trascrizione degli esempi musicali. Il trattato, diviso in quattro libri, ha per argomenti rispettivamente il cantus planus e le scale modali gregoriane, la musica misurata e le figure della notazione, l’arte del contrappunto e la più ampia casistica disponibile sulle proporzioni ritmiche.

Processi markoviani nascosti

We introduce the notation of Markov chains and their properties, and give the definition of ergodic, irreducible and aperiodic chains with correspective examples. Then, the definition of hidden Markov models is given and their characteristics are examined. We formulate three basic problems regarding the hidden Markov models and discuss the solution of two of them - the Viterbi algorithm and the forward-backward algorithm.

On the use of textural features for writer identification in old handwritten music scores

Writer identification consists in determining the writer of a piece of handwriting from a set of writers. In this paper we present a system for writer identification in old handwritten music scores which uses only music notation to determine the author. The steps of the proposed system are the following. First of all, the music sheet is preprocessed for obtaining a music score without the staff lines. Afterwards, four different methods for generating texture images from music symbols are applied. Every approach uses a different spatial variation when combining the music symbols to generate the textures. Finally, Gabor filters and Grey-scale Co-ocurrence matrices are used to obtain the features. The classification is performed using a k-NN classifier based on Euclidean distance. The proposed method has been tested on a database of old music scores from the 17th to 19th centuries, achieving encouraging identification rates.

High-Level Modeling of Multimodal Interaction Techniques Using NiMMiT

The past few years, multimodal interaction has been gaining importance in virtual environments. Although multimodality renders interacting with an environment more natural and intuitive, the development cycle of such an application is often long and expensive. In our overall field of research, we investigate how modelbased design can facilitate the development process by designing environments through the use of highlevel diagrams. In this scope, we present ‘NiMMiT’, a graphical notation for expressing and evaluating multimodal user interaction; we elaborate on the NiMMiT primitives and demonstrate its use by means of a comprehensive example.

Plattform Musikalische Bildung

Bei der Plattform Musikalische Bildung handelt es sich um ein Projekt der Hochschule für Musik Detmold. Die Plattform vereinigt in sich Ideen zum vernetzten Musiklernen, neu entwickelten Online-Musiklern-Tools sowie den Austausch und die Modifizierung dieser erstellten Kurse durch andere Dozenten und Lehrenden. Die Plattform steht allen Dozenten und Lehrern, Studierenden und Schülern an Hochschulen, aber auch Musikschulen und allgemein bildenden Schulen kostenlos zur Verfügung. Auf die Einblendung von Werbebannern wird verzichtet. Die Inbetriebnahme einer Betaversion ist im Oktober 2014 erfolgt. Weitere Ausbaustufen sind in Planung aber noch nicht gegenfinanziert.

Monte Carlo modeling of polarized light propagation: Stokes vs Jones - Part II

In this second part of our comparative study inspecting the (dis)similarities between “Stokes” and “Jones,” we present simulation results yielded by two independent Monte Carlo programs: (i) one developed in Bern with the Jones formalism and (ii) the other implemented in Ulm with the Stokes notation. The simulated polarimetric experiments involve suspensions of polystyrene spheres with varying size. Reflection and refraction at the sample/air interfaces are also considered. Both programs yield identical results when propagating pure polarization states, yet, with unpolarized illumination, second order statistical differences appear, thereby highlighting the pre-averaged nature of the Stokes parameters. This study serves as a validation for both programs and clarifies the misleading belief according to which “Jones cannot treat depolarizing effects.”

How Do Software Architects Specify and Validate Quality Requirements?

Software architecture is the result of a design effort aimed at ensuring a certain set of quality attributes. As we show, quality requirements are commonly specified in practice but are rarely validated using automated techniques. In this paper we analyze and classify commonly specified quality requirements after interviewing professionals and running a survey. We report on tools used to validate those requirements and comment on the obstacles encountered by practitioners when performing such activity (e.g., insufficient tool-support; poor understanding of users needs). Finally we discuss opportunities for increasing the adoption of automated tools based on the information we collected during our study (e.g., using a business-readable notation for expressing quality requirements; increasing awareness by monitoring non-functional aspects of a system).

Dicto: A Unified DSL for Testing Architectural Rules

Software architecture consists of a set of design choices that can be partially expressed in form of rules that the implementation must conform to. Architectural rules are intended to ensure properties that fulfill fundamental non-functional requirements. Verifying architectural rules is often a non- trivial activity: available tools are often not very usable and support only a narrow subset of the rules that are commonly specified by practitioners. In this paper we present a new highly-readable declarative language for specifying architectural rules. With our approach, users can specify a wide variety of rules using a single uniform notation. Rules can get tested by third-party tools by conforming to pre-defined specification templates. Practitioners can take advantage of the capabilities of a growing number of testing tools without dealing with them directly.

Dicto: Keeping Software Architecture Under Control

Dicto is a declarative language for specifying architectural rules using a single uniform notation. Once defined, rules can automatically be validated using adapted off-the-shelf tools.

Cantiques de Salomon Rossi : chants, psaumes et hymnes à 3, 4, 5, 6, 7 et 8 voix

Transcrits en notation moderne et publiés par S. Naumbourg

Choix de 22 madrigaux à cinq voix : avec accompagnement de chittarone, orgue, et basse continue ou à voix seules

Salomon Rossi. Transcrits en notation moderne d'après l'original imprimé à Venise (1600 - 1607) par Vincent d' Indy