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.
| Identifer | oai:union.ndltd.org:unibo.it/oai:amsdottorato.cib.unibo.it:616 |
| Date | 16 April 2007 |
| Creators | Zacchiroli, Stefano <1979> |
| Contributors | Asperti, Andrea |
| Publisher | Alma Mater Studiorum - Università di Bologna |
| Source Sets | Università di Bologna |
| Language | English |
| Detected Language | English |
| Type | Doctoral Thesis, PeerReviewed |
| Format | application/pdf |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.002 seconds