]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/dist/README
more work
[helm.git] / 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