Matita is a new document-centric interactive theorem prover that integrates several Mathematical Knowledge Management tools and techniques.

Matita is traditional. Its logical foundation is the Calculus of (Co)Inductive Constructions (CIC). It can re-use mathematical concepts produced by other proof assistants (e.g. Coq) when encoded in an XML representation of CIC. The interaction paradigm of Matita is familiar, being inspired by CtCoq and Proof General. Its proof language is procedural in the same spirit of LCF.

Matita is innovative:

• the user interface sports high quality bidimensional rendering of proofs and formulae transformed on-the-fly to MathML markup, on which direct manipulation of the underlying CIC terms is still possible;

• the knowledge base is distributed: every authored concepts can be published becoming part of the Matita library which 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.