helm/www/matita/matita_it.shtml

   1 <!-- $Id: matita.shtml 6610 2006-07-14 12:06:30Z zacchiro $ -->
   2 <!--#include virtual="xhtml-header.shtml" -->
   3 <html>
   4   <head>
   5     <meta name="keywords" content="Matita, prover, assistant" />
   6     <title>Matita - Home Page Italiana</title>
   7     <!--#include virtual="xhtml-meta.shtml" -->
   8   </head>
   9   <body>
  10     <!--#include virtual="menubar_it.shtml" -->
  11     <!--#include virtual="news_it.shtml" -->
  12     <div class="main">
  13
  14       <div class="topimage">
  15         <img src="images/matita-text-big.png" alt="Matita" />
  16         <a href="matita.shtml">
  17           <img src="flags/wgb.gif" alt="english flag" />
  18         </a>
  19       </div>
  20
  21       <p class="spaced">
  22       Matita e' un tool sperimentale di supporto alla dimostrazione
  23       interattiva di teoremi, in via di sviluppo al
  24       <a href="http://www.cs.unibo.it">Dipartimento di Scienze
  25       dell'Informazione</a> della
  26       <a href="http://www.unibo.it">Universita' degli Studi di Bologna</a>.
  27       </p>
  28
  29 <!-- <a href="http://www.mkm-ig.org">Mathematical Knowledge Management</a> tools and techniques. </p> -->
  30
  31       <p class="spaced">
  32       <span class="screenshots">
  33         <a class="quiet" href="images/screenshot-matita.png">
  34           <img src="images/MINI_screenshot-matita.png" alt="Matita screenshot: authoring interface" />
  35         </a>
  36       </span>
  37
  38       Matita e' basato sul Calcolo delle Costruzioni (Co)Induttive, ed
  39       parzialmente compatibile con l'analogo strumento francese
  40       <a href="http://coq.inria.fr">Coq</a>.
  41       Matita e' una applicazione ragionevolmente semplice e piccola,
  42       la cui complessita' architetturale puo' essere
  43       padroneggiata da laureandi, facendone uno strumento particolarmente
  44       utile per la sperimentazione di nuove idee e soluzioni in ambito
  45       universitario.
  46       Matita adotta una filosofia di scrittura delle prove basata su
  47       tattiche; lambda-termini di prova (codificati in XML) sono prodotti
  48       per la memorizzazione di lungo periodo e lo scambio di dati
  49       con altri sistemi.
  50       </p>
  51
  52       <p class="spaced">
  53       <span class="screenshots">
  54           <a class="quiet" href="images/screenshot-matita-href.png">
  55             <img src="images/MINI_screenshot-matita-href.png" alt="Matita screenshot: hyperlinks" />
  56           </a>
  57           <a class="quiet" href="images/screenshot-matita-selection.png">
  58             <img src="images/MINI_screenshot-matita-selection.png" alt="Matita screenshot: direct manipulation" />
  59           </a>
  60         </span>
  61       L'interfaccia grafica e' stata ispirata da CtCoq e
  62       <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>.
  63       Supporta una resa bidimensionale di alta qualita' delle espressioni
  64       basata sul markup
  65       <a href="http://www.w3.org/Math/">MathML</a>.</p>
  66
  67       <p class="spaced">
  68       <span class="screenshots">
  69           <a class="quiet" href="images/screenshot-cicbrowser-browsing.png">
  70             <img src="images/MINI_screenshot-cicbrowser-browsing.png" alt="Matita screenshot: library browsing" />
  71           </a>
  72           <a class="quiet" href="images/screenshot-cicbrowser-query.png">
  73             <img src="images/MINI_screenshot-cicbrowser-query.png" alt="Matita screenshot: Whelp query" />
  74           </a>
  75           <!--
  76           <a class="quiet" href="images/screenshot-cicbrowser-proof.png">
  77             <img src="images/MINI_screenshot-cicbrowser-proof.png" alt="Matita screenshot: proof rendering"
  78           </a>
  79           -->
  80       </span>
  81
  82       La <a href="library.shtml">base di conoscenza matematica</a> puo'
  83       essere
  84       <a href="http://helm.cs.unibo.it/browse/">visitata</a> come un ipertesto
  85       (localmente o sul World Wide Web) e si possono effettuare
  86       <a href="http://helm.cs.unibo.it/whelp/">ricerche</a> basate su
  87       interrogazioni contenutistiche; </p>
  88
  89       <p class="spaced">
  90         <span class="screenshots">
  91           <a class="quiet" href="images/screenshot-tinycals.png">
  92             <img src="images/MINI_screenshot-tinycals.png" alt="Matita screenshot: tinycals" />
  93           </a>
  94         </span>
  95         Il linguaggio delle tattiche, parte del vernacolo di prova,
  96         ha una semantica passo-passo che consente di ispezionare e
  97         eseguire in modo non atomico anche scripts altamente strutturati.</p>
  98
  99       <p>Matita e' finanziato parzialmente dai seguenti progetti:
 100       <ul>
 101        <li><a href=http://www.cs.chalmers.se/Cs/Research/Logic/Types/>
 102          Types Project</a>
 103        <li><a href=http://www.mctafi.math.unipd.it/>McTafi</a></li>
 104       </ul>
 105       </p>
 106       <!--#include virtual="bottombar.shtml" -->
 107     </div>
 108   </body>
 109 </html>