+ <sect1 id="Features">
+ <title>Features</title>
+ <para><application>Matita</application> is an interactive theorem prover
+ (or proof assistant) with the following characteristics:</para>
+ <itemizedlist>
+ <listitem>
+ <para>It is based on a variant of the Calculus of (Co)Inductive Constructions (CIC). CIC is also the logic of the Coq proof assistant.</para>
+ </listitem>
+ <listitem>
+ <para>It adopts a procedural proof language, but it has a new set of small step tacticals that improve proof structuring and debugging.</para>
+ </listitem>
+ <listitem>
+ <para>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:</para>
+ <itemizedlist>
+ <listitem>
+ <para>It is based and fully integrated with Gtk/Gnome.</para>
+ </listitem>
+ <listitem>
+ <para>An on-line help can be browsed via the Gnome documentation browser.</para>
+ </listitem>
+ <listitem>
+ <para>Mathematical formulae are rendered in two dimensional notation via MathML and Unicode.</para>
+ </listitem>
+ </itemizedlist>
+ </listitem>
+ <listitem>
+ <para>It integrates advanced browsing and searching procedures.</para>
+ </listitem>
+ <listitem>
+ <para>It allows the use of the typical ambiguous mathematical notation by means of a disambiguating parser.</para>
+ </listitem>
+ <listitem>
+ <para>It is compatible with the library of Coq (definitions and proof objects).</para>
+ </listitem>
+ </itemizedlist>
+ </sect1>
+ <sect1 id="WrtCoq">
+ <title>Matita vs Coq</title>