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

Dynamique discrète et structure des réseaux génétiques

Speaker:
Paul Ruet
Quando:
12/10/2007 - 10:00
Dove:
Studio 2.23 (studio di Lorenzo) - Dipartimento di Filosofia - Facoltà Lettere e Filosofia - Università Roma Tre - Via Ostiense 234 Roma
Abstract


Between interaction and semantics: visible acyclic nets

Speaker:
Michele PAGANI
Quando:
21/09/2007 - 08:00
Dove:
Aula 13 - Facoltà Lettere e Filosofia - Università Roma Tre - Via Ostiense 234 Roma
Abstract

We prove a strict correspondence between cut-elimination, acyclicity and denotational semantics in the framework of differential interaction nets with promotion (DIN for short). DIN is an extension of the multiplicative exponential linear logic (MELL) introducing differential operators for the exponentials.

We define the orthogonal TeX Embedding failed! of a net TeX Embedding failed! with conclusion TeX Embedding failed! as the set of all nets TeX Embedding failed! with a conclusion TeX Embedding failed! s.t. the cut between TeX Embedding failed! and TeX Embedding failed! is weak normalizable. Then, we introduce in DIN visible acyclicity, a geometric condition which in usual MELL characterizes those proof-structures which correspond to cliques in coherence spaces. Moreover, we consider finiteness spaces, a generalization of coherence spaces which are at the base of the differential extension of MELL.

Let TeX Embedding failed! be a cut-free net with conclusion TeX Embedding failed!, our results prove that the following conditions are equivalent:

1. TeX Embedding failed! contains all visible acyclic nets with a conclusion TeX Embedding failed!
2. TeX Embedding failed! is visible acyclic
3. TeX Embedding failed! is a finitary relation in the finiteness space associated with TeX Embedding failed!

These equivalences provide a generalization of the ones in the main theorems of the theory of linear logic proof-nets, namely: Bechét's theorem (TeX Embedding failed!), weak normalization theorem (TeX Embedding failed!), semantic soundness theorem (TeX Embedding failed!) and Retoré's theorem (TeX Embedding failed!). Above all, it discloses a deep unity in DIN between normalization, visible acyclicity and finiteness spaces, which was present (even if never actually remarked) only in the multiplicative fragment of linear logic.


TBA

Speaker:
Daniel de Carvalho
Quando:
09/07/2007 - 13:00
Dove:
Aula 12 - Facoltà Lettere e Filosofia - Università Roma Tre - Via Ostiense 234 Roma
Abstract


The use of phase semantics: to make sense out of nonsense

Speaker:
Kazushige TERUI (National Institute of Informatics, Tokio, Japan)
evento esterno
Quando:
23/05/2007 - 16:00
Dove:
Aula 12 - Facoltà Lettere e Filosofia - Università Roma Tre - Via Ostiense 234 Roma
Abstract

Phase semantics (Girard 87) and its intuitionistic/noncommutative variants (Abrusci, Okada, Sambin, Troelstra, etc.) are provability semantics for linear logic and its variants. While they are sometimes considered "abstract nonsense" (or at least uninteresting from the viewpoint of computation), one cannot deny that it has a wide range of applications. For instance:

Undecidability (Lafont)
Decidability via finite model property (Lafont, Okada-Terui, Galatos-Jipsen)
Cut-elimination (Okada, Kanovitch-Okada-Scedrov, Belardinelli-Jipsen-Ono)
Denotational completeness (Girard, Streicher)
Conservativity (Kanovitch-Okada-Terui, Hamano-Takemura)
Criteria for cut-elimination (Terui, Ciabattoni-Terui)
Interpolation and amalgamation properties (Terui)
Polarity and Focalization

Thus phase semantics is a good tool for applications, and it is still useful to study it. In this talk, I will survey some uses of phase semantics and try to extract general patterns, hoping that it will lead to more applications and establishment of phase semantics as a solid, concrete and sensible tool.


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)

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.