Warning: Table './church/sessions' is marked as crashed and last (automatic?) repair failed query: SELECT sid FROM sessions WHERE sid = 'jqre6bku9sq6rq2lm009ugv9l0' in /var/www/church/includes/database.mysql.inc on line 121
Gruppo di Logica e Geometria della Cognizione

 

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

Informal workshop on advances in Linear Logic proof nets

Organizzatori:
Lorenzo Tortora de Falco
Paolo Di Giamberardino
Inizio:
18/04/2008
Fine:
18/04/2008
Dove:
Facoltà di Lettere e Filosofia, via Ostiense, 234 - 00144 Roma
Descrizione

Discussion on the themes of proof-nets and their differential version (differential proof-nets). We have planned by now only a few number of structured talks:
- Damiano Mazza "Linear Logic by Levels and Bounded Time Complexity"
- Paolo Tranquilli "A characterization of MALL hypercoherent semantic correctness"
More information will follow.


Dimostrazioni, Polarità e Cognizione

Organizzatori:
Lorenzo Tortora de Falco
Inizio:
17/04/2008
Fine:
15/04/2008
Dove:
Sala Professori della Facoltà di Lettere e Filosofia, via Ostiense, 234 - 00144 Roma
Descrizione

Incontro di Logica in occasione della discussione delle tesi di dottorato in Filosofia e Teoria delle Scienze Umane di Paolo Di Giamberardino e Maria Teresa Medaglia.


Conferenza per il 60° compleanno di Jean-Yves Girard

Organizzatori:
LIGC
evento esterno
Inizio:
13/12/2007
Fine:
13/12/2007
Dove:
Foyer dell'Aula Magna della Facolta' di Lettere e Filosofia di Roma Tre.
Descrizione


Logica del secondo ordine: una lettura dei teoremi di incompletezza di Godel

Docente:
Vito Michele Abrusci
Inizio:
15/11/2007
Fine:
06/12/2007
Dove:
Sala del consiglio - Dipartimento di Filosofia - Facoltà Lettere e Filosofia - Università Roma Tre - Via Ostiense 234 Roma
Descrizione

Ciclo di lezioni all'interno del corso di dottorato in "Filosofia e Teoria delle Scienze umane".


Unprovability after Goedel

Speaker:
Lorenzo Carlucci
evento esterno
Quando:
12/11/2007 - 14:00
Dove:
Dipartimento Informatica - Via Salaria 113 - third floor - Seminari Lecture Room
Abstract

Since Goedel's famous discovery of the existence of an undecidable sentence in (first-order) Peano Arithmetic in 1931, the relevance of the incompleteness phenomena for so-called "mainstream" mathematics has been intensively debated. The question roughly was: since Goedel's undecidable propositions are mathematically meaningless, does the incompleteness phenomenon matter for "normal mathematics" at all?

A breakthrough occured in the late Seventies, with the discovery by Paris and Harrington that a seemingly innocent variant of the finite Ramsey Theorem is unprovable in Peano Arithmetic (while the finite Ramsey Theorem is provable in a much weaker system).

From then on, a large number of other (more or less) "natural" combinatorial statements have been found to be unprovable in stronger and stronger systems of arithmetic, analysis and even set-theory. Among the high points of this research is Harvery Friedman's proof that Robertson and Seymour's "Graph Minor Theorem" is unprovable from a strong (impredicative) system.

In other terms, many combinatorial theorems have been proved to be provable *only* under the assumption of some unexpectedly strong axiom of infinity.

We will give an overview of past and present research in the study of (arithmetic) unprovability. Research in this area features an interplay between proof theory, recursion theory, model theory, combinatorics, number theory etc. The basic concepts and proof techniques will be illustrated, as well as the current directions of research.

BIOGRAPHICAL SKETCH
Lorenzo Carlucci is currently affiliated with the Computer Science Department of the University of Rome "La Sapienza", as a Research Associate. He is also a Research Fellow of the "Scuola Normale Superiore di Pisa". He got his Ph.D. in Theoretical Computer Science at the "Computer and Information Sciences Department" of the University of Delaware, USA. He got his Ph.D. in Mathematics (spec. Mathematical Logic and Theoretical Computer Science) at the Mathematics Department of the University of Siena. His research interests include Mathematical independence results, proof theory, ordinal analysis and Recursion-theoretic learning theory.
http://www.cis.udel.edu/~carlucci/


A gentle introduction to 2-dimensional algebra and string diagrams

Docente:
Paul-André Melliès (CNRS-Université Paris 7)
Inizio:
28/10/2007
Fine:
04/11/2007
Dove:
Facoltà di Lettere e Filosofia - Università Roma Tre
Descrizione

Organizzazione del corso: Si tratta di un corso di 8 ore (2 ore al giorno i lunedi` 29, martedi` 30 e mercoledi` 31 ottobre ed il lunedi` 5 novembre). Gli orari precisi delle lezioni sono sulla pagina del corso.

Riassunto: In this introductory course, I will explain the basic concepts of 2-dimensional algebra, this including monoidal categories, the Yang-Baxter equations, Hopf algebras, trace operators, Kan extensions, Lawvere theories and operads, weighted limits, etc.
My ambition is to demonstrate how this 2-dimensional theory enables to reformulate a good part of algebra in a purely diagrammatic language, similar to flow charts in Programming Languages and to current notations for proofs in logic. Important point: my course is interactive, and will thus freely adapt to the wishes of the audience.


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.



Warning: Can't find file: 'watchdog' (errno: 2) query: INSERT INTO watchdog (uid, type, message, severity, link, location, referer, hostname, timestamp) VALUES (0, 'php', 'Table './church/sessions' is marked as crashed and last (automatic?) repair failed\nquery: SELECT sid FROM sessions WHERE sid = 'jqre6bku9sq6rq2lm009ugv9l0' in /var/www/church/includes/database.mysql.inc on line 121.', 2, '', 'http://logica.uniroma3.it/node?page=15', '', '44.220.251.236', 1728500177) in /var/www/church/includes/database.mysql.inc on line 121