Implementazione e visualizzazione di alberi di deduzione naturale in Lean a supporto della didattica della logica

Durante i laboratori del corso di logica per l’informatica del primo anno, viene utilizzato Lean 4, un linguaggio di programmazione per la dimostra- zione assistita per permettere agli studenti di approcciarsi alla scrittura di prove formali. Tuttavia, durante le esercitazioni a lezione, si adotta anche un approccio grafico basato sugli alberi di deduzione naturale. Questo lavoro di tesi propone lo sviluppo di un ponte tra le due modalità di visualizzazione delle prove logiche. A questo scopo, è stato progettato e realizzato in Lean un widget in grado di tradurre automaticamente le dimostrazioni in Lean in alberi di deduzione naturale e visualizzarle.