Matita (that means pencil in Italian) is a new interactive theorem prover under development at the University of Bologna. This new proof assistant presents several innovation with respect to the state-of-the-art, whereas reatining compatibility to some extent with Coq, which is based on the same underlying calculus (the Calculus of (Co)Inductive Constructions). We will give an overview of Matita and then focus on the innovative aspects (briefly listed below) of the user interaction within the system.
Disambiguation. Most activities connected with interactive proving require the user to input formulae. Though the user would like to write them using the common ambiguous mathematical notation, most systems inhibit this due to parsing ambiguities. 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 used in procedural proof scripts to combine tactics. With tacticals scripts can be made shorter and more maintainable. Unfortunately tacticals are incompatible with script management since the inhibit to position the execution point inside large blocks. Matita implements a small step semantics that solves the issue for the largest possible subset of LCF tacticals.
Meaningful notation. Proof assistant users craft new mathematical notation to ease the use of new concepts. The architecture used in Matita for extensible notation accounts for both high quality MathML-Presentation based rendering of formulae and for "meaningful notation", where presentational fragments are kept synchronized with the underlying CIC terms. Using this approach interoperability at the content level with other systems (such as CASs) is possible as well as direct manipulation of formulae on their rendered forms.
We will also briefly touch a few of non user interaction related innovations in Matita, pointing to the relevant literatura, such as content based queries and out of band proof hint notifications.