Matita 0.5.8

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 al nostro Subversion repository. Matita e' scritto in OCAML. La dimensione attuale dell'applicazione si aggira sulle 120.000 linee di codice. Con la versione 0.5.8 inizia la 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 pubblicati nel 2009. 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 partecipato per la prima volta alla competizione CASC22 (sezione paramodulazione) battendo diversi sistemi esistenti e vincendo il premio come Best Newcomer.