giovedì 19/10/1995, ore 17, aula G

V. Michele Abrusci

Semantica delle dimostrazioni della logica lineare non commutativa

Abstract
Una semantica delle dimostrazioni per la logica lineare non commutativa, nella quale alle due implicazioni (post-implicazione e retro-implicazione) viene assegnato significato diverso, può essere ottenuta considerando bimoduli sopra spazi di coerenza.In questa maniera, la logica lineare non commutativa arriva ad avere tutte le buone proprietà godute dalla logica lineare commutativa (calcolo dei sequenti con teorema di cut-elimination, semantica delle fasi, reti dimostrative, semantica delle dimostrazioni).

giovedì 2/11/1995, ore 17, aula G

Giuseppe Longo

Sulle dimostrazioni di teoremi indimostrabili

Abstract
Si introdurrà la nozione di "prova generica", abituale in Matematica e poco discussa in Logica. Sempre in modo molto informale, si osserverà come il rapporto fra prova generica e "prova specifica" sia essenziale per capire l'indimostrabilità, in senso costruttivo, di alcuni asserti veri (e dimostrabili, dunque, in un senso più ampio). Cercando di accennare solo ai metateoremi e all'idea generale delle loro dimostrazioni, si citeranno come esempi la prova dei teoremi di "normalizzazione" e di Paris-Harrington.
La Teoria dei Tipi (o Teoria della Dimostrazione costruttiva) fornisce un quadro rigoroso per poter parlare di prove generiche. In modo molto introduttivo, ma più formale, si porranno le basi di tale teoria, giusto quanto sufficiente a presentare un'applicazione di un risultato recente, il Teorema di Genericità, alla nozione formale di prova generica.

giovedì 16/11/1995, ore 17, aula G

Alberto Pettorossi

Logic Program Derivation and Preservation of Completion

Abstract
We study the relationships between the correctness of logic program transformation and program termination. We consider definite programs and we identify some "invariants" of the program transformation process. The validity of these invariants ensures the preservation of the success set semantics, provided that the existential termination of the initial program implies the existential termination of the final program. We also identify invariants for the preservation of the finite failure set semantics.
We consider four very general transformation rules: definition introduction, definition elimination, iff-replacement, and finite failure. Many versions of the transformation rules proposed in the literature, including unfolding, folding, and goal replacement, are instances of the iff-replacement rule.
By using our proposed invariants which are based on Clark completion, we prove, for our transformation rules, various results concerning the preservation of both the success set and finite failure set semantics. By exploiting some powerful properties of the Clark completion, we are able to derive simple proofs of these preservation results.
These proofs are much simpler than those done by induction on the construction of the SLD-trees, like the ones proposed in the literature for related results.

giovedì 30/11/1995, ore 17, aula G

Piero Pagliani

Analisi algebrica di dimostrazioni: un semplice case study

Abstract
Come è noto, la negazione intuizionista e’ stata criticata come "non costruttiva" da Nelson e Vorob’ev, che hanno proposto quella che viene chiamata "Logica Costruttiva con Negazione Forte".
Questa logica e’ semanticamente caratterizzata dalla classe delle Algebre di Nelson. Se a questo sistema aggiungiamo un operatore modale T esprimente il concetto "essere classicamente valido" otteniamo una nuova logica con notevoli proprietà, caratterizzata semanticamente da una sottovarietà delle Algebre di Nelson, identificabile esaminando il ruolo logico giocato da un particolare parametro nella costruzione duale di dette algebre a partire da Algebre di Heyting.
Nel seminario cercheremo di analizzare in modo direttamente algebrico i passi della dimostrazione in calcolo naturale di una fondamentale proprietà dell’operatore T. In questo modo potremo anche mostrare la relazione tra questo operatore e i due endomorfismi presenti nelle algebre trivalenti di Lukasiewicz.

giovedì 14/12/1995, ore 17, aula G

Andre Scedrov

Linear logic proof games and optimization: an introduction

Abstract
There has been substantial progress in complexity theory in the past several years in obtaining the non-approximability of NP-complete and PSPACE-complete optimization problems. In this joint work with P.D.Lincoln and J.C.Mitchell we establish non-approximability for several optimization problems related to provability in NP-complete and PSPACE-complete fragments of propositional linear logic. We represent complexity-theoretic games such as interactive protocols in a move-by-move fashion as linear logic proof games.

giovedì 11/1/1996, ore 17, aula G

Pierluigi Crescenzi
[I risultati presentati nel seminario sono stati in parte ottenuti in collaborazione con Sergio De Agostino e Giancarlo Bongiovanni, ed in parte ottenuti da Luca Trevisan.]

Sulla complessità parallela di approssimazione di MAX SAT

Abstract
Il problema MAX SAT consiste nel trovare, data una formula Booleana in forma normale congiuntiva, un'assegnazione di valori di verità che soddisfi il massimo numero di clausole.
E' ben noto che tale problema è NP-hard e dunque non risolvibile in tempo polinomiale (a meno che P=NP).
Al tempo stesso, MAX SAT ammette un algoritmo polinomiale "3/4-approssimante" ovvero è possibile determinare in tempo polinomiale un'assegnazione che soddisfa un numero di clausole pari ad almeno 3/4 del massimo.
In questo seminario descriveremo alcuni risultati ottenuti relativamente all'approssimazione di MAX SAT in tempo polilogaritmico con un calcolatore parallelo. In particolare descriveremo prima un semplice algoritmo polilogaritmico 1/2-approssimante per MAX SAT. Quindi mostreremo come convertire una formula di MAX 2-SAT (in cui ogni clausola ha al più 2 letterali) in una equivalente soddisfacente una particolare proprietà locale di soddisfacibilità: in base a tale trasformazione svilupperemo, per ogni e>0, un algoritmo polilogaritmico (3/4-e)-approssimante per MAX 2-SAT. Infine, utilizzando tecniche simili potremo descrivere un algoritmo polilogaritmico 0.724-approssimante per MAX SAT che è quindi molto vicino come prestazioni al miglior algoritmo sequenziale.

giovedì 25/1/1996, ore 17, aula G

Giuseppe Jacopini

Enumerabilità dei termini di un lambda-calcolo tipato esteso

Abstract
E' stata definita in un lavoro precedente un'estensione del lambda-calcolo tipato la cui interpretazione risulta naturale. Si è dimostrata la completezza di tale lambda-calcolo esteso al livello più basso (ovvero sono rappresentabili le funzioni ricorsive). Si è iniziato a studiare le proprietà degli operatori di tipo più alto, in particolare il problema della enumerabilità dei termini di tipo assegnato.

giovedì 8/2/1996, ore 17, aula G

Gianfranco Mascari

Quantaloidi ed equazioni al punto fisso

Abstract
I quantaloidi sono categorie arricchite sui sup-semireticoli: queste strutture sono state studiate con motivazioni diverse in teoria delle categorie, informatica teorica, logica matematica ed analisi funzionale.
Le equazioni al punto fisso possono essere utilizzate per studiare gli algoritmi ed i sistemi dinamici.
Le equazioni al punto fisso le cui soluzioni sono bimoduli tra Q-categorie (Q è un quantaloide) sono di fondamentale inportanza nella matematica computazionale (e.g. algoritmi di ottimizzazione su grafi, nuclei risolventi di equazioni integrali).

giovedì 22/2/1996, ore 17, aula G

Anna Labella
(lavoro in collaborazione con Zoltan Esik)

Teorie dell' iterazione: una caratterizzazione equazionale dell'operatore di punto fisso

Abstract
Le teorie dell'iterazione, studiate da Bloom ed Esik, forniscono una trattazione assiomatica dell'operatore di punto fisso in categorie cartesiane. Se l'operatore di punto fisso sopra una categoria è definito per inizialità allora le sue proprietà equazionali sono le stesse di quelle delle teorie dell'iterazione. Il teorema principale si riduce a provare che se una 2-teoria algebricamente completa soddisfa la "identità parametrica", allora soddisfa tutte le equazioni di una teoria dell'iterazione.

giovedì 7/3/1996, ore 17, aula G

Paola D'Aquino

Equazioni di Pell in frammenti dell'aritmetica di Peano

Abstract
Svilupperemo la teoria delle equazioni di Pell in frammenti deboli dell'aritmetica e studieremo le relazioni che intercorrono fra le soluzioni di equazioni di Pell e la funzione esponenziale.

giovedì 21/3/1996, ore 17, aula G

Giambattista Amati
(lavoro svolto con Keith van Rijsbegen e Flavio Ubaldini)

Un’applicazione della teoria semantica dell'informazione: la selezione e il ritrovamento dell’informazione come processi di apprendimento.

Abstract
Un tipico problema dell'apprendimento automatico (Machine Learning = ML) consiste nella classificazione dei dati, a partire da una base iniziale di esempi (training set), in due classi concettuali (positiva e negativa). Diverse teorie, descritte in un linguaggio di rappresentazione, vengono indotte come possibili candidati a spiegare "al meglio" i dati.
L'obiettivo è di selezionare tra queste la teoria “migliore”. Esistono diverse tecniche di ordinamento delle teorie a partire dai dati iniziali (il metodo di Rissanen's Minimum Description Length Principle (MDL), il metodo di Wallace & Freeeman's Minimum Message Length, o la formula di Robertson Sparck Jones dell'information retrieval). In questo seminario si introduce un metodo generale che descrive tale situazione di apprendimento.
Questo metodo si applica in particolare all'information retrieval. Si considera infatti una parola chiave come una teoria, e i documenti osservati come il training set iniziale. Viene utilizzato il metodo di decisione Bayesiano secondo il quale la teoria migliore è quella che massimizza l'utilità aspettata. Usando tre differenti misure di informazione e regole di decisione, tra le quali quelle di Hintikka e Carnap, si ottengono nove funzioni di ordinamento per le teorie. I comportamenti non intuitivi del principio di MDL e del ranking tradizionale dell'IR vengono risolti. Un'applicazione di tale metodo al problema della selezione dell'informazione verrà descritta.

giovedì 18/4/1996, ore 17, aula G

Lorenzo Tortora de Falco

Verso un modello matematico delle dimostrazioni della logica classica

Abstract
La teoria dei modelli è quella parte della logica matematica il cui oggetto di studio è la denotazione degli enunciati matematici, e può quindi, attraverso il teorema di completezza, essere vista come una teoria matematica della dimostrabilità.
Più recentemente, l'interazione con l'informatica teorica (l'isomorfismo di Curry-Howard e la programmazione funzionale) ha portato i logici in teoria della dimostrazione ad interessarsi alle dimostrazioni di un enunciato oltre che alla dimostrabilità dello stesso, rimettendo così in primo piano una vecchia idea di Heyting: trovare dei modelli matematici per le dimostrazioni degli enunciati matematici. Lo studio di tali modelli per la logica intuizionista è ormai bene avviato, mentre fino a pochi anni fa non esisteva alcun tentativo convincente di interpretare all'interno di una struttura algebrica le dimostrazioni della logica classica.
Si cercherà di fare una panoramica dei recenti sviluppi in questo senso, utilizzando come strumento di analisi la Logica Lineare.

giovedì 2/5/1996, ore 17, aula G

Marco Pedicini

Riduzioni Virtuali Orientate: un approccio algebrico alla ottimalità nel lambda-calcolo

Abstract
In "Essays on Combinatory Logic, lambda-Calculus and Formalism" (1980) Jean Jaques Lèvy introdusse il concetto di riduzione ottimale del lambda-calcolo. Solo 10 anni dopo però John Lamping, un ingegnere, riuscì a descrivere una riduzione di grafi che ne rendesse possibile l'implementazione.
Nel 1988, indipendentemente, Jean Yves Girard propose un programma in tre punti per la sua Geometria dell'Interazione:
1) trovare modelli matematici nei quali rappresentare una classe significativa di algoritmi (intesi come specifica ed esecuzione);
2) studiare questi modelli per dedurre le proprietà logiche astratte che caratterizzano l'esecuzione degli algoritmi di cui al punto 1 (ad es. una nozione astratta di tipo);
3) ricavare dai punti 1 e 2 una nozione di macchina astratta (non troppo distante da quella concreta) che mostri la fattibilità dell'esecuzione espressa nel modello matematico.
Nel 1992, M.Abadi, G.Gonthier e J.J.Lèvy misero in luce lo stretto legame tra l'implementazione di Lamping e la Geometria dell'Interazione della logica lineare.
Proponiamo una riduzione per "redessi virtuali" (concetto introdotto da V.Danos e L.Regnier nel 1993) che mette in luce alcune proprietà matematiche della riduzione ottimale di Lamping utilizzando il modello dell'esecuzione fornito dalla Geometria dell'Interazione.

giovedì 16/5/1996, ore 17, aula G

Marisa Venturini Zilli

Termini iterativi e computazioni simboliche

Abstract
Viene definita una lambda-notazione per la famiglia dei termini iterativi, che ha già ricevuto attenzione in ambito di computazioni simboliche.
Vengono mostrate le buone proprietà computazionali dei termini iterativi, in particolare per quanto riguarda l'unificazione.

giovedì 30/5/1996, ore 17, aula G

Patrizia Mentrasti

Simulazione del flusso di veicoli nel traffico urbano mediante automi cellulari

Abstract
La crescente complessità del traffico urbano lo rende assimilabile ad un "sistema complesso"; viene qui descritto un approccio "microscopico" al problema della simulazione del flusso di veicoli che è nella sostanza completamente nuovo e si fonda sui nuovi paradigmi del calcolo parallelo sincronizzato iniziati da J. von Neumann e sviluppati in modo molto fecondo negli ultimi anni; in particolare si mostrano due modelli, uno che studia la sincronizzazione dei semafori e l'altro che simula i parcheggi dei veicoli in aree di stazionamento apposite. Questi modelli teorici sono stati anche realizzati su calcolatore e testati su situazioni reali della città di Roma.