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

Alberto Pettorossi
(joint work with M.Proietti, IASI-CNR)

Synthesis of Programs from Unfold/Fold Proofs

Abstract
We address some issues related to the use of equivalence formulas for transforming and synthesizing logic programs.
In the first part we describe a program transformation method based on the unfold/fold rules which can be used for proving that a given first order equivalence formula of the form: All x [Ex y F(x,y) <-> Ex z G(x,z)], where F and G are conjunctions of atoms, is true in the least Herbrand model of a given program. Equivalence formulas of that form can be used to perform goal replacement steps, which allow us to transform clauses by replacing goals by equivalent ones while preserving the least Herbrand model. We provide some simple conditions ensuring total correctness of the goal replacement steps.
In the second part we show how the unfold/fold proof method described in the first part can be applied for solving synthesis problems which can be formulated as follows. Let us consider a program P and an equivalence formula of the form: All x [Ex y F(x,y) <-> Ex z (H(x,z), newp(x,z))], where F and H contain predicates defined in P and newp is a predicate symbol not occurring in P. We want to synthesize a set of clauses, say Eureka, such that the above equivalence formula is true in the least Herbrand model of (P + Eureka).

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

Gianfranco Mascari

Semantica della Riduzione

Abstract
Ad un calcolo logico si associano tre semantiche: la semantica delle formule, la semantica delle dimostrazioni, la semantica della riduzione delle trasformazioni (cut elimination).
Le strutture matematiche corrispondenti sono: strutture algebriche ordinate (operazioni = connettivi), categorie (funtori = connettivi), categorie arricchite.
Una nuova semantica della riduzione verrà definita su categorie parzialmente additive, monoidali e omologiche. Questa semantica presenta relazioni con la Semantica dei Processi, la "Geometry of Interaction" e la Semantica della Iterazione.

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

Paolo Lipparini

Problemi matematici risolti con metodi logici

Abstract
Si presenta un elenco di problemi di matematica che sono stati risolti (o dichiarati irrisolvibili, in vari sensi) mediante l’uso di metodi di logica matematica.
Si abbozza un’analisi dell’impatto (spesso problematico) che questi risultati hanno avuto sulla pratica matematica.
Ci si chiede non tanto se l’attività di divulgazione della logica fra i matematici venga svolta in maniera sufficientemente ampia, completa, precisa, quanto piuttosto se viene svolta in maniera sufficientemente energica.

giovedì 9/12/1993, ore 17, aula E

Ugo de' Liguoro

Un lambda-calcolo non deterministico e parallelo

Abstract
I concetti operazionali di non determinismo e parallelismo sono rappresentati attraverso estensioni del lambda-calcolo puro ed interpretati come operatori di sup ed inf in un reticolo continuo distributivo i cui elementi finiti sono numerabili. Tale struttura viene descritta con strumenti finitari, ovvero attraverso tipi con operatori ad arità finita.
La mappa di interpretazione dai termini agli elementi del reticolo è definita attraverso un sistema di assegnamento di tipo, il quale risulta corretto, completo, ed inducente una semantica pienamente astratta rispetto al preordine operazionale definito sui termini.

giovedì 13/1/1994, ore 17, aula E

Anna Labella
(in collaborazione con R. De Nicola)

Alberi e linguaggi

Abstract
La considerazione di agenti di calcolo non deterministici porta naturalmente a considerare strutture arboree etichettate.
Si può provare che alberi definiti come categorie arricchite sul semireticolo delle loro etichette costituiscono il modello libero per un linguaggio assiomatizzato alla maniera di Salomaa, purchè si lasci cadere la condizione di distributività tra le operazioni.
Si definirà la semantica operazionale corrispondente e si faranno vedere alcune semplici applicazioni di questo risultato e se ne vedrà l’estensione alla categoria di tali alberi.

giovedì 27/1/1994, ore 17, aula E

Piero Pagliani

La teoria logico-algebrica dei Rough Sets

Abstract
La "formazione di concetti" in presenza di informazioni incomplete, e quindi di incertezza e imprecisione, è una attività di primaria importanza in Intelligenza Artificiale.
Seguendo sostanzialmente una definizione classica, per conoscenza possiamo intendere l’abilità di classificare oggetti (stati, eventi, elaborazioni). Gli oggetti che sono nella stessa classe sono indiscernibili per mezzo della conoscenza posseduta e formano blocchi elementari (grani, atomi) per costruzioni più complesse. In particolare la granularità della conoscenza fa sì che alcune nozioni non possano essere espresse precisamente nell’ambito della conoscenza disponibile e possano essere definite solo in modo vago.
Nella Teoria dei Rough Sets, introdotta dal Politecnico di Varsavia al principio degli anni ‘80, ogni concetto impreciso è rimpiazzato da una coppia di concetti precisi, detti approssimazione inferiore e approssimazione superiore, basati sulla interpretazione dello spazio dei dati come spazio modale S5. Questa interpretazione induce la nozione di rough set, classe di equivalenza di concetti modulo l’uguaglianza delle due approssimazioni.
Il seminario presenterà gli aspetti logico-algebrici legati a questa teoria: i sistemi di rough sets verranno interpretati come Algebre di Nelson semi-semplici, come Algebre a 3 valori di Lukasiewicz e infine come generalizzazioni delle Algebre di Post e spazi di funzioni valutate su ideali. Si cercherà di mettere in luce come le varie interpretazioni siano legate ai diversi aspetti intuitivi dei rough sets .

giovedì 10/2/1994, ore 17, aula E

Maurizio Proietti
(in collaborazione con A.Pettorossi, Università di Roma “Tor Vergata”)

Trasformazione di programmi logici: regole e strategie

Abstract
Si presenterà una panoramica di alcune tecniche che sono state proposte in letteratura per la trasformazione dei programmi logici. Sarà dato particolare rilievo all’approccio basato su regole e strategie, e si affronteranno le seguenti due tematiche:
1) correttezza di alcune regole elementari rispetto a varie semantiche che sono state definite per i programmi logici, e
2) uso di strategie che guidino l’applicazione delle regole in modo da migliorare l’efficienza dei programmi.

giovedì 24/2/1994, ore 17, aula E

V. Michele Abrusci

Reti dimostrative non commutative

Abstract
Viene individuata una proprietà geometrica di grafi, che caratterizza tutti e soli i grafi che provengono da dimostrazioni nel frammento (times-par) del calcolo dei sequenti per la logica lineare classica non commutativa.
I grafi che soddisfano tale proprietà sono detti "reti dimostrative non commutative" (non commutative proof nets).

giovedì 10/3/1994, ore 17, aula E

Giuseppe Scollo

Interpolation in categories of pre-institutions

Abstract
Pre-institutions are a weakening of institutions in the sense of Goguen and Burstall, introducing an abstract notion of logical system. When equipped with suitable morphisms, known as pre-institution transformations, they give rise to a hierarchy of categories. Pre-institution transformations preserve satisfaction (in both directions). Pre-institution categories give rise to a "soft" model-theoretic framework for the lifting of classical properties, such as compactness, from abstract logics in the sense of abstract model theory, to a model-independent notion of logical system. Downward reduction of model-theoretic properties along suitable transformations is a frequent phenomenon.
Subject of this talk is an analysis of Craig-style interpolation properties in categories of pre-institutions. While the equivalence between sentence interpolation and Robinson property under compactness and Boolean closure is well-known, a similar result under different assumptions (not involving compactness) is newly established for presentation interpolation. Distinct reduction theorems for interpolation and Robinson properties are presented as well.

giovedì 24/3/1994, ore 17, aula E

Maurizio Castellan
(in collaborazione con Mario Piazza)

La semantica dei quantali all'opera

Abstract
Nel calcolo dei sequenti per il frammento moltiplicativo della logica lineare, le regole strutturali di contrazione e di indebolimento continuano a valere per le formule equivalenti alle costanti logiche 1 e falso. Mediante l'introduzione di opportuni quantali di Girard concreti si prova che esse sono le uniche formule con la suddetta proprietà.
Il risultato getta luce sul potere espressivo del calcolo logico in questione.

giovedì 7/4/1994, ore 17, aula E

Adolfo Piperno
(lavoro in collaborazione con Simona Ronchi della Rocca)

Inferenza di tipi ed estensionalità

Abstract
Il sistema F2 di assegnazione di tipi polimorfi a termini del lambda-calcolo è la controparte alla Curry del sistema F di Girard e Reynolds. Pur se introdotto nei primi anni '70 il problema della decidibilità di tale sistema è rimasto aperto per lungo tempo. Solo nel 1993 è stato annunciato un risultato di indecidibilità. Lo studio delle relazioni fra tipi ed estensionalità, vale a dire fra tipaggi di un termine e tipaggi di termini ad esso estensionalmente equivalenti (e quindi computazionalmente equivalenti), fornisce una stratificazione decidibile di F2.

giovedì 21/4/1994, ore 17, aula E

Giambattista Amati
(in collaborazione con L.Carlucci Aiello, D.M.Gabbay, F.Pirri)

Tableaux, punti fissi e ragionamento non monotono

Abstract
Esiste una corrispondenza ben precisa tra una logica L e il suo sistema di tableaux. Un sistema di tableaux permette di scoprire, a partire da una teoria consistente T, la classe dei suoi modelli M. Tale costruzione è precisata da sequenze di “mosse algoritmiche”. Se si impongono delle restrizioni sul modo di applicare tali sequenze si restringe il numero dei modelli di T e quindi viene determinata una sottoclasse di modelli M_D contenuta in M. Ciò dà origine ad una nuova nozione di conseguenza logica: A ha come conseguenza B sse, per ogni modello m di M_D, m soddisfa A implica che m soddisfa B. In logica dei defaults, ad esempio, M_D è l’insieme delle possibili estensioni o punti fissi per una teoria dei defaults T.
Considereremo una particolare caratterizzazione dei modelli M_D. T e le restrizioni imposte sulla costruzione dei tableaux vengono tradotte in una formula Y(p), essendo p una variabile proposizionale, di una particolare logica modale: i punti fissi per p in tale logica corrispondono, ad esempio, alle estensioni M_D in logica dei defaults. Tale logica modale differisce dal sistema modale G perché può ammettere nessuna o più soluzioni di punto fisso: ciò è infatti quello che normalmente avviene in ragionamento non monotono quando, in presenza di conoscenza incompleta, le possibili estensioni sono necessariamente multiple.

giovedì 5/5/1994, ore 17, aula E

Alden Pixley

Boolean Universal Algebra

Abstract
An algebra is affine complete if each function compatible with all of the congruence relations on A is a polynomial.
A variety of algebras is affine complete if each algebra of the variety is affine complete; the variety of Boolean algebras is affine complete.
We discuss some of the properties affine complete varieties share with the variety of Boolean algebras and how other properties are natural extensions of Boolean properties.

giovedì 12/5/1994, ore 17, aula E

William Lawvere

Objective number theory

Abstract
Two recent results concerning the solution of algebraic equations in the Burnside rig of a distributive category are discussed. Although Lawvere (1990) showed that 7-tuples of trees can be encoded as single trees, suggesting that complex numbers can arise as Euler characteristics, it was Blass who recently showed that (e.g.) 5-tuples cannot be, thus verifying the conjecture and possibly opening the way for a more realistic notion of “computability”. Concerning distributive categories (such as that of finite graphs) having finite hom-sets, Shanuel has shown that solutions of algebraic equations are exactly the objects satisfying the separable/unramified/decidable property, and that moreover the equation satisfied can always be chosen to be “falling-power-nilpotence”.

giovedì 19/5/1994, ore 17, aula E

Fabio Bellissima

Consequentia Mirabilis : vicende di una regola logica

Abstract
Consequentia Mirabilis. è il nome attribuito alla regola logica che corrisponde alla seguente tautologia: ((¬A) -> A) -> A. In altri termini la regola asserisce che, data una proposizione A, se dalla negazione di A si deduce A stessa, allora A è vera.
Il fatto di ottenere la verità di A dalla sua negazione ha, nel corso dei secoli, alimentato fantasie e acceso entusiasmi, ma anche causato il sorgere di perplessità circa la correttezza dell’inferenza e l’effettivo intervento dell’ipotesi ¬A nella dimostrazione di A. Intorno a questi due problemi (ed in particolare al secondo) si è sviluppato un dibattito teorico che trascende la specifica regola e coinvolge il concetto stesso di dimostrazione logica. Le posizioni assunte sono state spesso estreme ed inconciliabili: la Consequentia Mirabilis, ad esempio, è bella ma inutile secondo Wolff, Lambert e Bolzano, mentre è il metodo dimostrativo dei momenti cruciali secondo Saccheri, che a conclusione dell’ Euclides ab omni naevo vindicatus afferma: "Questa sembra essere la caratteristica primaria di ogni verità fondamentale, che partendo dalla sua negazione assunta come vera, mediante una forma di mirabile riaffermazione possa alla fine essere ricondotta a se stessa." Quasi a confermare questa fede, due secoli dopo Cantor userà la Consequentia Mirabilis per dimostrare l’infinità dei numeri transfiniti.