X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fmatita.shtml;h=ce58853f7749f710461247d64dcbaacf375a1c53;hb=ff5659b6ee47292a33c84b0889b5d66d729397f6;hp=8d6a75f292791576df284c3dbd714e3bbb7e16ae;hpb=2a60d8bb599605a8f6a132f4a016b21de39b16d2;p=helm.git diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml index 8d6a75f29..ce58853f7 100644 --- a/helm/www/matita/matita.shtml +++ b/helm/www/matita/matita.shtml @@ -7,6 +7,7 @@ +
@@ -17,17 +18,23 @@ integrates several Mathematical Knowledge Management tools and techniques.

-

Matita is traditional. Its logical foundation is the +

+ + + Matita screenshot: authoring interface + + + Matita is traditional. Its logical foundation is the Calculus of (Co)Inductive Constructions (CIC). It can re-use - mathematical concepts produced by other proof assistants like - Coq and encoded in an - XML encoding of CIC. The interaction - paradigm of Matita is familiar, being inspired by CtCoq and + mathematical concepts produced by other proof assistants (e.g. + Coq) when encoded in an + XML representation of CIC. The + interaction paradigm of Matita is familiar, being inspired by CtCoq and Proof General. Its proof language is procedural in the same spirit of LCF.

Matita is innovative:

-