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

Collusions : toward an agonal ontology

Speaker:
Jean-Baptiste Joinet (Université Lyon 3 - Centre Cavaillès, ENS, Paris)
Quando:
02/05/2018 - 11:00
Dove:
Dipartimento di Matematica e Fisica, Lgo S. Leonardo Murialdo 1, palazzina C, aula 311 (terzo piano)
Abstract

In Frege and Russell’s line, the main tool to propagate ontology toward higher orders is realized by quotienting sets by equivalence relations. Indeed, this leads to produce, at the next order, separated individualities (disjoint non empty subsets covering the original set) and this in such a way that this separation is conceptually generated from a relation at the initial order.
This way to relate ontology and equivalence relations is deeply Parmenidian in inspiration : non only because it considers individualities independently of time (first point), but also because it propagates at the next order the idea of an autonomy of individualities, i.e. the idea that the individuality of individuals is independent of any relational commitment between them (second point).
"Denotational semantics of programs" (the research programme launched by Strachey and Scott around 1969) can be seen as a first step to substitute to Parmenidian ontology an Heraclitean ontology, in the sense that it faces the first point (individualities in time): in a computational universe, transformation comes first and separation phenomenas are generated by (and compatible with) these transformation.
In that talk, I will present my current work on a complementary program toward a non Parmenidian ontological point of view facing the second point (Agonal ontology) which starts by introducing a generalization of equivalence relations, collusions (total and surjective collusive relations). After having presented their main properties, notably with respect to the partitioning purpose, I will conclude about logical potential interpretations.


Dalle prove sintattiche alle combinatorial proofs

Speaker:
Matteo Acclavio (LIX - INRIA Parsifal Team)
Quando:
23/03/2018 - 14:30
Dove:
Dipartimento di Matematica e Fisica, Università degli Studi Roma Tre, largo San Leonardo Murialdo,1 - Pal.C - AULA 311
Abstract

In questo incontro studieremo come le combinatorial proofs di Hughes possono essere utilizzate per definire una nozione di equivalenza tra dimostrazioni per la logica classica. Mostreremo poi come diversi formalismi (calcolo dei sequenti, alberi di refutazione e resolution) possano essere tradotti in combinatorial proofs e quale nozione di identità viene definita da ciascuno di essi.


Negative local feedbacks in Boolean networks

Speaker:
Paul Ruet (CNRS, IRIF, Université Paris-Diderot)
Quando:
23/03/2018 - 11:00
Dove:
Dipartimento di Matematica e Fisica, Università degli Studi Roma Tre, largo San Leonardo Murialdo,1 - Pal.C - AULA 311
Abstract

We shall be interested in the asymptotic dynamical properties of Boolean networks: fixed points, attractive cycles, and more general attractors. While the properties of Boolean networks without local cycle or without local positive cycle are rather well understood, recent literature raises the following two questions about networks without local negative cycle. Do they have at least one fixed point? Should all their attractors be fixed points? We give negative answers to both questions: we show that and-nets without local negative cycle may have no fixed point, and that Boolean networks without local negative cycle may have (antipodal) attractive cycles.


Periodic structure of graph dynamical systems on maxterm and minterm Boolean functions.

Speaker:
Jose C. Valverde (Università di Castiglia-La Mancia)
Quando:
07/12/2017 - 11:00
Dove:
Dipartimento di Matematica e Fisica, L.go S. Leonardo Murialdo 1, Aula 211
Abstract

The emergence of the concepts of cellular automata (CA) (Wolfram, 1983, 1984, 1986) and Boolean (BN) network (Kauffman, 1969), between the end of the 60s and early 80s, for the formalization of computational processes and genetic regulation, respectively, was a first step in the development of modeling of evolutionary phenomena using networks. This type of modeling has been useful to solve various problems in other Sciences such as Chemistry (see Kier & Seybold, 2009; Kier, Seybold & Cheng 2005; Scalise & Schulman, 2015), Physics (see Chopard & Droz, 1998), Biology (see Deutsch & Dormann, 2004, Toroczkai & Güçlü, 2007), Ecology (see Dieckman, Law & Metz, 2000; Hofbauer & Sigmund, 2003; Hogeweg, 1988), even of Social Sciences like Psychology or Sociology (see Abraham, 2015; Kempe, Kleminberg & Tardos, 2005).
This new paradigm of modeling has evolved in recent years, giving rise to the concept of graph dynamical system (GDS), which generalizes the previous ones, since it contemplates that the relationships among elements of the system can be arbitrary. That is, the graph representing the relations among elements of the system, called dependency graph, could be arbitrary. In this generalization, the smallest units of aggregation of the phenomenon are called nodes (or vertices), in relation to their membership in the graph, relieving the term of cells in a CA and entities in a BN.
In this talk, we discuss some of the advances in the study of the periodic structure of a GDS when the evolution operator is a maxterm or minterm Boolean function.


Una interpretazione di CCS nella ludica

Speaker:
Stefano Del Vecchio (Università Roma Tre - Université Paris Nord)
Quando:
24/11/2017 - 11:00
Dove:
Dipartimento di Matematica e Fisica, Palazzina C, Aula 311
Abstract

Starting from works aimed at extending the Curry-Howard correspondence to process calculi through linear logic, we give another Curry-Howard counterpart for Milner's Calculus of Communicating Systems (CCS) by taking Ludics as the target system. Indeed interaction, Ludics' dynamic, allows to fully represent both the non-determinism and non-confluence of the calculus. CCS processes are interpreted into carefully defined behaviours of Ludics using a new construction, called directed behaviour, that allows controlled interaction paths by using pruned designs. Execution of processes is characterized as interaction on behaviours, by implicitly representing the causal order and conflict relation of event structures. As a direct consequence, we are also able to interpret deadlocked processes, and identify deadlock-free ones.


A characterization of head-normalization through some intersection type systems and the relational model via Taylor expansion

Speaker:
Federico Olimpieri (Université d'Aix-Marseille)
Quando:
06/10/2017 - 11:00
Dove:
Dipartimento di Matematica e Fisica, L.go S. Leonardo Murialdo 1, Palazzina C, Aula 311
Abstract

Via the Taylor expansion of lambda terms it is possible to provide an innovative proof of the head-normalization theorem for the relational model.
Thanks to this result we can also state in a very natural way the equivalence between the relational model and some intersection type systems.


Numeration 2017

Organizzatori:
Vilmos Komornik
Marco Pedicini
Inizio:
05/06/2017
Fine:
09/06/2017
Dove:
Università Roma Tre -- Argiletum Via Madonna dei Monti 40 Sala Urbano VIII
Descrizione

The goal of this workshop is to bring together researchers interested in interactions between numeration systems, ergodic theory, number theory and combinatorics.


Le teorie del ragionamento nella prospettiva dei due processi: la distinzione tra processi inferenziali intuitivi e riflessivi

Speaker:
Massimo Marraffa
Quando:
12/05/2017 - 11:30
Dove:
Dipartimento di Matematica e Fisica, Aula 311, pal. C, l.go S. Leonardo Murialdo 1
Abstract

Secondo le teorie ‘dei due sistemi’, il sistema cognitivo umano sarebbe composto da almeno due sottosistemi. Il Sistema 1 opera in modo inconscio e rapido, producendo risposte intuitivamente cogenti a problemi di apprendimento e ragionamento. Il Sistema 2 opera invece in modo cosciente e lento, entrando in azione solo quando il soggetto è indotto a svolgere un compito inferenziale in modo riflessivo.
Nel mio intervento solleverò due obiezioni a questa famiglia di teorie. 
(1) L’immagine di due sistemi neurocognitivi che esistono l’uno accanto all’altro e competono per il controllo del comportamento dell’agente ha scarsa plausibilità evoluzionistica: perché mai l’evoluzione invece di modificare, estendere o integrare l’architettura del preesistente S1, avrebbe ricominciato tutto da capo con S2? Più plausibile è allora l'ipotesi che i processi di S2 siano realizzati in quelli di S1 . Ossia non vi sono due sistemi distinti, bensì due livelli o strati di processi cognitivi, l’uno dipendente dalle operazioni dell’altro. In quest’ottica, non occorre supporre che l’evoluzione abbia fortemente arricchito l’architettura di S1 per far nascere S2; basta immaginare che i sottosistemi di S1 siano stati orchestrati e utilizzati in modi nuovi.
(2) Ammettiamo la realtà della distinzione fra processi di ragionamento intuitivi e riflessivi; e accogliamo la congettura che il ragionamento riflessivo sia in larga misura realizzato dalle operazioni cicliche di processi intuitivi inconsci (fra cui i sottosistemi normalmente assegnati a S1). Ciò non equivale però a una conferma dell’ipotesi dei due sistemi; e questo perché -- è stato sostenuto -- la distinzione fra S1 e S2 non coincide con la distinzione fra ragionamento intuitivo e ragionamento riflessivo.


Laver tables

Speaker:
Patrick Dehornoy (Université Caen-Normandie)
Quando:
17/02/2017 - 11:30
Dove:
Dipartimento di Matematica e Fisica, Aula 311 Largo San Leonardo Murialdo, 1
Abstract

Discovered (or invented?) by Richard Laver in the 1990s, the tables that are now known as Laver tables are finite structures obeying the self-distributivity law x(yz)=(xy)(xz). Although their construction is totally explicit, some of their combinatorial properties are (so far) established only using unprovable set theoretical axioms, a quite unusual and paradoxical situation. We shall explain the construction of Laver tables, their connection with set theory, and their potential applications in low-dimensional topology via the recent computation of some associated cocycles.


Proof Diagrams for Multiplicative Linear Logic: Syntax and Semantics

Speaker:
Matteo Acclavio (Université de Caen)
Quando:
10/02/2017 - 11:30
Dove:
Aula 311 (Palazzina C, Dipartimento di Matematica e Fisica, l.go S. Leonardo Murialdo 1)
Abstract

Le reti di prova sono una sintassi per le prove della logica lineare con una rappresentazione geometrica intuitiva che permette di definire una relazione di equivalenza tra derivazioni meno fine rispetto alla pura equivalenza sintattica.
In questo incontro daremo una sintassi bidimensionale alternativa per le derivazioni della logica lineare moltiplicativa. Nel nostro caso, la sintassi dei diagrammi di corde permette la definizione di un formalismo in cui verificare se un diagramma corrisponde ad una prova può essere verificato in tempo lineare.
Inoltre mostreremo come questa sintassi possa essere utilizzata per definire una semantica denotazionale per la logica lineare moltiplicativa con unità tramite classi di equivalenza di diagrammi (generata da una riscrittura terminante).