Benvenuto
Gruppo di Logica e Geometria della Cognizione
coordinatore: V. Michele Abrusci

 

Dipartimento di Matematica e Fisica
Università Roma Tre
Largo San Leonardo Murialdo 1
00144 Roma -Italia

 

Il fondamento scientifico della costituzione del gruppo risiede nell'interesse che tutti i suoi componenti portano alla moderna teoria della dimostrazione. Questo settore della logica matematica ha conosciuto recentemente una vera e propria "rinascita", dovuta al suo incontro con l'informatica: la corrispondenza di Curry-Howard stabilisce una corrispondenza tra dimostrazioni e programmi e tra esecuzione dei programmi ed eliminazione del taglio (un procedimento di trasformazione delle dimostrazioni ben noto ai logici). La scoperta di questa semplice e fondamentale corrispondenza è il punto di partenza per un nuovo approccio alla nozione di costruttività in logica ed alla programmazione in informatica.

In quest'ambito si colloca l'apparizione della logica lineare, che unisce gli aspetti "costruttivi" della logica intuizionista alle simmetrie della logica classica. La logica lineare nasce da un'analisi matematica molto fine della semantica delle dimostrazioni della logica intuizionista. Dalla sua apparizione nel 1986, essa si è imposta come strumento usato in vari settori di ricerca, dalla teoria della dimostrazione al lambda-calcolo, dalle macchine astratte al calcolo distribuito, dalla teoria della complessità alla programmazione logica.


News

Non-determinismi nelle reti d'interazione

Speaker:
Andrei Dorman
Quando:
27/05/2011 - 11:00
Dove:
Aula Verra, Facoltà di Lettere e Filosofia - Università Roma Tre, via Ostiense 234
Abstract


Espansione di Taylor dei lambda-termini ordinari e uniformità

Speaker:
Giulio Guerrieri
Quando:
20/05/2011 - 11:00
Dove:
Sala del Consiglio, Dipartimento di Filosofia - Università Roma Tre, via Ostiense 234
Abstract

Ehrhard e Regnier hanno definito l'espansione di Taylor di un lambda-termine ordinario come una combinazione lineare infinita di termini del lambda-calcolo con risorse. Il lambda-calcolo con risorse è una variante del lambda-calcolo ordinario in cui invece dell'applicazione ordinaria è presente un'applicazione "lineare". A livello logico, il lambda-calcolo con risorse corrisponde alle reti differenziali senza la promozione. Servendosi di una proprietà di uniformità, Ehrhard e Regnier hanno mostrato che la somma delle forme normali dei termini che compaiono nell'espansione di Taylor di un lambda-termine ordinario M è l'espansione di Taylor dell'albero di Böhm di M. Presenteremo brevemente tali risultati e uno degli attuali obiettivi di ricerca (ancora in fieri): caratterizzare la proprietà di uniformità nelle reti differenziali senza promozione.


The concept of Interaction. Crossovers among Biology, Logic and Philosophy

Organizzatori:
V. Michele Abrusci
Giulia Frezza
Inizio:
27/04/2011
Fine:
Dove:
Sala Conferenze, piano terra della Facoltà di Lettere e Filosofia - Università Roma Tre, via Ostiense 234
Descrizione

Come d'abitudine per il nostro Gruppo in occasione della discussione di una tesi di dottorato, è organizzato un workshop informale con la partecipazione dei membri della giuria e dei membri del nostro Gruppo che desiderino intervenire.

Il programma dettagliato della giornata è disponibile qui


Ontologies, Logic and Interaction

Organizzatori:
V. Michele Abrusci
Marco Romano
Inizio:
26/04/2011
Fine:
Dove:
Sala Conferenze, piano terra della Facoltà di Lettere e Filosofia - Università Roma Tre, via Ostiense 234
Descrizione

Come d'abitudine per il nostro Gruppo in occasione della discussione di una tesi di dottorato, è organizzato un workshop informale con la partecipazione dei membri della giuria e dei membri del nostro Gruppo che desiderino intervenire.

Il programma dettagliato della giornata è disponibile qui


La sintassi trascendentale: cosa è, che prospettive apre alla ricerca logica

Speaker:
V. Michele Abrusci
Quando:
04/03/2011 - 11:00
Dove:
Aula Verra, piano terra della Facoltà di Lettere e Filosofia -- Università Roma Tre, via Ostiense 234
Abstract


Les fondements à l'ère post-fondationnelle

Organizzatori:
Giuseppe Longo
Giulia Frezza
evento esterno
Inizio:
18/11/2010
Fine:
20/11/2010
Dove:
Amphi Darboux, Institut Henri Poincaré (IHP), Paris -- rue P. et M. Curie, 11 (vicino a rue d'Ulm), Parigi
Descrizione

Incontro annuale del gruppo LIGC (Logica e interazione, verso una geometria della cognizione)

Pagina ufficiale dell'Incontro


Ricerche logiche ed epistemologiche

Organizzatori:
Michele Abrusci
Teresa Numerico
Inizio:
09/07/2010
Fine:
Dove:
Aula Verra, Facoltà di Lettere e Filosofia - Università Roma Tre, via Ostiense 234
Descrizione

A conclusione delle attività nell’anno accademico 2009-2010, saranno presentati e discussi temi della ricerca logica ed epistemologica sui quali lavorano alcuni membri del gruppo di ricerca “Logica e Geometria della Cognizione” (coordinato dal prof. V. Michele Abrusci, Dipartimento di Filosofia).
Per ulteriori informazioni rivolgersi a tnumerico@uniroma3.it

Qui il programma stampabile


Negation and protological foundations for logic

Speaker:
Jean-Baptiste Joinet (Université Paris 1 Sorbonne-Panthéon)
Quando:
18/06/2010 - 14:00
Dove:
Aula 5, Villa Mirafiori, Via Carlo Fea 2, Roma
Abstract

Starting from the formalist/intuitionist debate about ideality of negation in the first third of the XXth century, I will investigate the
functional approaches of negation as a unary logical connective, leading to the contemporary interactional approaches of negation as a protological binary relation between processus. In these times where logical pluralism has become logical plethorism, I will conclude about the foundational rôle of this conception of negation for logic.


Measuring the Expressiveness of Rewriting Systems through Event Structures

Speaker:
Damiano Mazza
Quando:
21/05/2010 - 10:30
Dove:
Aula Verra, Facoltà di Lettere e Filosofia - Università Roma Tre, via Ostiense 234
Abstract

We develop a methodology for studying and comparing the expressiveness of computational models which are based on rewriting. We consider a class of rewriting systems, which we call normal, admitting a natural interpretation in terms of event structures; this is done by building up on work of Mazurkiewicz, Nielsen, Plotkin, Winskel, Melliès, and Mimram. Then, we introduce the notion of bisimilar embedding of event structures, which allows us to say when a computational system is "at least as expressive" as another one, as soon as these two are described in terms of event structures. Finally, we prove a few separation results for normal rewriting systems based on this notion, and we give an application of these to interaction nets and their non-deterministic variants, including Ehrhard and Regnier's differential interaction nets.


Armonie classiche per connettivi computazionali

Speaker:
Mattia Petrolo
Quando:
14/05/2010 - 11:30
Dove:
Aula Verra, Facoltà di Lettere e Filosofia - Università Roma Tre, Via Ostiense 234
Abstract

La teoria antirealista del significato sviluppata a partire dagli anni '70 da Dummett, Prawitz e Martin-Löf, stabilisce diversi desiderata che le regole logiche devono soddisfare affinché esse possano caratterizzare adeguatamente i connettivi logici. In particolare, il requisito di armonia impone un "equilibrio deduttivo" che apparentemente non può essere soddisfatto che dalle regole della logica intuizionista.

Nella prima parte del talk, mostriamo in che senso l'isomorfismo di Curry-Howard rispecchia fedelmente tali condizioni richieste ad un calcolo logico. All'interno di questo quadro teorico, analizziamo alcuni limiti degli approcci tradizionali alla nozione di armonia e proponiamo un criterio sufficiente per definire un connettivo logico. Tale criterio rende conto del fatto che le proprietà dei connettivi intuizionisti hanno una natura fondamentalmente computazionale.

Nella seconda parte del talk, esaminiamo alcune possibili strategie per estendere alla logica classica il criterio proposto. Questo costituisce un primo passo verso la possibilità di valutare l´importanza filosofica della "costruttivizzazione" della logica classica.