X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_intro.xml;h=6c22f46647fe4dad91567fefc8f3af95c5b82634;hb=7a9b394943d524181128816a4b02152aa79929fe;hp=a3dbc51660b9e6d4a6a0eef1dd9c41b9b4ef26a3;hpb=6073f0bd6760d393f229d1b61a91bf9b64af2f09;p=helm.git diff --git a/helm/software/matita/help/C/sec_intro.xml b/helm/software/matita/help/C/sec_intro.xml index a3dbc5166..6c22f4664 100644 --- a/helm/software/matita/help/C/sec_intro.xml +++ b/helm/software/matita/help/C/sec_intro.xml @@ -3,13 +3,94 @@ 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. + + -