Amministrazione trasparente

Le attività di ricerca saranno preferibilmente ma non necessariamente indirizzate verso i seguenti argomenti- esplorare i limit computazionali alla dimostrabilità finita, analizzando la complessità dell dimostrazioni di formalizzazioni di  teoremi combinatori  in sistemi di dimostrazione, con l'obiettivo di: (a) classificare i metodi di theorem proving a seconda della loro efficienza nel produrre tali dimstrazioni; (b) progettare algoritmi per la generazione automatica di dimostrazioni o porvare la loro impossibilità e collegare tali problemi con la complessità delle dimostrazioni- studio della potenza logica dei versioni finite di teoremi tipo Hindman. Tali teoremi coinvolgono una profonda connessione tra metodi logici combinatori e computazionali. in particolare si considererà lo studio (nel senso della reverse mathematics)  di alcune versioni ristrette e finite di tali teoremi.