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

Jump from Parallel to Sequential Proofs: Additives

Speaker:
Paolo Di Giamberardino
Quando:
19/04/2007 - 16:00
Dove:
Aula 19 -- Facoltà Lettere e Filosofia -- Università Roma Tre
Abstract

In a previous work, we introduced a framework for the proof nets of the multiplicative fragment of Linear Logic, where partially sequentialised nets are allowed. In this seminar we extend this result to include additives, using a definition of proof nets, called J-proof nets, which is the typed version of the L-nets of Faggian and Maurel.
In J-proof nets, we can characterize nets with different degrees of sequentiality, by gradual insertion of sequentiality constraints (jumps). As a byproduct, we obtain a simple proof of the sequentialisation theorem.

Pi-calculus in differential interaction nets

Speaker:
Thomas Ehrhard (joint work with Olivier Laurent)
Quando:
16/04/2007 - 13:30
Dove:
AUla 12, Facoltà Lettere e Filosofia, Università Roma Tre
Abstract

We propose a translation of a pi-calculus without sums nor replication/recursion into an untyped and essentially promotion-free version of differential interaction nets. We define a transition system of labeled processes and a transition system of labeled differential interaction nets. We prove that our translation from processes to nets is a bisimulation between these two transition systems. This shows that differential interaction nets are sufficiently expressive for representing concurrency and mobility, as formalized by the pi-calculus.

Interazionismo logico

Organizzatori:
Michele Abrusci
Jean-Baptiste Joinet
Inizio:
05/11/2006
Fine:
06/11/2006
Dove:
Facoltà Lettere e Filosofia - Università Roma Tre
Descrizione

Nelle scienze contemporanee ha acquisito un ruolo centrale il concetto di interazione tra processi (biologici, fisici, informatici, etc…). Da parte sua, la logica si è rinnovata attraverso il dialogo con l’informatica, proponendosi come una teoria generale dell’interazione. Inizialmente confinata agli ambienti più tecnici, questa problematica si sta estendendo a indagini filosofiche, promuovendo un approccio alternativo all’epistemologia del novecento, reimpostando il legame tra la logica e le scienze. Il recente convegno di Logica, Scienze e Filosofia che si è tenuto a Cerisy ­la ­Salle (settembre 2006), ha posto in modo programmatico questa apertura della logica al mondo Presentazione e discussione a cura di:

  1. Jean­Baptiste Joinet (UFR de Philosophie, Univ. Paris 1)
  2. Vito Michele Abrusci (Dip. Filosofia, Univ. Roma Tre)
Programma
Lista seminari

Concorrenza e reti di interazione differenziali

Docente:
Thomas Ehrard
Inizio:
10/04/2006
Fine:
18/04/2006
Dove:
Aula 15 - Facoltà di Lettere e Filosofia - Università Roma Tre
Descrizione

Lezioni di dottorato tenute da Thomas Ehrhard (Equipe Preuves, Programmes et Systèmes - CNRS UMR 7126 - Paris) all'interno del programma: Rete italo-francese di ricerca in logica e geometria del calcolo.

Geometria della logica

Organizzatori:
Michele Abrusci
Inizio:
27/04/2006
Fine:
28/04/2006
Dove:
Facoltà di Lettere e Filosofia Università Roma Tre
Descrizione

In occasione della discussione delle tesi di dottorato di Michele Pagani e Gabriele Pulcini, si terrà un incontro di studio di logica matematica, filosofia e informatica.
Programma
Lista seminari