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: Exponentials

Speaker:
Paolo Di Giamberardino
Quando:
07/05/2010 - 11:30
Dove:
Aula Verra, Facoltà di Lettere e Filosofia - Università Roma Tre, via Ostiense 234
Abstract

In previous works, by importing ideas from game semantics (notably Faggian-Maurel-Curien's ludics nets), we defined a new class of multiplicative/additive polarized proof nets, called J-proof nets. The distinctive feature of J-proof nets with respect to other proof net syntaxes, is the possibility of representing proof nets which are partially sequentialized, by using jumps (that is, untyped extra edges) as sequentiality constraints.

Starting from this result, in the present work we extend J-proof nets to the multiplicative/exponential fragment, in order to take into account structural rules: more precisely, we replace the familiar linear logic notion of exponential box with a less restricting one (called cone defined by means of jumps. As consequence, we get a syntax for polarized nets where, instead of a structure of boxes nested one into the other, we have one of cones which can be partially overlapping. Moreover, we define normalization for exponential J-proof nets, proving, by Gandy's method, that even in case of ''superposed'' cones, reduction enjoys confluence and strong normalization.


Un'applicazione del SAT-solver in bioinformatica

Speaker:
Marco Pedicini
Quando:
23/04/2010 - 11:30
Dove:
Aula Verra, Facoltà di Lettere e Filosofia - Università Roma Tre, Via Ostiense 234
Abstract

Lo studio di sistemi dinamici adatti alla descrizione dei sistemi biologici e' sempre stato di fondamentale interesse per le implicazioni che puo' avere nelle applicazioni in medicina. La possibilita' di accedere a dati sperimentali che rendono la descrizione dei fenomeni biologici con un livello di dettaglio che si spinge fino al livello molecolare, rendono necessario l'utilizzo di modelli interpretativi della realta' in grado di spiegare fenomeni complessi.

Nello studio del sistema immunitario abbiamo proposto una nuova metodologia per combinare
- database di letteratura specialistica (dataminig),
- serie temporali di dati di microarray,
- modello della dinamica meno accurato,

e fornire un modello piu' accurato per la descrizione del sistema di interazione tra geni che governa la reazione del sistema immunitario (differenziazione delle cellule T).

Lavoro in preparazione: M. Pedicini, F. Barrenas, T. Clancy, F. Castiglione, E. Hovig, K. Kanduri, D. Santoni, M. Benson. Combining network modeling and gene expression microarray analysis to explore the dynamics of Th1 and Th2 cell regulation.


Verso una logica dell'innovazione

Speaker:
Remo Pareschi
Quando:
26/03/2010 - 11:30
Dove:
Aula Verra, Facoltà di Lettere e Filosofia - Università Roma Tre, via Ostiense 234
Abstract


Arithmetic of Supersingular Koblitz Curves in Characteristic Three

Speaker:
Prof. Roberto Avanzi (Bochum, Germany)
Quando:
25/03/2010 - 11:00
Dove:
AULA 311, Dipartimento di Matematica dell'Università Roma Tre - Largo San Leonardo Murialdo, 1
Abstract

Roberto Avanzi (Bochum, Germany)
joint work with Clemens Heuberger (Graz, Austria)
and Helmut Prodinger (Stellenbosch, South Africa)

We consider digital expansions of scalars for supersingular Koblitz curves in characteristic three. These are expansions of integers to the algebraic base of TeX Embedding failed!, where TeX Embedding failed! is a zero of a polynomial TeX Embedding failed!. The obvious application of these expansions is to scalar multiplication on Koblitz curves.

A simple connection between TeX Embedding failed!-adic expansions and balanced ternary representations is given.

Windowed non-adjacent representations are considered whereby the digits are elements of minimal norm. We exploit the rotational symmetry of the digit set to reduce the memory requirements of scalar multiplication by a factor of six with respect to previous methods. Furthermore, we give an explicit description of the elements of the digit set, allowing for a very simple and efficient precomputation strategy.

Additionally, we explicitly describe the action of some endomorphisms on the Koblitz curve as a scalar multiplication by an explicitly given integer.


Alcune osservazioni sulle nozioni di verità e indecidibilità

Speaker:
Gabriele Pulcini
Quando:
19/03/2010 - 11:30
Dove:
Aula Verra, Facoltà di Lettere e Filosofia - Università Roma Tre, via Ostiense 234
Abstract


Sulla iniettività della semantica relazionale in MELL, 2

Speaker:
Lorenzo Tortora de Falco
Quando:
19/02/2010 - 11:30
Dove:
Aula Verra, Facoltà di Lettere e Filosofia - Università Roma Tre, Via Ostiense 234
Abstract


Sulla iniettività della semantica relazionale in MELL, 1

Speaker:
Daniel De Carvalho
Quando:
29/01/2010 - 11:30
Dove:
Aula Verra, Facolta' di Lettere e Filosfia - Universita' Roma Tre, Via Ostiense 234
Abstract


Semantica relazionale e tempo di calcolo, in logica lineare moltiplicativa

Speaker:
Giulio Guerrieri
Quando:
22/01/2010 - 12:15
Dove:
Aula Verra, Facoltà di Lettere e Filosofia - Università Roma Tre, Via Ostiense 234
Abstract


Linear Logic by asymmetric levels

Speaker:
Andrei Dorman
Quando:
22/01/2010 - 11:30
Dove:
Aula Verra, Facoltà di Lettere e Filosofia - Università Roma Tre, Via Ostiense 234
Abstract


Prime considerazioni su “LOGICOMIX: an epic search for truth”

Speaker:
Michele Abrusci
Quando:
15/01/2010 - 11:30
Dove:
Aula Verra, Facoltà di Lettere e Filosofia - Università Roma Tre, Via Ostiense 234
Abstract