matita/help/C/sec_intro.xml

   1
   2 <!-- ============= Introduction ============================== -->
   3
   4 <chapter id="sec_intro">
   5   <title>Introduction</title>
   6   <sect1 id="Features">
   7     <title>Features</title>
   8
   9     <para>
  10       <application>Matita</application> is an interactive theorem prover
  11       (or proof assistant) with the following characteristics:</para>
  12
  13     <itemizedlist>
  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.
  16      </listitem>
  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.
  19      </listitem>
  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:
  23       <itemizedlist>
  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
  26         browser.</listitem>
  27        <listitem>Mathematical formulae are rendered in two dimensional
  28         notation via MathML and Unicode.</listitem>
  29       </itemizedlist>
  30      </listitem>
  31      <listitem>It integrates advanced browsing and searching procedures.
  32      </listitem>
  33      <listitem>It allows the use of the typical ambiguous mathematical notation
  34       by means of a disambiguating parser.
  35      </listitem>
  36      <listitem>It is compatible with the library of Coq (definitions and
  37       proof objects).
  38      </listitem>
  39     </itemizedlist>
  40   </sect1>
  41
  42   <sect1 id="WrtCoq">
  43     <title>Matita vs Coq</title>
  44
  45     <para>
  46       The system shares a common look&amp;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:
  52     </para>
  53
  54     <itemizedlist>
  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>
  65     </itemizedlist>
  66
  67     <para>
  68       Still from the user point of view, the main differences with respect
  69       to Coq are:
  70     </para>
  71
  72     <itemizedlist>
  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
  76       variable;</listitem>
  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>
  84     </itemizedlist>
  85
  86   </sect1>
  87 </chapter>