{'fraction_non_alphanumeric': 0.02039529015979815, 'fraction_numerical': 0.001471825063078217, 'mean_word_length': 4.7941534713763705, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
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.