Sviluppo di un interactive theorem prover in ELPI

In questo elaborato è discusso l'utilizzo del linguaggio Lambda Prolog, con interprete ELPI, per lo sviluppo di dimostratori interattivi. Nel primo capitolo viene introdotto Lambda Prolog, sono fornite indicazioni storiche sull'interactive theorem proving e descritto cosa ci si aspetta da un interactive theorem prover basato sull'isomorfismo di Curry-Howard. Le estensioni fornite da ELPI sono analizzate rispetto alla possibilità di facilitare l'implementazione di un dimostratore interattivo. Nel secondo capitolo è introdotta Minimalist Type Theory, analizzato il kernel implementato e su cui è stato costruito il lavoro sviluppato, con una trattazione dell'implementazione di un elaboratore e di un dimostratore interattivo. Per concludere, vengono analizzati pro e contro della soluzione proposta e i suoi possibili sviluppi futuri.