<a href="http://www.unibo.it">Universita' degli Studi di Bologna</a>.
</p>
-<!-- <a href="http://www.mkm-ig.org">Mathematical Knowledge Management</a> tools and techniques. </p> -->
+ <p>Un dimostratore interattivo e' uno strumento software di
+ ausilio alla dimostrazione formale di teoremi attraverso
+ la collaborazione tra l'uomo e la macchina. Fornisce un liguaggio
+ formale in cui coesistono definizioni matematiche, algoritmi eseguibili,
+ teoremi e relative dimostrazioni, ed un ambiente interattivo che tiene
+ traccia dello stato corrente delle prove, e le aggiorna in funzione dei
+ comandi (tattiche) impartiti dall'utente. </p>
- <p class="spaced">
- <span class="screenshots">
- <a class="quiet" href="images/screenshot-matita.png">
- <img src="images/MINI_screenshot-matita.png" alt="Matita screenshot: authoring interface" />
- </a>
- </span>
-
- Matita e' basato sul Calcolo delle Costruzioni (Co)Induttive, ed
- parzialmente compatibile con l'analogo strumento francese
- <a href="http://coq.inria.fr">Coq</a>.
- Matita e' una applicazione ragionevolmente semplice e piccola,
- la cui complessita' architetturale puo' essere
- padroneggiata da laureandi, facendone uno strumento particolarmente
- utile per la sperimentazione di nuove idee e soluzioni in ambito
- universitario.
- Matita adotta una filosofia di scrittura delle prove basata su
- tattiche; lambda-termini di prova (codificati in XML) sono prodotti
- per la memorizzazione di lungo periodo e lo scambio di dati
- con altri sistemi.
- </p>
-
- <p class="spaced">
- <span class="screenshots">
- <a class="quiet" href="images/screenshot-matita-href.png">
- <img src="images/MINI_screenshot-matita-href.png" alt="Matita screenshot: hyperlinks" />
- </a>
- <a class="quiet" href="images/screenshot-matita-selection.png">
- <img src="images/MINI_screenshot-matita-selection.png" alt="Matita screenshot: direct manipulation" />
- </a>
- </span>
- L'interfaccia grafica e' stata ispirata da CtCoq e
- <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>.
- Supporta una resa bidimensionale di alta qualita' delle espressioni
- basata sul markup
- <a href="http://www.w3.org/Math/">MathML</a>.</p>
+ <p>
+ Matita si fonda su di un Sistema di <a href="http://en.wikipedia.org/wiki/Dependent_type">Tipi Dipendenti</a> noto con il nome di Calcolo delle
+ Costruzioni Induttive.</p>
- <p class="spaced">
- <span class="screenshots">
- <a class="quiet" href="images/screenshot-cicbrowser-browsing.png">
- <img src="images/MINI_screenshot-cicbrowser-browsing.png" alt="Matita screenshot: library browsing" />
- </a>
- <a class="quiet" href="images/screenshot-cicbrowser-query.png">
- <img src="images/MINI_screenshot-cicbrowser-query.png" alt="Matita screenshot: Whelp query" />
- </a>
- <!--
- <a class="quiet" href="images/screenshot-cicbrowser-proof.png">
- <img src="images/MINI_screenshot-cicbrowser-proof.png" alt="Matita screenshot: proof rendering"
- </a>
- -->
- </span>
-
- La <a href="library.shtml">base di conoscenza matematica</a> puo'
- essere
- <a href="http://helm.cs.unibo.it/browse/">visitata</a> come un ipertesto
- (localmente o sul World Wide Web) e si possono effettuare
- <a href="http://helm.cs.unibo.it/whelp/">ricerche</a> basate su
- interrogazioni contenutistiche; </p>
+ <p>Questo calcolo integra al proprio interno alcuni costrutti computazionali
+ tipici dei linguaggi di programmazione funzionali: in particolare, si
+ possono definire funzioni per ricorsione (ben fondata), che possono essere
+ valutate e testate come dei normali programmi.
+ </p>
- <p class="spaced">
- <span class="screenshots">
- <a class="quiet" href="images/screenshot-tinycals.png">
- <img src="images/MINI_screenshot-tinycals.png" alt="Matita screenshot: tinycals" />
- </a>
- </span>
- Il linguaggio delle tattiche, parte del vernacolo di prova,
- ha una semantica passo-passo che consente di ispezionare e
- eseguire in modo non atomico anche scripts altamente strutturati.</p>
+ <p>Al tempo stesso, le dimostrazioni sono una parte integrale del
+ formalismo, cosa che permette di ottenere, attraverso l'
+ <a href="http://en.wikipedia.org/wiki/Curry-Howard_correspondence">isomorfismo di Curry Howard </a>, una efficace integrazione tra specifica del comportamento, sua realizzazione implementativa e relativa verifica di correttezza: le prove sono oggetti di prima classe del linguaggio
+ e possono essere trattati come dei normali tipi di dato, inducendo
+ in modo naturale uno stile di programmazione simile al
+ <a href="http://en.wikipedia.org/wiki/Proof-carrying_code">proof-carrying-code</a>, dove frammenti di software sono arricchiti con dimostrazioni di
+ alcune delle loro proprieta'.</p>
+
+ <p>Matita e' attualmente adottato nel Progetto Europeo <a href="http://cerco.cs.unibo.it/">CerCo</a> (Certified Complexity) per la verifica formale
+ della preservazione della complessita' durante la fase di compilazione
+ da linguaggio C verso un linguaggio assembly tipico di microprocessori
+ per sistemi embedded.</p>
- <p>Matita e' finanziato parzialmente dai seguenti progetti:
- <ul>
- <li><a href=http://www.cs.chalmers.se/Cs/Research/Logic/Types/>
- Types Project</a>
- <li><a href=http://www.mctafi.math.unipd.it/>McTafi</a></li>
- </ul>
- </p>
<!--#include virtual="bottombar.shtml" -->
+
</div>
</body>
</html>
projects / helm.git / blobdiff