Sviluppo di un interactive theorem prover in ELPI

Piemontese, Cristiano (2018) Sviluppo di un interactive theorem prover in ELPI. [Laurea magistrale], Università di Bologna, Corso di Studio in Informatica [LM-DM270]
Documenti full-text disponibili:
[img] Documento PDF (Thesis)
Disponibile con Licenza: Creative Commons: Attribuzione - Non commerciale - Condividi allo stesso modo 3.0 (CC BY-NC-SA 3.0)

Download (457kB)

Abstract

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.

Abstract
Tipologia del documento
Tesi di laurea (Laurea magistrale)
Autore della tesi
Piemontese, Cristiano
Relatore della tesi
Scuola
Corso di studio
Indirizzo
CURRICULUM A: TECNICHE DEL SOFTWARE
Ordinamento Cds
DM270
Parole chiave
interative theorem proving,dimostrazione interattiva,programmazione logica,lambda prolog,ELPI,isomorfismo Curry-Howard,teoria dei tipi
Data di discussione della Tesi
20 Dicembre 2018
URI

Altri metadati

Statistica sui download

Gestione del documento: Visualizza il documento

^