Implementazione del linguaggio dichiarativo in Matita 0.99.x

In questo lavoro di tesi verra discussa l'implementazione del linguaggio dichiarativo del dimostratore interattivo di Teoremi Matita nella versione 0.99.x. Il linguagigo dichiarativo è una feature offerta da diversi dimostratori interattivi di teoremi, che permette di condurre la dimostrazione assistita al calcolatore mediante un linguaggio simile al linguaggio naturale. Questa feature ha applicazioni interessanti nell'utilizzo di Matita da parte di personale poco specializzato della dimostrazione assistita, e all'Università di Bologna viene utilizzato per la didattica della Logica Matematica.