MATITA
------

Matita is a new document-centric interactive theorem prover that integrates
several Mathematical Knowledge Management tools and techniques.

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 Proof
General. Its proof language is procedural in the same spirit of LCF.

Matita is innovative:

- the user interface sports high quality bidimensional rendering of proofs and
  formulae transformed on-the-fly to MathML markup, on which direct
  manipulation of the underlying CIC terms is still possible;

- the knowledge base is distributed: every authored concepts can be published
  becoming part of the Matita library which can be browsed as an hypertext
  (locally or on the World Wide Web) and searched by means of content-based
  queries;

- the tactical language, part of the proof language, has step-by-step
  semantics, enabling inspection and replaying of deeply structured proof
  scripts.

More information are available on the Matita web site:

  http://matita.cs.unibo.it/


INSTALLATION
------------

See the file INSTALL for building and installation instructions.


BUGS
----

Bugs reporting is handled using the Bugzilla bug tracker available at:

  http://bugs.mowgli.cs.unibo.it/


LICENSE
-------

Matita and its documentation are free software.
See the file COPYING for copying conditions.