helm/software/matita/dist/README

   1
   2 MATITA
   3 ------
   4
   5 Matita is a new document-centric interactive theorem prover that integrates
   6 several Mathematical Knowledge Management tools and techniques.
   7
   8 Matita is traditional. Its logical foundation is the Calculus of (Co)Inductive
   9 Constructions (CIC). It can re-use mathematical concepts produced by other
  10 proof assistants like Coq and encoded in an XML encoding of CIC. The
  11 interaction paradigm of Matita is familiar, being inspired by CtCoq and Proof
  12 General. Its proof language is procedural in the same spirit of LCF.
  13
  14 Matita is innovative:
  15
  16 - the user interface sports high quality bidimensional rendering of proofs and
  17   formulae transformed on-the-fly to MathML markup, on which direct
  18   manipulation of the underlying CIC terms is still possible;
  19
  20 - the knowledge base is distributed: every authored concepts can be published
  21   becoming part of the Matita library which can be browsed as an hypertext
  22   (locally or on the World Wide Web) and searched by means of content-based
  23   queries;
  24
  25 - the tactical language, part of the proof language, has step-by-step
  26   semantics, enabling inspection and replaying of deeply structured proof
  27   scripts.
  28
  29 More information are available on the Matita web site:
  30
  31   http://matita.cs.unibo.it/
  32
  33
  34 INSTALLATION
  35 ------------
  36
  37 See the file INSTALL for building and installation instructions.
  38
  39
  40 BUGS
  41 ----
  42
  43 Bugs reporting is handled using the Bugzilla bug tracker available at:
  44
  45   http://bugs.mowgli.cs.unibo.it/
  46
  47
  48 LICENSE
  49 -------
  50
  51 Matita and its documentation are free software.
  52 See the file COPYING for copying conditions.
  53