2 <!-- ============= Introduction ============================== -->
4 <chapter id="sec_intro">
5 <title>Introduction</title>
7 <title>Features</title>
10 <application>Matita</application> is an interactive theorem prover
11 (or proof assistant) with the following characteristics:</para>
14 <listitem>It is based on a variant of the Calculus of (co)Inductive
15 Constructions (CIC). CIC is also the logic of the Coq proof assistant.
17 <listitem>It adopts a procedural proof language, but it has a new
18 set of small step tacticals that improve proof structuring and debugging.
20 <listitem>It has a stand-alone graphical user interface (GUI) inspired by
21 CtCoq/Proof General. The GUI is implemented according to the state
22 of the art. In particular:
24 <listitem>It is based and fully integrated with Gtk/Gnome.</listitem>
25 <listitem>An on-line help can be browsed via the Gnome documentation
27 <listitem>Mathematical formulae are rendered in two dimensional
28 notation via MathML and Unicode.</listitem>
31 <listitem>It integrates advanced browsing and searching procedures.
33 <listitem>It allows the use of the typical ambiguous mathematical notation
34 by means of a disambiguating parser.
36 <listitem>It is compatible with the library of Coq (definitions and
43 <title>Matita vs Coq</title>
46 The system shares a common look&feel with the Coq proof assistant
47 and its graphical user interface. The two systems have the same logic,
48 very close proof languages and similar sets of tactics. Moreover,
49 Matita is compatible with the library of Coq.
50 From the user point of view the main lacking features
51 with respect to Coq are:
55 <listitem>proof extraction;</listitem>
56 <listitem>an extensible language of tactics;</listitem>
57 <listitem>automatic implicit arguments;</listitem>
58 <listitem>several ad-hoc decision procedures;</listitem>
59 <listitem>several rarely used variants for most of the tactics;</listitem>
60 <listitem>sections and local variables. To maintain compatibility
61 with the library of Coq, theorems defined inside sections are abstracted
62 by name over the section variables; their instances are explicitly
63 applied to actual arguments by means of explicit named
64 substitutions.</listitem>
68 Still from the user point of view, the main differences with respect
73 <listitem>the language of tacticals that allows execution of partial
74 tactical application;</listitem>
75 <listitem>the unification of the concept of metavariable and existential
77 <listitem>terms with subterms that cannot be inferred are always allowed
78 as arguments of tactics or other commands;</listitem>
79 <listitem>ambiguous terms are disambiguated by direct interaction
80 with the user;</listitem>
81 <listitem>theorems and definitions in the library are always accessible
82 without needing to require/include them; right now, only notation needs
83 to be included to become active, but we plan to remove this limitation.</listitem>