Matita is traditional. Its logical foundation is the +
+
+
+
+
+
+ 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:
--
+
-