Warning: Table './church/sessions' is marked as crashed and last (automatic?) repair failed query: SELECT sid FROM sessions WHERE sid = 'jenddif3ra09jpe7gauq0716a1' 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

Measuring the Expressiveness of Rewriting Systems through Event Structures

Speaker:
Damiano Mazza
Quando:
21/05/2010 - 10:30
Dove:
Aula Verra, Facoltà di Lettere e Filosofia - Università Roma Tre, via Ostiense 234
Abstract

We develop a methodology for studying and comparing the expressiveness of computational models which are based on rewriting. We consider a class of rewriting systems, which we call normal, admitting a natural interpretation in terms of event structures; this is done by building up on work of Mazurkiewicz, Nielsen, Plotkin, Winskel, Melliès, and Mimram. Then, we introduce the notion of bisimilar embedding of event structures, which allows us to say when a computational system is "at least as expressive" as another one, as soon as these two are described in terms of event structures. Finally, we prove a few separation results for normal rewriting systems based on this notion, and we give an application of these to interaction nets and their non-deterministic variants, including Ehrhard and Regnier's differential interaction nets.


Armonie classiche per connettivi computazionali

Speaker:
Mattia Petrolo
Quando:
14/05/2010 - 11:30
Dove:
Aula Verra, Facoltà di Lettere e Filosofia - Università Roma Tre, Via Ostiense 234
Abstract

La teoria antirealista del significato sviluppata a partire dagli anni '70 da Dummett, Prawitz e Martin-Löf, stabilisce diversi desiderata che le regole logiche devono soddisfare affinché esse possano caratterizzare adeguatamente i connettivi logici. In particolare, il requisito di armonia impone un "equilibrio deduttivo" che apparentemente non può essere soddisfatto che dalle regole della logica intuizionista.

Nella prima parte del talk, mostriamo in che senso l'isomorfismo di Curry-Howard rispecchia fedelmente tali condizioni richieste ad un calcolo logico. All'interno di questo quadro teorico, analizziamo alcuni limiti degli approcci tradizionali alla nozione di armonia e proponiamo un criterio sufficiente per definire un connettivo logico. Tale criterio rende conto del fatto che le proprietà dei connettivi intuizionisti hanno una natura fondamentalmente computazionale.

Nella seconda parte del talk, esaminiamo alcune possibili strategie per estendere alla logica classica il criterio proposto. Questo costituisce un primo passo verso la possibilità di valutare l´importanza filosofica della "costruttivizzazione" della logica classica.


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



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 = 'jenddif3ra09jpe7gauq0716a1' in /var/www/church/includes/database.mysql.inc on line 121.', 2, '', 'http://logica.uniroma3.it/node?page=11', '', '18.207.255.67', 1728526590) in /var/www/church/includes/database.mysql.inc on line 121