X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fhelp%2FC%2Fsec_intro.xml;h=773bda24ca7f86fe0e0cba580a3e5f6e103d6b98;hb=3beaf3083a6677e1ea8228e618f385bef67b7f15;hp=5510c8eef810b2532374cc8b62bfdaf673f01af8;hpb=f89e30b4f792260fe73c013aa18559bb2b85f3e4;p=helm.git
diff --git a/matita/help/C/sec_intro.xml b/matita/help/C/sec_intro.xml
index 5510c8eef..773bda24c 100644
--- a/matita/help/C/sec_intro.xml
+++ b/matita/help/C/sec_intro.xml
@@ -1,15 +1,96 @@
-
+
Introduction
-
- What is Matita?
-
+
+ Features
+ Matita is an interactive theorem prover
+ (or proof assistant) with the following characteristics:
+
+
+ It is based on a variant of the Calculus of (co)Inductive Constructions (CIC). CIC is also the logic of the Coq proof assistant.
+
+
+ It adopts a procedural proof language, but it has a new set of small step tacticals that improve proof structuring and debugging.
+
+
+ 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:
+
+
+ It is based and fully integrated with Gtk/Gnome.
+
+
+ An on-line help can be browsed via the Gnome documentation browser.
+
+
+ Mathematical formulae are rendered in two dimensional notation via MathML and Unicode.
+
+
+
+
+ It integrates advanced browsing and searching procedures.
+
+
+ It allows the use of the typical ambiguous mathematical notation by means of a disambiguating parser.
+
+
+ It is compatible with the library of Coq (definitions and proof objects).
+
+
+
+
+ Matita vs Coq
- Matita is a proof assistant for ...
+ The system shares a common look&feel with the Coq proof assistant
+ and its graphical user interface. The two systems have the same logic,
+ very close proof languages and similar sets of tactics. Moreover,
+ Matita is compatible with the library of Coq.
+ From the user point of view the main lacking features
+ with respect to Coq are:
-
-
-
-
+
+
+ proof extraction;
+
+
+ an extensible language of tactics;
+
+
+ automatic implicit arguments;
+
+
+ several ad-hoc decision procedures;
+
+
+ several rarely used variants for most of the tactics;
+
+
+ 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.
+
+
+
+ Still from the user point of view, the main differences with respect
+ to Coq are:
+
+
+
+ the language of tacticals that allows execution of partial tactical application;
+
+
+ the unification of the concept of metavariable and existential variable;
+
+
+ terms with subterms that cannot be inferred are always allowed as arguments of tactics or other commands;
+
+
+ ambiguous terms are disambiguated by direct interaction with the user;
+
+
+ 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.
+
+
+
+