2 <!-- ============= Introduction ============================== -->
4 <chapter id="sec_intro">
5 <title>Introduction</title>
7 <title>Features</title>
8 <para><application>Matita</application> is an interactive theorem prover
9 (or proof assistant) with the following characteristics:</para>
12 <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>
15 <para>It adopts a procedural proof language, but it has a new set of small step tacticals that improve proof structuring and debugging.</para>
18 <para>It has a stand-alone graphical user interface (GUI) inspired by
19 CtCoq/Proof General. The GUI is implemented according to the state
20 of the art. In particular:</para>
23 <para>It is based and fully integrated with Gtk/Gnome.</para>
26 <para>An on-line help can be browsed via the Gnome documentation browser.</para>
29 <!--<para>Mathematical formulae are rendered in two dimensional notation via MathML and Unicode.</para>-->
30 <para>Mathematical formulae are rendered via Unicode.</para>
36 <para>It integrates advanced browsing and searching procedures.</para>
39 <para>It allows the use of the typical ambiguous mathematical notation by means of a disambiguating parser.</para>
43 <para>It is compatible with the library of Coq (definitions and proof objects).</para>
49 <title>Matita vs Coq</title>
51 The system shares a common look&feel with the Coq proof assistant
52 and its graphical user interface. The two systems have variants
54 close proof languages and similar sets of tactics. <!--Moreover,
55 Matita is compatible with the library of Coq.-->
56 From the user point of view the main lacking features
57 with respect to Coq are:
61 <para>proof extraction;</para>
64 <para>an extensible language of tactics;</para>
67 <para>automatic implicit arguments;</para>
70 <para>several ad-hoc decision procedures;</para>
73 <para>several rarely used variants for most of the tactics;</para>
76 <para>sections and local variables. <!--To maintain compatibility with the library of Coq, theorems defined inside sections are abstracted by name over the section variables; their instances are explicitly applied to actual arguments by means of explicit named substitutions.--></para>
80 Still from the user point of view, the main differences with respect
85 <para>the language of tacticals that allows execution of partial tactical application;</para>
88 <para>the unification of the concept of metavariable and existential variable;</para>
91 <para>terms with subterms that cannot be inferred are always allowed as arguments of tactics or other commands;</para>
94 <para>ambiguous terms are disambiguated by direct interaction with the user;</para>
97 <para>theorems and definitions in the library are always accessible without needing to require/include them; right now, only notation needs to be included to become active, but we plan to remove this limitation.</para>