giovedì 22/10/1992, ore 17, aula E

Piero Pagliani

Una applicazione della dualità di Sendlewski per le algebre di Nelson alla logica ed alla rappresentazione della conoscenza, via spazi di approssimazione

Abstract
Negli ultimi anni si sono sviluppati due approcci alla Rappresentazione della Conoscenza, basati sulla polarità <intensione, estensione> : i "Concept Lattices" di Wille e gli "Approximation Spaces" di Pawlak. In particolare la nozione di "rough set" è stata presa come base per una semantica per le logiche della conoscenza e dell'apprendimento. In questo seminario in particolare si analizzeranno le proprietà algebriche dell'operatore K(A) (operatore di conoscenza per il soggetto cognitivo A) alla luce dei recenti risultati di dualità per le algebre di Nelson (modelli per la logica con negazione forte). Saranno in questo modo analizzabili le trasformazioni dei modelli algebrici quando si aggiungano o cancellino informazioni e quando si postuli esplicitamente la decidibilità degli enunciati atomici.

giovedì 5/11/1992, ore 17, aula E

Gianfranco Mascari , Marco Pedicini

Il paradigma di Curry-Howard per il lambda-calcolo puro: eliminazione del taglio ed estrazione di sottotermini

Abstract
Il paradigma di Curry-Howard:

può essere esteso al lambda-calcolo puro.
La logica lineare permette un’analisi più fine della funzionalità (D = ! D --o D) ed inoltre consente di introdurre delle equivalenze tra dimostrazioni del calcolo dei sequenti che danno luogo alle reti di dimostrazioni.
Un nuovo approccio logico al lambda-calcolo viene offerto dal calcolo delle reti di dimostrazione: la riduzione viene vista come eliminazione del taglio. Una delle proprietà fondamentali del lambda-calcolo puro, l' "internalizzazione dell’estrazione di un sottotermine" viene analizzata, per la prima volta, da un punto di vista logico.

giovedì 19/11/1992, ore 17.30, aula E

Rocco De Nicola

Equivalenze comportamentali e logiche modali

Abstract
Saranno introdotte diverse nozioni di equivalenza per sistemi di transizione etichettati che identificano sistemi concorrenti e non-deterministici che non presentano differenze "osservabili". Delle equivalenze introdotte saranno anche date caratterizzazioni in termini di logiche modali, in particolare temporali.

giovedì 3/12/1992, ore 17, aula E

Silvio Maracchia , Paolo Freguglia

Momenti di storia della logica

Abstract
Maracchia : Le origini della logica sono strettamente connesse a quelle della matematica razionale; spesso gli stessi personaggi (Parmenide, Platone, Aristotele,...) operano nell'uno e nell’altro campo a testimonianza di un comune atteggiamento: la fiducia nella ragione e nel metodo deduttivo per il conseguimento della "verità". Non tutti però sono dello stesso avviso.
Freguglia : Gli studi algebrico-logici, che si andarono sviluppando nella seconda metà dell'Ottocento e nel primo Novecento sulla scia dell’opera booleana, ebbero anche in Italia, con Peano e la sua scuola (C.Burali Forti, A.Padoa, G.Vailati), interessanti sviluppi e sistemazioni. Ma anche altri matematici italiani, non appartenenti alla scuola peaniana, si dedicarono sempre in quel periodo a questi studi: in particolare ci soffermeremo su Alfonso Del Re.

giovedì 17/12/1992, ore 17, aula E

V. Michele Abrusci

Connettivi per lo scambio, nella logica lineare noncommutativa

Abstract
Alla logica lineare noncommutativa (intuizionista o classica), nella quale è assente la regola di scambio, possono essere aggiunti due nuovi connettivi ("ovunque" , "comunque"): una formula "ovunque" può muoversi in avanti o indietro nello spazio delle assunzioni, una formula "comunque" può muoversi in avanti o indietro nello spazio delle conclusioni. Con l’aggiunta di questi nuovi connettivi si ha una logica con la stessa forza della logica lineare commutativa di Girard, ma con maggiore potere espressivo. Per il calcolo dei sequenti ottenuto vale il teorema di cut-elimination, e anzi la dimostrazione di questo teorema getta una nuova luce sul significato della regola di taglio (cut-rule) come regola di comunicazione tra input/output o assunzione/conclusione.

mercoledì 13/1/1993, ore 16, aula E

Gianni Rigamonti

Alcuni aspetti del pensiero di Cantor

Abstract
Ci sono, nel pensiero di Georg Cantor, due aspetti centrali che appaiono estremamente interessanti ma anche molto problematici: il processo di formazione dei numeri transfiniti (I) e la concezione del continuo (II).
I. Cantor postula un "secondo principio di produzione" dei numeri interi in base al quale ogni successione monotona ascendente, anche non convergente, ha un limite. Ma in realtà fa uso, inavvertitamente, di assunzioni ancora più forti.
II. La concezione cantoriana del continuo travalica la matematica per investire la teoria della conoscenza e addirittura la metafisica. Si può dimostrare che alla sua base ci sono forti riferimenti a Leibniz e, al di là di Leibniz, ai presocratici.

mercoledì 13/1/1993, ore 17, aula E

Giambattista Amati

Logica temporale per il ragionamento con defaults

Abstract
Agli inizi degli anni ottanta l'Intelligenza Artificiale ha lanciato la sfida di fondare un paradigma di ricerca in logica nel quale si potessero trattare gli aspetti dinamici del ragionamento. Logiche modali ed intuizioniste, opportunamente concepite, possono a tal fine essere utilizzate per descrivere in modo generale processi inferenziali nei quali l'informazione viene cumulata. Più in particolare si mostrerà come il ragionamento per defaults è immergibile in una logica temporale (si fornisce una traduzione del default in una particolare logica temporale). Questo risultato fornisce una semantica chiara ed immediata al default reasoning, alternativa alle semantiche "esterne" ed artificiose di Shoham ed Etherington.

giovedì 28/1/1993, ore 17, aula E

Franco Montagna

Alcuni aspetti dei fenomeni di speed up in sistemi formali per l'Aritmetica

Abstract
Un problema importante nello studio delle lunghezze di dimostrazioni è quello di accorciare le dimostrazioni in un sistema formale senza produrre nuovi teoremi. Questo fenomeno si può verificare quando si usano dimostrazioni al second’ordine (di formule al primo ordine), quando si modifica opportunamente il sistema di assiomi, o infine quando si modificano le regole di inferenza. Lo speed up by provability è il fenomeno in base al quale alcune dimostrazioni si accorciano se si dimostra la dimostrabilità di una formula invece della formula stessa. Verranno dati esempi di teoremi aventi un significato matematico o metamatematico immediato la cui dimostrabilità è superesponenzialmente più corta da dimostrare di quanto non lo sia il teorema stesso.

giovedì 11/2/1993, ore 17, aula E

Corrado Böhm

Ricorsione senza punto fisso

Abstract
Autoriferimento, autoappartenenza e autoapplicazione sono stati forieri prima di paradossi poi di progresso. E' noto che funzioni o funzionali definiti da equazioni ricorsive sono punti fissi di operatori espressi mediante i parametri delle equazioni. Nel lambda-calcolo, in più esistono combinatori in grado di esprimere la soluzione di "qualsiasi" equazione al punto fisso. Essi hanno tuttavia un carattere infinitario, simile a un processo di limite, quindi il loro uso non facilita i calcoli concreti. Nella conferenza verrà illustrato con esempi il teorema della risolubilità di un'ampia classe di equazioni funzionali (su naturali, su sequenze di..., su alberi etichettati da...) mediante lambda-termini in forma normale evitando combinatori del punto fisso, ma con l'uso essenziale dell'auto-applicazione. Gli esempi sono espressi nel linguaggio della CuCh-machine, veicolo della programmazione funzionale e il cui modo di operare con "ambienti" è basato sul teorema suddetto.

giovedì 25/2/1993, ore 17, aula E

Ugo de' Liguoro

Sistemi di assegnamento di tipi disgiuntivi per il lambda-calcolo puro

Abstract
Si presentano alcune estensioni dei sistemi di tipi di Curry e intersezione mediante l'uso di una forma di disgiunzione finitaria e, successivamente, con una forma di disgiunzione infinitaria (tipi esistenziali). Si esaminano alcune conseguenze di tali estensioni sia concernenti la riduzione che la teoria dei modelli per il lambda-calcolo puro.

giovedì 11/3/1993, ore 17, aula E

Paolo Lipparini

Algebra Universale ed Algebra

Abstract
Recentemente è stata sviluppata una Teoria del Commutatore per strutture algebriche generali (nel caso dei gruppi essa corrisponde al commutatore di sottogruppi normali; nel caso degli anelli commutativi al prodotto fra ideali). Questa teoria mostra, sorprendentemente, che alcuni concetti sviluppati in teoria dei gruppi e in teoria degli anelli sono in realtà esempi (in maniera non banale !) di uno stesso concetto più generale; allo stesso modo, ad esempio, in cui (molto più banalmente) sottogruppi normali corrispondono ad ideali bilateri, cioè a congruenze (nuclei di omomorfismi).
Si sosterrà la tesi (non troppo popolare) che interazioni fra algebra e algebra universale, almeno in qualche caso, possono essere fruttuose per entrambi i settori.

giovedì 25/3/1993, ore 17, aula E

Egon Börger

A Mathematical Model for Full Prolog

Abstract
We present a formal semantics of the full language PROLOG as emerging from the ISO WG17 standardization effort. Our description uses the notion of evolving algebras as recently proposed by Y.Gurevich which allow to directly reflect the dynamic (and resource-bounded) aspects of computation. The proposed formal semantics for PROLOG, far from being hopelessly complicated, unnatural or machine-dependent, is simple, natural, abstract and in particular supports the process oriented understanding of programs by programmers.
Our specific aim is to provide a mathematically precise but simple framework in which standards can be defined rigorously and in which different implementations may be compared and judged.We will also report on further applications of this model to PROLOG compilation and to logic programming languages which include features for constraints, types or concurrency.

mercoledì 21/4/1993, ore 17, aula E

Claudio Bernardi

Relazioni non fondate e dintorni

Abstract
(a) Facendo riferimento a insiemi in cui sono definite relazioni non fondate si ottengono paradossi, più o meno noti, diversi come struttura dal paradosso del mentitore.
(b) Un teorema di punto fisso permette, in un certo senso, definizioni autoreferenti. In opportuni contesti topologici e logici sembrano possibili anche definizioni infondate.

giovedì 6/5/1993, ore 17, aula E

Claudio Pizzi

Logica condizionale classica e gradi di olismo

Abstract
Viene difesa la tesi secondo cui le logiche condizionali di Stalnaker-Lewis si possono interpretare molto naturalmente come logiche che rispecchiano visioni più o meno fortemente olistiche della realtà. Questa interpretazione rende più trasparente la differenza tra questi sistemi e i sistemi condizionali “consequenzialisti”, in cui si assume che i condizionali esprimano un nesso consequenziale tra antecedente e conseguente.
Alla luce di questa premessa filosofica vengono esaminati tre sistemi condizionali di potenza deduttiva crescente, il terzo dei quali - chiamato C2Pr - è una variante probabilistica dei più noti sistemi C1 e C2 dovuti rispettivamente a Lewis e Stalnaker. Si cerca quindi di esplicitare il grado di “coinvolgimento olistico” di ciascuno di questi, in base a considerazioni semantiche.
Si fa vedere inoltre che la misura del grado di coinvolgimento olistico di questi sistemi può essere espressa in almeno due modi differenti - mediante equivalenze di particolare forma e mediante disgiunzioni di particolare forma - le quali hanno in comune il fatto di esprimere forme indebolite del collasso delle modalità.

martedì 18/5/1993, ore 17, aula I

Jean-Yves Girard

Linear logic

Abstract
Linear logic is a refinement of intuitionistic logic, inspired by linear algebra. Contrary to intuitionistic or classical logic, linear logic does not deal with truths but with resources. This is the basis for possible applications in computer science.
Mathematically speaking, semantics of linear logic sets up various geometrical problems: e.g. denotational semantics, but also the theory of proof-nets which leads to the geometry of interactions.
Logically speaking, linear logic can help to unify logic in a single system.

giovedì 20/5/1993, ore 17, aula E

Giovanni Sambin

Il programma di Camerino, versione 1.1

Abstract
Il programma di Camerino (perché a Camerino è stato esposto per la prima volta nell'aprile 92) è di vedere, data una teoria degli insiemi di base molto affidabile e meccanizzabile come la teoria intuizionistica dei tipi di Martin-Löf, quali principi si devono aggiungere per poter sviluppare una versione costruttiva dei vari rami della matematica. Più concretamente, si aggiunge ad ITT una nozione di sottoinsieme, che si dimostra conservativa e che permette di sviluppare un approccio alla topologia "pointfree", basato sulla nozione di copertura.
Si illustrano le definizioni, i risultati e alcune delle applicazioni attuali di tale approccio.
Infine, si offrono alcune impressioni sulla rilevanza fondazionale del programma.

giovedì 3/6/1993, ore 17, aula E

Alessandro Berarducci
(in collaborazione con B. Intrigila)

Alcuni nuovi risultati sulle estensioni coerenti del lambda-calcolo

Abstract
Dati due lambda-termini chiusi A e B, consideriamo il problema se sia possibile aggiungere coerentemente al lambda-beta-calcolo l'equazione A=B. Il problema in generale è algoritmicamente indecidibile, tuttavia se assumiamo che A sia uno “0-termine” possiamo dare delle buone condizioni sufficienti affinché A=B sia coerente. Come applicazione otteniamo alcuni risultati controintuitivi tra cui:
1) esiste un lambda-termine chiuso X che si può coerentemente uguagliare ad ogni altro termine chiuso tranne che all'identità lambda-x.x
2) esiste un lambda-termine chiuso X che non si può coerentemente uguagliare al combinatore di punto fisso di Curry Y, ma si può coerentemente uguagliare ad ogni forma normale chiusa. In particolare la uguagliabilità ad ogni forma normale chiusa non garantisce la uguagliabilità ad ogni termine chiuso.