X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_intro.xml;h=6c22f46647fe4dad91567fefc8f3af95c5b82634;hb=f583b4389d0227ff0da1954af484db7ef1f5fbfc;hp=5510c8eef810b2532374cc8b62bfdaf673f01af8;hpb=1da3c8d481853c3d6b9f33385ebde848866a37b5;p=helm.git
diff --git a/helm/software/matita/help/C/sec_intro.xml b/helm/software/matita/help/C/sec_intro.xml
index 5510c8eef..6c22f4664 100644
--- a/helm/software/matita/help/C/sec_intro.xml
+++ b/helm/software/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.
+
+
+
+