]> matita.cs.unibo.it Git - helm.git/blob - helm/www/matita1.0/documentation.shtml
- natural numbers with infinity for lambdadelta
[helm.git] / helm / www / matita1.0 / documentation.shtml
1 <!--#include virtual="xhtml-header.shtml" -->
2 <!-- $Id$ -->
3 <html xmlns="http://www.w3.org/1999/xhtml">
4   <head>
5     <title>Matita - Documentation</title>
6     <!--#include virtual="xhtml-meta.shtml" -->
7 <script type="text/javascript">
8   function toggleAbstracts() {
9     abstracts = document.getElementsByTagName("span");
10     len = abstracts.length;
11     for (i=0; i != len-1; i++) {
12       elt = abstracts.item(i);
13       if (elt.hasAttribute("class")) {
14         if (elt.getAttribute("class") == "paper_abstract") {
15           if (elt.style.display != "none") {
16             elt.style.display = "none";
17           } else {
18             elt.style.display = "inline";
19           }
20         }
21       }
22     }
23   }
24 </script>
25   </head>
26   <body>
27     <!--#include virtual="menubar.shtml" -->
28     <div class="main">
29       <h1>Matita Documentation</h1>
30
31       <h2>User Manual<a name="manual"></a></h2>
32
33       <p> The Matita User Manual is accessible from Matita itself via the
34       <a href="http://developer.gnome.org/arch/doc/help.html">GNOME Help
35         System</a>, just hit <kbd>&lt;F1&gt;</kbd> while running Matita and it
36       will be shown to you. </p>
37
38       <p> Alternatively you can browse it in
39       <!--<a href="http://www.w3.org/TR/xhtml1/">-->XHTML<!--</a>--> format:
40       </p>
41       <ul>
42         <li> <a href="docs/manual/html">Matita User Manual (XHTML format, multiple pages)</a>
43         </li>
44       </ul>
45
46       <p> The source code of the user manual (in <a
47         href="http://www.oasis-open.org/docbook/">DocBook</a> format) is
48       available from our repository, in the
49       <a href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&amp;path=%2Ftrunk%2Fhelm%2Fsoftware%2Fmatita%2Fhelp%2FC%2F&amp;rev=0&amp;sc=0">matita/help/C/</a> folder. </p>
50
51       <h2>Tutorials<a name="tutorial"></a></h2>
52
53       <p>A not so short <a href="FILES/matita-tut.pdf">tutorial</a> by 
54       A.Asperti, discussing some basic notions of number theory, for
55       the stable version of Matita.</p>
56
57       <p>A <a href="docs/tutorial/igft.html">tutorial</a> by E.Tassi based on
58       the formalization of the paper "Between formal topology and game theory:
59       an explicit solution for the conditions for an inductive generation of
60       formal topologies" by S.Berardi and S.Valentini. The tutorial describes
61       the ng version of Matita (not officially released yet, cohexisting with
62       the stable system in version 0.5.8). If some characters are not displayed
63       correctly (i.e. you are not using firefox) you may try the 
64       <a href="docs/tutorial/igft.pdf">pdf version</a>.
65       </p>
66
67
68       <h2>Exercises<a name="exercises"></a></h2>
69
70       <p>Some commented <a href="FILES/matita-ex.pdf">exercises</a> given at the 
71       <a href="http://typessummerschool07.cs.unibo.it">types summer school 2007</a>
72       by C.Sacerdoti and E.Tassi.
73       </p>
74
75       <h2>Publications</h2>
76       <!--#include virtual="papers.shtml" -->
77
78       <h2>Large Developments</h2>
79       <!--#include virtual="theses.shtml" -->
80
81       <!--#include virtual="bottombar.shtml" -->
82     </div>
83   </body>
84 </html>