La tesi introduce la logica intuizionista da un punto di vista informatico in modo da poter osservare la corrispondenza di Curry-Howard: la relazione tra questo tipo di logica e la Teoria della calcolabilità. Grazie a questi risultati è stato possibile sviluppare dei proof assistant: sistemi informatici utili per la dimostrazione di prove matematiche. Si vedranno infine degli esempi, scritti in Agda.
Presentazione della logica intuizionista
CAROLI, FLAVIO
2021/2022
Abstract
La tesi introduce la logica intuizionista da un punto di vista informatico in modo da poter osservare la corrispondenza di Curry-Howard: la relazione tra questo tipo di logica e la Teoria della calcolabilità. Grazie a questi risultati è stato possibile sviluppare dei proof assistant: sistemi informatici utili per la dimostrazione di prove matematiche. Si vedranno infine degli esempi, scritti in Agda.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
915804_tesicaroli.pdf
non disponibili
Tipologia:
Altro materiale allegato
Dimensione
373.27 kB
Formato
Adobe PDF
|
373.27 kB | Adobe PDF |
I documenti in UNITESI sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
Utilizza questo identificativo per citare o creare un link a questo documento:
https://hdl.handle.net/20.500.14240/81144