Table of Contents
Matita is an interactive theorem prover - (or proof assistant) with the following characteristics:
It is based on a variant of the Calculus of (co)Inductive Constructions (CIC). CIC is also the logic of the Coq proof assistant.
It adopts a procedural proof language, but it has a new set of small step tacticals that improve proof structuring and debugging.
It has a stand-alone graphical user interface (GUI) inspired by +
Chapter 1. Introduction 
Matita Home+ User Manual (rev. 1α)ÂTable of Contents
Matita is an interactive theorem prover + (or proof assistant) with the following characteristics:
It is based on a variant of the Calculus of (Co)Inductive Constructions (CIC). CIC is also the logic of the Coq proof assistant.
It adopts a procedural proof language, but it has a new set of small step tacticals that improve proof structuring and debugging.
It has a stand-alone graphical user interface (GUI) inspired by CtCoq/Proof General. The GUI is implemented according to the state of the art. In particular:
It is based and fully integrated with Gtk/Gnome.
An on-line help can be browsed via the Gnome documentation browser.
Mathematical formulae are rendered in two dimensional notation via MathML and Unicode.
It integrates advanced browsing and searching procedures.
It allows the use of the typical ambiguous mathematical notation by means of a disambiguating parser.
It is compatible with the library of Coq (definitions and proof objects).
Home  Matita vs Coq