Patch to make it compile with recent OCaml

[helm.git] / helm / www / matita / matita_it.shtml

diff --git a/helm/www/matita/matita_it.shtml b/helm/www/matita/matita_it.shtml
index 49db3b9f67f521303c78923b6f0b4f675a8f7e94..04b43167c0780a6a1dac8718beb7615ba9a88857 100644 (file)
--- a/helm/www/matita/matita_it.shtml
+++ b/helm/www/matita/matita_it.shtml
@@ -26,29 +26,39 @@
       <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>