Matita is a graphical interactive theorem prover based on the Calculus of (Co)Inductive Constructions. . Matita adopts XML-encoded proof objects are produced for storage and exchange. This makes it compatible, at some extent, with Coq. . The graphical interface has been inspired by CtCoq and Proof General. It supports high quality bidimensional rendering of proofs and formulae transformed on-the-fly to MathML markup
matita-doc | user manual of the Matita interactive theorem prover | Mehr ...
This package contains the PDF and HTML formatted Matita user manual.
matita-standard-library | standard library for the Matita interactive theorem prover | Mehr ...
Matita is a graphical interactive theorem prover based on the Calculus of (Co)Inductive Constructions. . This package contains the standard library of theorems of the matita interactive theorem prover.
