Indagini in Deep Inference

Simonetto, Andrea (2010) Indagini in Deep Inference. [Laurea magistrale], Università di Bologna, Corso di Studio in Informatica [LM-DM270]
Documenti full-text disponibili:
[img]
Anteprima
Documento PDF
Download (532kB) | Anteprima

Abstract

La tesi è uno studio di alcuni aspetti della nuova metodologia “deep inference”, abbinato ad una rivisitazione dei concetti classici di proof theory, con l'aggiunta di alcuni risultati originali orientati ad una maggior comprensione dell'argomento, nonché alle applicazioni pratiche. Nel primo capitolo vengono introdotti, seguendo un approccio di stampo formalista (con alcuni spunti personali), i concetti base della teoria della dimostrazione strutturale – cioè quella che usa strumenti combinatoriali (o “finitistici”) per studiare le proprietà delle dimostrazioni. Il secondo capitolo focalizza l'attenzione sulla logica classica proposizionale, prima introducendo il calcolo dei sequenti e dimostrando il Gentzen Hauptsatz, per passare poi al calcolo delle strutture (sistema SKS), dimostrando anche per esso un teorema di eliminazione del taglio, appositamente adattato dall'autore. Infine si discute e dimostra la proprietà di località per il sistema SKS. Un percorso analogo viene tracciato dal terzo ed ultimo capitolo, per quanto riguarda la logica lineare. Viene definito e motivato il calcolo dei sequenti lineari, e si discute del suo corrispettivo nel calcolo delle strutture. L'attenzione qui è rivolta maggiormente al problema di definire operatori non-commutativi, che mettono i sistemi in forte relazione con le algebre di processo.

Abstract
Tipologia del documento
Tesi di laurea (Laurea magistrale)
Autore della tesi
Simonetto, Andrea
Relatore della tesi
Scuola
Corso di studio
Indirizzo
Curriculum A: Scienze informatiche
Ordinamento Cds
DM270
Parole chiave
Deep Inference, Proof Theory, Teoria della Dimostrazione, Cut elimination, Gentzen Hauptsatz
Data di discussione della Tesi
21 Ottobre 2010
URI

Altri metadati

Statistica sui download

Gestione del documento: Visualizza il documento

^