Matita (that means pencil in italian) is an experimental, interactive theorem prover under development at the Computer Science Department of the University of Bologna.
Matita is based on the
Calculus of (Co)Inductive Constructions, and is compatible, at some
extent, with Coq.
It is a reasonably small and simple application, whose
architectural and software complexity is meant to be mastered by
students, providing a tool particularly suited for testing innovative
ideas and solutions.
Matita adopts a tactic based editing mode; (XML-encoded) proof objects
are produced for storage and exchange.
The graphical interface has been inspired by CtCoq and
Proof General.
It supports high quality bidimensional rendering of
proofs and formulae transformed on-the-fly to
MathML markup
The knowledge base can be
browsed as an hypertext
(locally or on the World Wide Web) and
searched by means of
content-based queries;
The tactical language, part of the proof language, has
step-by-step semantics, enabling inspection and replaying of deeply
structured proof scripts.
Matita is partially supported by the following Projects: