Seminario di Geometria: Alcuni risultati di topologia formale in Matita
Il dott. Claudio Sacerdoti Coen dell'Universita' di Bologna terra' un seminario dal titolo
Alcuni risultati di topologia formale in Matita
giovedi' 13 gennaio alle ore 14:30 nella Sala Conferenze "F.Tricerri".
Abstract:
Matita e' un dimostratore interattivo di teoremi sviluppato a Bologna dal gruppo di ricerca diretto dal Prof. Asperti. Esso e' basato sull'isomorfismo di Curry-Howard e implementa una variante del Calcolo delle Costruzioni (Co-)Induttive. In particolare, la prossima versione del sistema rendera' possibile la formalizzazione di risultati in Matematica Costruttiva e Predicativa (ove, cioe', la collezzione dei sottoinsiemi di un insieme dato forma una classe propria).
In questo talk mostreremo la formalizzazione in Matita di un importante risultato di topologia formale che proviene dall'ambito della Basic Picture, una nuova astrazione della topologia ad opera di Giovanni Sambin fortemente basata sulla Matematica Costruttiva e Predicativa. Il risultato asserisce l'esistenza di un funtore (full & faithful) fra due categorie di spazi topologici generalizzati. E' stato quindi necessario formalizzare in Matita alcune definizioni base di teoria delle categorie in logica costruttiva e predicativa.