X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fmatita_it.shtml;h=04b43167c0780a6a1dac8718beb7615ba9a88857;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;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 screenshot: authoring interface - - - - 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. -

- -

- - - Matita screenshot: hyperlinks - - - Matita screenshot: direct manipulation - - - 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.

-

- - - Matita screenshot: library browsing - - - Matita screenshot: Whelp query - - - - - 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. +

-

- - - Matita screenshot: tinycals - - - 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: -

-

+