Da Matita a Dedukti e ritorno

Dedukti è un software che agisce da type checker per definizioni, enunciati e prove codificati nel calcolo che implementa. Quest’ultimo è sufficientemente espressivo da poter rappresentare anche altri calcoli. Questo rende Dedukti un framework logico con il quale è possibile sviluppare un sistema di codifica che converta nel suo linguaggio le dimostrazioni scritte per altri proof assistant. Inizialmente si effettua un’analisi del processo di esportazione del codice da Matita a Dedukti, Matita è un assistente alla dimostrazione sviluppato pres- so l’Università di Bologna, basato sul calcolo delle costruzioni (co)-induttive. Successivamente si illustra la funzionalità di importazione del codice Dedukti in Matita e si esaminano le sfide che si presentano nel ricostruire i termini originali di Matita, a partire dal codice Dedukti esportato in precedenza.