Implementazione del linguaggio dichiarativo in Matita 0.99.x

Berlingieri, Andrea (2019) Implementazione del linguaggio dichiarativo in Matita 0.99.x. [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 - Condividi allo stesso modo 3.0 (CC BY-SA 3.0)

Download (1MB)

Abstract

In questo lavoro di tesi verra discussa l'implementazione del linguaggio dichiarativo del dimostratore interattivo di Teoremi Matita nella versione 0.99.x. Il linguagigo dichiarativo è una feature offerta da diversi dimostratori interattivi di teoremi, che permette di condurre la dimostrazione assistita al calcolatore mediante un linguaggio simile al linguaggio naturale. Questa feature ha applicazioni interessanti nell'utilizzo di Matita da parte di personale poco specializzato della dimostrazione assistita, e all'Università di Bologna viene utilizzato per la didattica della Logica Matematica.

Abstract
Tipologia del documento
Tesi di laurea (Laurea)
Autore della tesi
Berlingieri, Andrea
Relatore della tesi
Scuola
Corso di studio
Ordinamento Cds
DM270
Parole chiave
Logica,Proof Assistant,Matita,Curry-Howard,Lambda Calcolo tipato
Data di discussione della Tesi
16 Ottobre 2019
URI

Altri metadati

Statistica sui download

Gestione del documento: Visualizza il documento

^