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     <para><application>Matita</application> is an interactive theorem prover
   9       (or proof assistant) with the following characteristics:</para>
  10     <itemizedlist>
  11       <listitem>
  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>
  13       </listitem>
  14       <listitem>
  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>
  16       </listitem>
  17       <listitem>
  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>
  21         <itemizedlist>
  22           <listitem>
  23             <para>It is based and fully integrated with Gtk/Gnome.</para>
  24           </listitem>
  25           <listitem>
  26             <para>An on-line help can be browsed via the Gnome documentation browser.</para>
  27           </listitem>
  28           <listitem>
  29             <para>Mathematical formulae are rendered in two dimensional notation via MathML and Unicode.</para>
  30           </listitem>
  31         </itemizedlist>
  32       </listitem>
  33       <listitem>
  34         <para>It integrates advanced browsing and searching procedures.</para>
  35       </listitem>
  36       <listitem>
  37         <para>It allows the use of the typical ambiguous mathematical notation by means of a disambiguating parser.</para>
  38       </listitem>
  39       <listitem>
  40         <para>It is compatible with the library of Coq (definitions and proof objects).</para>
  41       </listitem>
  42     </itemizedlist>
  43   </sect1>
  44   <sect1 id="WrtCoq">
  45     <title>Matita vs Coq</title>
  46     <para>
  47       The system shares a common look&amp;feel with the Coq proof assistant
  48       and its graphical user interface. The two systems have the same logic,
  49       very close proof languages and similar sets of tactics. Moreover,
  50       Matita is compatible with the library of Coq.
  51       From the user point of view the main lacking features
  52       with respect to Coq are:
  53     </para>
  54     <itemizedlist>
  55       <listitem>
  56         <para>proof extraction;</para>
  57       </listitem>
  58       <listitem>
  59         <para>an extensible language of tactics;</para>
  60       </listitem>
  61       <listitem>
  62         <para>automatic implicit arguments;</para>
  63       </listitem>
  64       <listitem>
  65         <para>several ad-hoc decision procedures;</para>
  66       </listitem>
  67       <listitem>
  68         <para>several rarely used variants for most of the tactics;</para>
  69       </listitem>
  70       <listitem>
  71         <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>
  72       </listitem>
  73     </itemizedlist>
  74     <para>
  75       Still from the user point of view, the main differences with respect
  76       to Coq are:
  77     </para>
  78     <itemizedlist>
  79       <listitem>
  80         <para>the language of tacticals that allows execution of partial tactical application;</para>
  81       </listitem>
  82       <listitem>
  83         <para>the unification of the concept of metavariable and existential variable;</para>
  84       </listitem>
  85       <listitem>
  86         <para>terms with subterms that cannot be inferred are always allowed as arguments of tactics or other commands;</para>
  87       </listitem>
  88       <listitem>
  89         <para>ambiguous terms are disambiguated by direct interaction with the user;</para>
  90       </listitem>
  91       <listitem>
  92         <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>
  93       </listitem>
  94     </itemizedlist>
  95   </sect1>
  96 </chapter>