From b8e426e4d942b7776fe8411f01df6974b2d35fc5 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 3 Apr 2012 09:17:00 +0000 Subject: [PATCH] Versione italiana --- helm/www/matita/matita.shtml | 2 + helm/www/matita/matita_it.shtml | 94 +++++++-------------------------- 2 files changed, 21 insertions(+), 75 deletions(-) diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml index 68ebc8ad2..b06da9bd0 100644 --- a/helm/www/matita/matita.shtml +++ b/helm/www/matita/matita.shtml @@ -25,6 +25,8 @@ University of Bologna.

+

+

diff --git a/helm/www/matita/matita_it.shtml b/helm/www/matita/matita_it.shtml index eeafd975e..49db3b9f6 100644 --- a/helm/www/matita/matita_it.shtml +++ b/helm/www/matita/matita_it.shtml @@ -26,85 +26,29 @@ Universita' degli Studi di Bologna.

- +

+ Matita si fonda su di un Sistema di Tipi Dipendenti noto con il nome di Calcolo delle + Costruzioni Induttive.

-

- - - 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.

+

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. +

-

- - - 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;

+

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 e + ragionamento: 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 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.

+

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: -

-

- -- 2.39.2