Da Matita a Dedukti e ritorno

Girolimetto, Mattia (2023) Da Matita a Dedukti e ritorno. [Laurea], Università di Bologna, Corso di Studio in Informatica [L-DM270]
Documenti full-text disponibili:
[img] Documento PDF (Thesis)
Disponibile con Licenza: Creative Commons: Attribuzione - Non commerciale - Condividi allo stesso modo 4.0 (CC BY-NC-SA 4.0)

Download (194kB)

Abstract

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.

Abstract
Tipologia del documento
Tesi di laurea (Laurea)
Autore della tesi
Girolimetto, Mattia
Relatore della tesi
Scuola
Corso di studio
Ordinamento Cds
DM270
Parole chiave
Proof Assistant,Matita,Dedukti,Logical Framework
Data di discussione della Tesi
19 Luglio 2023
URI

Altri metadati

Statistica sui download

Gestione del documento: Visualizza il documento

^