<a href="http://www.unibo.it">Universita' degli Studi di Bologna</a>.
</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>
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>Questo calcolo integra al proprio interno alcuni cosrtutti computazionali tipici dei linguaggi di programmazione funzionali: in particolare, si
- possono definire funzioni per ricorsione (ben fondata), la cui
- applizazione puo' essere effetivamente calcolata come per normali programmi.
+ <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>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 e
- ragionamento: le prove sono oggetti di prima classe del linguaggio
+ <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
+ <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>
+ <!--#include virtual="bottombar.shtml" -->
+
</div>
</body>
</html>