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

Una rilettura logica d'alcuni problemi di metodo in linguistica e in scienze sociali

Speaker:
Antonio Mosca
Quando:
08/05/2009 - 11:00
Dove:
Aula Verra, Facoltà di Lettere e Filosofia - Università Roma Tre, Via Ostiense 234
Abstract


Reti di prova tra determinismo e non determinismo

Organizzatori:
Lorenzo Tortora de Falco
Paolo Tranquilli
Inizio:
24/04/2009
Fine:
Dove:
Facoltà di Lettere e Filosofia Università Roma Tre via Ostiense 234
Descrizione

Workshop informale in occasione della discussione di dottorato di Paolo Tranquilli.


La dinamica del vivente

Speaker:
Giulia Frezza
Quando:
17/04/2009 - 11:00
Dove:
Aula Verra, Facoltà di Lettere e Filosofia - Università Roma Tre, Via Ostiense 234
Abstract

La dinamica del vivente - Alcuni elementi critici per lo studio del vivente da un punto di vista procedurale


Ricostruire una rete di prova dal suo sviluppo di Taylor

Speaker:
Michele Pagani
Quando:
03/04/2009 - 11:00
Dove:
Aula Verra, Facoltà di Lettere e Filosofia - Università Roma Tre, Via Ostiense 234
Abstract

Ricostruire una rete di prova dal suo sviluppo di Taylor (lavoro in comune con Christine Tasson).

La logica lineare (LL) è basata sull'analogia tra la linearità in algebra (i.e. commutazione con somme e prodotti con scalari) e la linearità in informatica (i.e. utilizzo dei dati di entrata esattamente una volta). Portando avanti tale analogia, Ehrhard e Regnier hanno introdotto la logica lineare differenziale (DiLL) -- un'estensione di LL con operatori differenziali. In questo contesto la promozione (l'analogo in logica dell'esponenziale) può essere approssimata da una somma di reti differenziali per mezzo di una nozione di sviluppo di Taylor.

Presenteremo un algoritmo per definire l'inverso dello sviluppo di Taylor. Più precisamente, definiremo un sistema di riscrittura (merging reduction) in grado di ricostruire da una somma finita S di reti differenziali, una rete di prova R con promozione se e solo se S è contenuta nell'espansione di Taylor di R. L'algoritmo è non-deterministico, valido e completo. Termineremo mostrando la stretta relazione tra una proprietà di confluenza della merging reduction e il problema dell'iniettività della semantica relazionale per la logica lineare.

http://www.pps.jussieu.fr/%7Emichele/taylorLL.pdf


Semantica denotazionale per la logica lineare a livelli

Speaker:
Damiano Mazza
Quando:
27/03/2009 - 11:00
Dove:
Aula Verra, Facoltà di Lettere e Filosofia - Università Roma Tre, Via Ostiense 234
Abstract

Semantica denotazionale per la logica lineare a livelli (lavoro in collaborazione con Pierre Boudes e Lorenzo Tortora de Falco)

In un lavoro recente con Patrick Baillot, abbiamo introdotto una nuova caratterizzazione logica del tempo elementare basata sulla cosiddetta logica lineare a livelli (L3), più generale di quella introdotta da Girard basata su ELL (nel senso che ELL è un sottosistema proprio di L3, che si ottiene eguagliando due parametri strutturali - profondità e livello - che sono in generale distinti nelle proof net di L3).
In questo talk presenterò un quadro categorico per la definizione di modelli denotazionali di L3 a partire da modelli della logica lineare.


Costruzione concorrente di reti di prova e sistemi transazionali

Speaker:
Roberto Maieli
Quando:
20/03/2009 - 11:00
Dove:
Aula Verra, Facoltà di Lettere e Filosofia - Università Roma Tre, Via Ostiense 234
Abstract


Logica, cognizione e dimostrazioni visive

Speaker:
Mario Piazza
Quando:
06/03/2009 - 14:00
Dove:
Aula Verra, Facoltà di Lettere e Filosofia - Università Roma Tre, via Ostiense 234
Abstract


Algebre di von Neumann, shift registers e complessità

Speaker:
Marco Pedicini
Quando:
27/02/2009 - 14:00
Dove:
Aula Verra, Facoltà di Lettere e Filosofia - Università Roma Tre, Via Ostiense 234
Abstract


Una misura semantica del tempo di esecuzione in logica lineare

Speaker:
Lorenzo Tortora de Falco
Quando:
13/02/2009 - 14:00
Dove:
Aula Verra, Facoltà di Lettere e Filosofia - Università Roma Tre, Via Ostiense 234
Abstract

"Una misura semantica del tempo di esecuzione in logica lineare" (lavoro in collaborazione con D. De Carvalho e M. Pagani)


Lezioni per la ricerca in logica

Docente:
V. Michele Abrusci
Inizio:
04/03/2009
Fine:
15/05/2009
Dove:
Aula 16 (ore 16-18). Facoltà di Lettere e Filosofia - Università Roma Tre, Via Ostiense 234
Descrizione

Introduzione critica alla logica lineare e ai suoi sviluppi
Lezioni di sintesi: 6, 13 e 20 marzo 2009.

Esposizione critica della teoria della dimostrazione del ‘900
Lezioni di sintesi: 27 marzo, 3 e 17 aprile 2009.

Le branche della logica nel XXI secolo
Lezioni di sintesi: 8 e 15 maggio 2009.