lunedì 21/10/1996, ore 17, aula C

Piero Pagliani

Generalizzazione degli Spazi di Approssimazione di Pawlak tramite una estensione delle Algebre Modali di Relazioni

Abstract
Gli Spazi di Approssimazione permettono di calcolare le approssimazioni superiori ed inferiori di generici sottoinsiemi di un universo U, che non siano esattamente definibili tramite proprietà osservabili. Queste approssimazioni sono interpretabili, in termini logici, come le modalità "possibile" e, rispettivamente, "necessario" di uno spazio modale di tipo S5.
In questo seminario si affronterà il problema di approssimare, invece che semplici sottoinsiemi, relazioni binarie arbitrarie definite sull'universo U. Si dimostra, utilizzando un'estensione dell'interpretazione degli spazi modali come algebre di relazione, che occorre far ricorso ad un'algebra modale "non commutativa", dove le modalità sono definite da operatori strettamente connessi alle pre-implicazioni ed alle post-implicazioni della logica lineare non commutativa, ed alle pre-specificazioni e post-specificazioni più generali della semantica dei programmi di Hoare.
Sulla base di questi risultati sono state implementate funzioni di calcolo delle approssimazioni di carattere molto generale.

giovedì 21/11/1996, ore 17, aula I

Alberto Zanardo

Semantiche e Linguaggi per Logiche del Tempo e del Tempo Ramificato

Abstract
Verrà brevemente presentata la più comune logica "alla Prior" per il Tempo Lineare e verrà successivamente considerato il problema di definire un linguaggio e una nozione di verità adeguati per una rappresentazione "ad albero" del tempo, in cui, in accordo con l'indeterminismo, gli istanti temporali hanno un unico passato, ma possono avere più "possibili futuri".
In questo contesto, verranno considerate le logiche del tempo ramificato di tipo Peirceano ed Occamista, la cui semantica coinvolge una quantificazione (del secondo ordine) sull'insieme dei possibili futuri.
Verrà analizzato il potere espressivo dei linguaggi Peirceano ed Occamista, assieme a recenti proposte di estensioni di questi. Tali proposte sono giustificate sia dall'uso dei tempi verbali nei linguaggi naturali sia da alcune applicazioni della logica temporale in informatica ed in intelligenza artificiale.
Si accennerà in particolare alle logiche temporali CTL e CTL*, che sono la "controparte informatica" delle logiche Peirceana ed Occamista, in cui gli istanti temporali sono visti come "stati" in una computazione eventualmente non deterministica.
Nel corso del seminario verranno presentati alcuni risultati e problemi aperti riguardanti questioni di assiomatizzabilità, decidibilità e caratterizzabilità di strutture.

giovedì 12/12/1996, ore 17, aula B

Vincent Danos
(Joint work with Laurent Regnier (IML, CNRS))

Bridging the gap between games & coherence semantics for Linear Logic

Abstract
Games can be constructed, following Blass and Abramsky-Jagadeesan-Malacaria, in which Linear Logic proofs are interpreted as strategies and (head linear) cut-elimination as an interaction sequence between strategies.
These interaction sequences interleave moves in different basic games. If one forgets this interleaving in all interaction sequences in which a given proof takes part, then one gets its traditional coherence semantics interpretation.

giovedì 16/1/1997, ore 17, aula B

Paolo Lipparini

Nuove applicazioni degli ultrafiltri alla topologia

Abstract
E' ben noto che il prodotto di spazi topologici compatti è ancora compatto, ma certe proprietà più deboli della compattezza piena non sono conservate rispetto al prodotto. Ad esempio, esiste uno spazio topologico numerabilmente compatto il cui quadrato non è numerabilmente compatto (uno spazio si dice numerabilmente compatto se ogni ricoprimento numerabile ha un sottoricoprimento finito).
Varie caratterizzazioni degli spazi tutte le cui potenze sono numerabilmente compatte sono state trovate mediante l'uso di ultrafiltri; e analogamente per altre simili proprietà di compattezza.
Si mostra che, in un senso ben preciso, l'uso degli ultrafiltri è inevitabile nello studio di queste proprietà di compattezza.

giovedì 13/2/1997, ore 17, aula B

Marisa Venturini Zilli

Termini iterativi razionali

Abstract
Viene definita una lambda-notazione per la famiglia dei termini iterativi, che ha già ricevuto attenzione in ambito di computazioni simboliche.
Viene definita una semantica per la famiglia dei termini iterativi razionali e viene in particolare considerato il rapporto tra matching e unificazione.

giovedì 13/3/1997, ore 17, aula B

Anna Labella

Alberi e logica con modalità graduate

Abstract
Gli alberi a ramificazione finita vengono considerati come semantica per il comportamento di agenti di computazione e l'equivalenza osservazionale introdotta su questi ultimi è quella che corrisponde all'isomorfismo tra alberi. A questo punto si va alla ricerca di una logica che caratterizzi questa semantica nello stile di Hennessy-Milner, cioè tale che due processi sono equivalenti se e soltanto se verificano le stesse formule. Si trova che si può risolvere il problema considerando una versione positiva della logica modale con operatori graduati.

giovedì 17/4/1997, ore 17, aula B

F. W. Lawvere

Kinship and mathematical categories

Abstract
Those concepts which are historically stable tend to be those which in some way reflect reality. A concept which has enjoyed some historical stability for 40,000 years is the one involving ideas of genealogy and kinship. A more accurate model than heretofore possible of kinship can be sharpened with help of the modern theory of flexible mathematical categories.
Abstracting the genealogical aspect of a given society yields a mathematical structure within which aunts, cousins, etc. can be precisely defined. For example gender and moiety become labelling morphisms within that category. Topological operations, such as contracting a connected subspace to a point, are shown to permit rationally neglecting the remote past.
The logic of genealogy is not at all 2-valued nor boolean, because the truth-value space naturally associated with the ancestor concept has a rich lattice structure. A finitary approximation to this theory is also considered and the corresponding category of structures is fully analyzed.

giovedì 22/5/1997, ore 17, aula B

Rocco De Nicola

Testing Processes via Basic Observables

Abstract
We propose a general approach to define behavioural preorders over process terms by considering the precongruences induced by three basic observables. These observables provide information about the initial communication capabilities of processes and about their possibility of engaging in an infinite internal chattering.
We show that some of the observables-based precongruences do correspond to behavioral preorders long studied in the literature. The coincidence proofs shed light on the differences between well known preorder and on the role played in their definition by tests for internal chattering.