X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fhelp%2FC%2Fsec_intro.xml;fp=matita%2Fhelp%2FC%2Fsec_intro.xml;h=6c22f46647fe4dad91567fefc8f3af95c5b82634;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/matita/help/C/sec_intro.xml b/matita/help/C/sec_intro.xml new file mode 100644 index 000000000..6c22f4664 --- /dev/null +++ b/matita/help/C/sec_intro.xml @@ -0,0 +1,96 @@ + + + + + Introduction + + 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 + + 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. + + + +