From a42ff35af2d413daa87d567ff265b2ebe3c9b58d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 26 May 2006 14:18:09 +0000 Subject: [PATCH] More documentation. --- helm/software/matita/help/C/sec_intro.xml | 75 +++++++++++++++++++++-- 1 file changed, 71 insertions(+), 4 deletions(-) diff --git a/helm/software/matita/help/C/sec_intro.xml b/helm/software/matita/help/C/sec_intro.xml index a3dbc5166..169517088 100644 --- a/helm/software/matita/help/C/sec_intro.xml +++ b/helm/software/matita/help/C/sec_intro.xml @@ -3,13 +3,80 @@ Introduction - - What is Matita? + + Features - Matita is a proof assistant for ... + 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. + + + + 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. + + - -- 2.39.2