Chapter 1. Introduction

Table of Contents

Matita vs Coq


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).