Talk – Teoremi sociali con PostgreSQL

Abstract

I metodi formali permettono di comporre automaticamente le dimostrazioni al computer di teoremi di matematica, permettendo di fatto a più matematici di unire gli sforzi (in modo asincrono) verso obiettivi più ambiziosi.

Tali metodi sono ancora più importanti alla luce di risultati notevoli ottenuti di recente (cfr. [http://www.ams.org/notices/200811/]) e anche di progetti di enormi dimensioni (i.e. [https://code.google.com/p/flyspeck/]) che cercano di dare risposta a delle sfide sinora inedite ( [ Why give a formal proof of the Kepler Conjecture?])

In questo talk mostreremo come sia possibile implementare, usando PostgreSQL, una infrastruttura per la certificazione collaborativa di teoremi matematici basata sulle transazioni ACID, i linguaggi procedurali e le query ricorsive, e dotata di una interfaccia web versatile che incoraggia ulteriormente il lavoro di gruppo anche tramite dispositivi mobili quali i tablet.

slides:

Relatori

  • Marco Maggesi : Ricercatore in matematica presso Dipartimento di Matematica e Informatica “Ulisse Dini” dell’Università di Firenze, si occupa di geometria e di formalizzazione della matematica al computer.  Inoltre si interessa di fondamenti dei linguaggi di programmazione e, in particolare, della sintassi astratta per i linguaggi funzionali. Oltre alle pubblicazioni scientifiche del suo settore, ha realizzato varie librerie di matematica formalizzata con i proof assistants Coq, HOL Light e Isabelle.
  • Alberto Mancini: PhD in Matematica Applicata,  lavora all’Universita’ di Firenze dove si occupa dell’amministrazione delle risorse di calcolo del Dipartimento di Matematica ed Informatica “U.Dini” Dopo numerosi anni spesi facendo ricerca nel campo della Fisica Matematica e la Matematica Industriale Alberto si occupa adesso prevalentemente dello sviluppo di applicazioni web con il GWT Toolkit (complilatore da java a javascript) ed alle tecnologie web in generale lavorando anche come consulente e docente in corsi di HTML5, Java e Javascript, oltre naturalmente fi GWT.
  • Gianni Ciolli : Principal Consultant per 2ndQuadrant Italia, lavora con Software Libero e Open Source da più di 15 anni.È stato co-fondatore e presidente (2001-2004) del PLUG – Prato Linux User Group; ha organizzato varie edizioni del PostgreSQL day italiano, e nel 2013 è stato eletto nel consiglio di ITPUG – Italian PostgreSQL Users Group. Fa parte di 2ndQuadrant dal 2008, come sviluppatore, consulente e docente, e ha partecipato come speaker a conferenze su PostgreSQL in diversi paesi europei. Le sue competenze informatiche includono anche linguaggi funzionali e calcolo simbolico.Ha un dottorato di ricerca in Matematica ed è autore di pubblicazioni di ricerca in Geometria Algebrica, Fisica Teorica e Dimostrazioni Formali. È stato assegnista di ricerca e docente all’Università di Firenze. Abita attualmente a Londra, e tra gli altri suoi interessi ci sono musica, teatro, poesia e sport, in particolare l’Atletica leggera dove compete negli eventi multipli.

Link alle slide del talk

Contatti