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.

Web advertising. Le comunicazioni commerciali on-line.

La tesi ha ad oggetto lo studio e l’approfondimento delle forme di promozione commerciale presenti in Rete caratterizzate, più che da una normale evoluzione, da continue metamorfosi che ridefiniscono ogni giorno il concetto di pubblicità. L’intento è quello di analizzare il quadro giuridico applicabile alla pubblicità via Web, a fronte della varità di forme e di modalità che essa può assumere. Nel lavoro vengono passate in rassegna le caratteristiche che differenziano la pubblicità commerciale on-line rispetto a quella tradizionale; tra le quali, particolare rilievo assume la capacità d’istaurare una relazione – diretta e non mediata – tra impresa e consumatore. Nel prosieguo viene affrontato il problema dell’individuazione, stante il carattere a-territoriale della Rete, della legge applicabile al web advertising, per poi passare ad una ricognizione delle norme europee ed italiane in materia, senza trascurare quelle emanate in sede di autodisciplina. Ampio spazio è dedicato, infine, all’esame delle diverse e più recenti tecniche di promozione pubblicitaria, di cui sono messi in evidenza gli aspetti tecnico-informatici, imprescindibili ai fini di una corretta valutazione del tema giuridico. In particolare, vengono approfonditi il servizio di posizionamento a pagamento offerto dai principali motori di ricerca (keywords advertising) e gli strumenti di tracciamento dei “comportamenti” on-line degli utenti, che consentono la realizzazione di campagne pubblicitarie mirate (on-line behavioural advertising). Il Web, infatti, non offre più soltanto la possibilità di superare barriere spaziali, linguistiche o temporali e di ampliare la propria sfera di notorietà, ma anche di raggiungere l’utente “interessato” e, pertanto, potenziale acquirente. Di queste nuove realtà pubblicitarie vengono vagliati gli aspetti più critici ed esaminata la disciplina giuridica eventualmente applicabile anche alla luce delle principali decisioni giurisprudenziali nazionali ed europee in materia, nonché delle esperienze giuridiche nord-americane e di tipo autoregolamentare.

Knowledge Patterns for the Web: extraction, tranformation and reuse

This thesis aims at investigating methods and software architectures for discovering what are the typical and frequently occurring structures used for organizing knowledge in the Web. We identify these structures as Knowledge Patterns (KPs). KP discovery needs to address two main research problems: the heterogeneity of sources, formats and semantics in the Web (i.e., the knowledge soup problem) and the difficulty to draw relevant boundary around data that allows to capture the meaningful knowledge with respect to a certain context (i.e., the knowledge boundary problem). Hence, we introduce two methods that provide different solutions to these two problems by tackling KP discovery from two different perspectives: (i) the transformation of KP-like artifacts to KPs formalized as OWL2 ontologies; (ii) the bottom-up extraction of KPs by analyzing how data are organized in Linked Data. The two methods address the knowledge soup and boundary problems in different ways. The first method provides a solution to the two aforementioned problems that is based on a purely syntactic transformation step of the original source to RDF followed by a refactoring step whose aim is to add semantics to RDF by select meaningful RDF triples. The second method allows to draw boundaries around RDF in Linked Data by analyzing type paths. A type path is a possible route through an RDF that takes into account the types associated to the nodes of a path. Then we present K~ore, a software architecture conceived to be the basis for developing KP discovery systems and designed according to two software architectural styles, i.e, the Component-based and REST. Finally we provide an example of reuse of KP based on Aemoo, an exploratory search tool which exploits KPs for performing entity summarization.

One archive, many readings. Personal archives as complex networks in the semantic web

Personal archives are the archives created by individuals for their own purposes. Among these are the library and documentary collections of writers and scholars. It is only recently that archival literature has begun to focus on this category of archives, emphasising how their heterogeneous nature necessitates the conciliation of different approaches to archival description, and calling for a broader understanding of the principle of provenance, recognising that multiple creators, including subsequent researchers, can contribute to shaping personal archives over time by adding new layers of contexts. Despite these advances in the theoretical debate, current architectures for archival representation remain behind. Finding aids privilege a single point of view and do not allow subsequent users to embed their own, potentially conflicting, readings. Using semantic web technologies this study aims to define a conceptual model for writers' archives based on existing and widely adopted models in the cultural heritage and humanities domains. The model developed can be used to represent different types of documents at various levels of analysis, as well as record content and components. It also enables the representation of complex relationships and the incorporation of additional layers of interpretation into the finding aid, transforming it from a static search tool into a dynamic research platform.  The personal archive and library of Giuseppe Raimondi serves as a case study for the creation of an archival knowledge base using the proposed conceptual model. By querying the knowledge graph through SPARQL, the effectiveness of the model is evaluated. The results demonstrate that the model addresses the primary representation challenges identified in archival literature, from both a technological and methodological standpoint. The ultimate goal is to bring the output par excellence of archival science, i.e. the finding aid, more in line with the latest developments in archival thinking.