X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fmatita_it.shtml;h=04b43167c0780a6a1dac8718beb7615ba9a88857;hb=258d2e384e8bf7008d2fb01c7d3fee5126d65120;hp=379be3d530d131aac01cf97adc2ed4bd751cba3f;hpb=884876e28023324f68c97f1e387431d21b0a6453;p=helm.git diff --git a/helm/www/matita/matita_it.shtml b/helm/www/matita/matita_it.shtml index 379be3d53..04b43167c 100644 --- a/helm/www/matita/matita_it.shtml +++ b/helm/www/matita/matita_it.shtml @@ -26,84 +26,39 @@ Universita' degli Studi di Bologna.
- +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.
-
-
-
-
-
-
-
- Matita e' basato sul Calcolo delle Costruzioni (Co)Induttive, ed
- parzialmente compatibile con l'analogo strumento francese
- Coq.
- 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.
-
-
-
-
-
-
-
-
-
- L'interfaccia grafica e' stata ispirata da CtCoq e
- Proof General.
- Supporta una resa bidimensionale di alta qualita' delle espressioni
- basata sul markup
- MathML.
+ Matita si fonda su di un Sistema di Tipi Dipendenti noto con il nome di Calcolo delle + Costruzioni Induttive.
-
-
-
-
-
-
-
-
-
-
-
- La base di conoscenza matematica puo'
- essere
- visitata come un ipertesto
- (localmente o sul World Wide Web) e si possono effettuare
- ricerche basate su
- interrogazioni contenutistiche;
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. +
-
-
-
-
-
-
- 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.
Al tempo stesso, le dimostrazioni sono una parte integrale del + formalismo, cosa che permette di ottenere, attraverso l' + isomorfismo di Curry Howard , 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 + proof-carrying-code, dove frammenti di software sono arricchiti con dimostrazioni di + alcune delle loro proprieta'.
+ +Matita e' attualmente adottato nel Progetto Europeo CerCo (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.
-Matita e' finanziato parzialmente dai seguenti progetti: -