giovedì 13/11/1997, ore 17, aula F

Piero Pagliani

Comportamenti logici locali e globali: riesame di alcune logiche a più valori dal punto di vista delle informazioni incomplete

Abstract
L'analisi di dati e concetti imprecisi è uno dei maggiori filoni di ricerca in Computer Science ("Soft Computing" e "Knowledge Discovery in Database", "Control Theory"). A tal fine sono stati proposti diversi sistemi teorici di "Approximate Reasoning", come la Teoria dei Fuzzy Sets e la Teoria dei Rough Sets alle quali corrispondono interessanti modelli logico-algebrici.
In questo seminario si partirà dalla constatazione ovvia, benchè finora poco esplicitata in termini matematici, che in ogni sistema di "Approximate Reasoning" coesistono due diversi aspetti: uno riguardante i dati esatti e l'altro i dati imprecisi che si presentano normalmente mischiati nei sistemi d'informazione. Ne segue che una analisi "globale" di tali sistemi non può essere considerata soddisfacente. Viene quindi qui proposta un'analisi che tenga conto sia degli aspetti complessivi "globali", che portano a logiche a più valori e si riferiscono alle informazioni imprecise, sia di quelli "locali" che sono descrivibili dalla logica classica in quanto si riferiscono alla parte esatta delle nostre informazioni.
Questa analisi verrà sviluppata utilizzando in modo naturale le topologie di Grothendieck e gli operatori di Lawvere-Tierney, introdotti per poter governare matematicamente il concetto di validità locale.

giovedì 11/12/1997, ore 17, aula F

Marco Pedicini

Modello finito della Geometria dell'Interazione per la Logica Lineare Elementare, parte I

Abstract
In "Light linear logic" (Logic and computational complexity, Indianapolis, IN, 1994, LNCS 960, 145--176, Springer, 1995), J.-Y. Girard ha introdotto il sistema della logica lineare elementare (ELL) e della light linear logic (LLL), derivati indebolendo l'insieme degli isomorfismi che caratterizzano i connettivi esponenziali della logica lineare.
I due calcoli ottenuti hanno una cut elimination intrinsecamente limitata (rispettivamente elementare e polinomiale). Anche il potere espressivo di questi calcoli cattura le rispettive classi di complessità poiché essi permettono di rappresentare le funzioni elementari e polinomiali.
Mostreremo alcuni risultati a proposito della semantica della riduzione in ELL sviluppati a partire dal lavoro: Pedicini M., Remarks on Elementary Linear Logic (Preliminary Report) (A Special Issue on the Linear Logic 96, Tokyo Meeting, Electronic Notes in Theoretical Computer Science, Volume 3, Elsevier, 1996).

giovedì 15/1/1998, ore 17, aula F

Paolo Lipparini

Sulle giustificazioni degli assiomi di ZFC, e di possibili estensioni

Abstract
Esiste (con opportune precisazioni) un consenso abbastanza generalizzato fra i matematici sull'uso degli assiomi di ZFC come ambiente adatto per sviluppare la matematica. E' ben noto che ZFC è incompleta, anche per quanto riguarda questioni di importanza matematica. E' stupefacente che, di fronte all'ampio consenso riscosso dalla teoria ZFC, le opinioni su come estenderla siano estremamente discordanti.
Si cerca quindi di analizzare le motivazioni addotte in favore di ZFC (una rassegna recente si può trovare su P.Maddy, Believing the axioms I, II, JSL 53, 481-512 e 738-764). Si tenta di sostenere la tesi che queste motivazioni sono più che altro argomenti addotti a posteriori, che non giustificano ZFC (o che perlomeno non conducono necessariamente alla scelta di ZFC fra tante possibili teorie), e che in realtà ZFC è piuttosto una codificazione della pratica matematica (dell'inizio del secolo). (Solo di recente sono state prese in seria considerazione le forti connessioni tra lo sviluppo della teoria degli insiemi e l'evoluzione della pratica matematica; vedi A.Kanamori, Bull. ASL Vol 2 N.1).

giovedì 12/2/1998, ore 17, aula F

Marco Pedicini

Modello finito della Geometria dell'Interazione per la Logica Lineare Elementare, parte II

Abstract
Nella prima parte del seminario sono stati discussi gli aspetti di rappresentabilita' e di complessita' connessi alla sintassi di ELL [1], in questa seconda parte verranno esposti i risultati legati agli aspetti operazionali ed in particolare si parlera' della ricerca di una connessione esplicita tra complessita' e semantica della riduzione.

[1] Girard, Jean-Yves: Light linear logic (Logic and computational complexity Indianapolis, IN, 1994, 145-176, Lecture Notes in Comput. Sci., 960, Springer, Berlin, 1995).
[2] Pedicini, Marco: Remarks on Elementary Linear Logic (Preliminary Report). (A Special Issue on the Linear Logic 96, Tokyo Meeting, Electronic Notes in Theoretical Computer Science Volume 3, Elsevier, 1996)

giovedì 19/3/1998, ore 17, aula F

Anna Labella

Bisimulazione e logica

Abstract
Il concetto di bisimulazione si basa su un teorema di punto fisso ma, nei diversi modelli, l'operatore coinvolto può assumere un significato propriamente logico. In questo seminario verrà esposta l'approccio di Joyal-Nielsen-Winskel, ma anche un modo alternativo di affrontare il problema.

giovedì 23/4/1998, ore 17, aula F

Paola D'Aquino

Campi finiti non standard nell'induzione limitata

Abstract
Verranno studiati i campi finiti costruiti su modelli non standard dell'aritmetica di Peano. Presentero' quanto dei risultati classici sui campi finiti puo' essere riprodotto. Infine esaminero' il piccolo teorema di Fermat nell'aritmetica limitata.

giovedì 7/5/1998, ore 17, aula F

Roberto Maieli

Calcolo dei sequenti unificati ad una sola parte

Abstract
Nel 1993 Jean-Yves Girard ha introdotto la LOGICA UNIFICATA. La pricipale novita' era data da un unico Calcolo dei Sequenti (LU, ispirato ai "Sistemi Focalizzati Diadici" di J.M.Andreoli, 1990), dove la Logica Classica, Intuizionista e Lineare apparivano come frammenti del Calcolo, cioe', come particolari classi di Formule e Sequenti.
Questo originale calcolo aveva pero' l'inconveniente di essere 'piuttosto esteso perche' usava una formulazione a due parti per accomodare la logica intuizionista in modo piu' esplicito e perche' c'erano connettivi classici, intuizionisti e lineari...'(J.-Y. Girard).
Noi mostreremo come e' possibile superare tale inconveniente formulando un Calcolo dei Sequenti Unificati ad una sola parte (LU1) equivalente a quello originale ma di gran lunga piu' piccolo. Fare cio' comporterebbe la perdita della regola della negazione di LU, e di conseguenza la perdita delle simmetrie logiche del calcolo. Usando pero' la negazione lineare e' possibile ricostruire l'originale negazione di LU, con il risultato che tutte le simmetrie originali vengono preservate.
Il Calcolo LU1 ammette una cut-elimination che fa usodi semplici ipotesi come quella di 'grado di una di un cut' (che dipende solo dal numero di esponenziali prenessi alla formula) e di 'altezza lineare' di una dimostrazione.
In piu', la natura di 'sistema focalizzato' appare in LU1 piu' esplicita rispetto al Calcolo LU di Girard.

giovedì 28/5/1998, ore 17, aula F

Maurizio Proietti
(lavoro in collaborazione con Alberto Pettorossi, Universita' di Roma 2)

Una strategia generica per la derivazione automatica dei programmi logici

Abstract
La metodologia di trasformazione dei programmi si prefigge di derivare in modo automatico programmi corretti ed efficienti da specifiche formali.
Considereremo l'approccio basato su regole e strategie, che permette di separare il problema della correttezza da quello dell'efficienza: le regole di trasformazione assicurano la correttezza del programma derivato rispetto alle specifiche (e rispetto ad una determinata semantica), mentre le strategie di trasformazione combinano diverse regole al fine di derivare programmi con migliori caratteristiche computazionali.
In letteratura sono state presentate diverse strategie per la trasformazione di programmi logici (i.e. insiemi di clausole di Horn).
Mostreremo come tali strategie possano essere ottenute raffinando un'unica strategia generica, cioe' una strategia parametrizzata rispetto ad alcune strategie sussidiarie. La nostra strategia generica corrisponde al calcolo di un punto fisso di un opportuno operatore sull'insieme delle clausole di Horn. Oltre a consentire una comprensione teorica migliore, il nostro approccio fornisce strumenti concreti per la definizione di nuove strategie di trasformazione dei programmi e per l'analisi delle proprieta' di dette strategie.