Matita 0.99.1

Matita e' un dimostratore interattivo di teoremi basato su una variante del Calcolo delle Costruzioni CoInduttive. Il software, che e' open source, e' rilasciato ai termini della GNU General Public Licence ed e' pubblicamente accessibile come repository Subversion. Matita e' scritto in OCAML. La dimensione attuale dell'applicazione si aggira sulle 70.000 linee di codice. La versione 0.99.1 rappresenta la prima release dopo una riscrittura completa del software Matita al fine di modificare il sistema logico su cui il software si basa e di sperimentare e testare qualitativamente e quantitativamente nuove soluzioni e algoritmi descritti nei lavori di ricerca degli autori. In particolare: A) e' stato implementato un nuovo kernel compatto per una nuova variante del Calcolo delle Costruzioni CoInduttive. Fra le modifiche piu' significative: una nuova rappresentazione compatta per le metavariabili che ottimizza sensibilmente il caso delle sostituzioni esplicite formate da un segmento di indici di de Brujin consecutivi; una nuova gestione algebrica degli universi, specificabili dagli utenti, che e' compatibile sia con la logica classica che con quella intuizionista; una nuova euristica per la conversione di lambda-termini che permette di limitare il numero di riduzioni non necessarie; proof irrelevance per gli argomenti proposizionali delle costanti che semplifica sensibilmente la programmazione con tipi dipendenti; eliminazione della ricorsione strutturale come oggetto di prima classe, al fine di aumentare sensibilmente le prestazioni della macchina di riduzione. B) e' stato implementato un nuovo motore di refinement che, a differenza del precedente, si basa su un algoritmo bi-direzionale per l'inferenza dei tipi che rende la type inference molto piu' efficace in caso di tipi dipendenti. Inoltre e' stata introdotta la nozione di ``vettore di argomenti impliciti''. Entrambe le modifiche hanno permesso di ridurre in maniera sensibile la complessita' e la quantita' di codice necessario per l'implementazione delle tattiche di base. E' stata inoltre proposta e implementata l'innovativa tecnica degli hint di unificazione per permettere all'utente di controllare l'algoritmo di unificazione in uno stile simile alla programmazione logica. Tale meccanismo ha sussunto diversi meccanismi ad-hoc presenti nella vecchia implementazione. C) riscrittura completa del codice di paramodulazione che ora si basa su una rappresentazione astratta del linguaggio dei termini. Matita ha anche ricevuto il riconoscimento come Best Newcomer nella competizione CASC22 (sezione paramodulazione) battendo diversi sistemi esistenti. D) implementazione di un sistema per l'estrazione di codice OCaml da prove costruttive.