Testo italiano

Ragionamento su aggregati e numeri a supporto della programmazione e relative verifiche: dagli algoritmi di decisione alla programmazione con vincoli con multi-insiemi, insiemi e mappe

Testo inglese

Aggregate- and number-reasoning for computing: from decision algorithms to constraint programming with multisets, sets, and maps

Testo italiano

Il progetto verte sull'automazione del ragionamento su aggregati con applicazioni alla verifica e alla programmazione dichiarativa con vincoli insiemistici.
Esso si articolerà principalmente nelle seguenti tematiche strettamente correlate.

1. Teoria computabile degli insiemi e decidibilità in sistemi formali
Si applicherà un approccio unificante al problema della decisione in teoria degli insiemi a diversi casi di studio.
Si studieranno inoltre alcuni problemi di decisione relativi a teorie specializzate quali la teoria dei grafi, la teoria delle liste, l'analisi reale elementare.
Da un punto di vista più pragmatico, si approfondiranno alcune tecniche efficienti basate sui tableaux analitici per la decisione di vari frammenti della teoria degli insiemi e si cercherà di implementare le procedure di decisione più efficienti all'interno di un verificatore all-purpose.
L'integrazione in sistemi automatici di dimostrazione di decisori per frammenti di teorie matematiche dovrebbe risultare superiore a metodi generali come il principio di risoluzione. Ciò richiederà l'approfondimento di metodi ibridi di prova come la T-risoluzione.
Sarà inoltre approfondito lo studio di sistemi per il supporto visuale interattivo al ragionamento automatico.

2. Calcolo mappale di Tarski-Givant.
Si impiegherà questo formalismo logico-algebrico per la specifica di tipi astratti di dato e per assiomatizzazioni finite di teorie con schemi di induzione, separazione, rimpiazzamento ecc.
L'integrazione di decisori con la T-risoluzione sarà applicata a teorie degli insiemi e di algebre di relazione.
I metodi di dimostrazione automatica studiati all'interno di questa e di altre tematiche saranno applicati al ragionamento sulle gerarchie di ereditarietà fra classi (in specie algebriche).
Sia per il calcolo mappale che per la T-risoluzione, la sperimentazione con gli approcci proposti presuppone lo sviluppo di tecniche di traduzione tra formalismi.

3. Programmazione dichiarativa con vincoli su aggregati.
Si approfondiranno le ricerche inerenti la definizione, uso e realizzazione di linguaggi di programmazione che incorporano la nozione di insieme e le relative operazioni insiemistiche di base. In particolare, si intende:
- estendere lo studio ad altre forme di aggregati, in particolare a multi-insiemi e liste;
- migliorare ed ampliare l'interprete del linguaggio logico a vincoli finora sviluppato, anche con l'utilizzo di strumenti di analisi statica dei programmi e predisponendo meccanismi e costrutti per la programmazione metalogica;
- estendere lo studio relativo all'inserimento di vincoli insiemistici, dal contesto dei linguaggi logici a vincoli (CLP) a quello più ampio dei linguaggi dichiarativi;
- approfondire lo studio dei problemi connessi con la definizione e l'uso di insiemi intensionali;
- valutare l'uso dei linguaggi con insiemi e multi-insiemi in diverse applicazioni, in particolare in quelle basate su tecniche di "multiset rewriting";
- progettare e sviluppare un prototipo del nucleo di un linguaggio visuale che offra strumenti visuali di base per la definizione e manipolazione di oggetti insiemistici.

Inoltre, utilizzando i formalismi e gli strumenti sviluppati nel presente progetto, si svilupperà uno scenario di dimostrazione dei passaggi salienti del Teorema dei Quattro Colori come caso emblematico di sperimentazione e di valutazione di proposte e risultati che matureranno nel progetto stesso. In particolare, si punterà a stimare l'adeguatezza di proposte di costrutti di programmazione dichiarativa con vincoli, e con varie forme di aggregati finiti e di operazioni su di essi, alla formulazione di algoritmi per la ricerca di soluzioni ad istanze del problema.

Testo inglese

The project is about the automation of reasoning over aggregates with applications to the verification and to declarative programming with set constraints.
The project will mainly consist of the following three closely related research subjects.

1. Computable set theory and decidability in formal systems
We will apply a unifying approach to the decision problem in set theory and we will apply it to several case studies.
In addition, we will study the decision problem for some specialized theories such as graph theory, list theory, and elementary real analysis.
From a more pragmatic point of view, we will deepen some efficient techniques based on analytic tableaux to decide fragments of set theory and we will implement the most efficient decision procedures within an all-purpose verifier.
The integration of provers for fragments of mathematical theories within automated deduction systems should prove superior to such fully unspecialized methods as the resolution principle. This requires the deepening of hybrid proof methods such as T-resolution.
We will also deepen the study of systems for the interactive visual support to automated reasoning.

2. Tarski-Givant map calculus
This logical-algebraic formalism will be applied to abstract data type specification and to finite axiomatizations of theories featuring schemes of induction, separation, replacement, etc.
The integration of provers with T-resolution will be applied to theories of sets and of relation algebras.
The automated deduction methods studied within the other topics will be applied to reasoning about inheritance hierarchies of (especially, algebraic) classes.
Both for the map calculus and for T-resolution, the proposed approaches will be experimented by developing translation techniques between the two formalisms.

3. Declarative programming with aggregate constraints
We will deepen the research concerning the definition, application, and implementation of programming languages that embed the notion of set and the relevant basic set-theoretical operations. In particular, the following topics will be addressed:
- enlarging our framework to different forms of data aggregates, in particular, multisets and lists;
- enhancing and optimizing the interpreter of the constraint logic programming developed so far, in particular by using static program analysis tools and by providing metalogic programming features (mechanisms and constructs);
- widening the analysis on set constraint embedding, from the context of constraint logic programming (CLP) languages to the wider context of declarative languages;
- studying problems connected with the definition and use of intensional sets;
- evaluating the use of our programming languages with sets and multisets in various applications, in particular those based on multiset rewriting techniques;
- designing and implementing the core part of a visual language that provides basic visual facilities to define and manipulate set (and multiset) objects.

In addition, by using the formalisms and instruments developed within the present project, we will develop a proof scenario of the salient steps of the Four-Color Theorem as a representative example of experimentation and evaluation of the proposals and results relative to the project itself. In particular, we will estimate the adequacy of the proposed declarative programming constructs, together with various types of finite aggregates and operations on them, relative to the formulation of algorithms for searching solutions to different instances of the problem.

INF/01 - INFORMATICA

Testo italiano
TEORIA COMPUTABILE DEGLI INSIEMI ; PROGRAMMAZIONE DICHIARATIVA ; VINCOLI INSIEMISTICI ; CALCOLO MAPPALE DI TARSKI-GIVANT ; LOGICA ALGEBRICA ; DECIDIBILITA` IN SISTEMI FORMALI ; AUTOMAZIONE DEL RAGIONAMENTO DEDUTTIVO ; RISCRITTURA DI MULTI-INSIEMI ; SISTEMI A TABLEAUX

Testo inglese
COMPUTABLE SET THEORY ; DECLARATIVE PROGRAMMING ; SET CONSTRAINTS ; TARSKI-GIVANT MAP CALCULUS ; ALGEBRAIC LOGIC ; DECIDABILITY IN FORMAL SYSTEMS ; AUTOMATION OF DEDUCTIVE REASONING ; MULTISET REWRITING ; TABLEAU SYSTEMS

CANTONE	DOMENICO
(cognome)	(nome)

Professore ordinario	10/01/1959	CNTDNC59A10C351S
(qualifica)	(data di nascita)	(codice di identificazione personale)

Università degli Studi di CATANIA	Facoltà di SCIENZE MATEMATICHE FISICHE e NATURALI
(università)	(facoltà)
K05B	Dipartimento di MATEMATICA E INFORMATICA
(settore scient.discipl.)	(Dipartimento/Istituto)

095/7383052	095/7337036	cantone@dmi.unict.it
(prefisso e telefono)	(numero fax)	(E-mail)

Testo italiano

Domenico Cantone si è laureato in Matematica presso l'Università di Catania nel 1982.
Nel 1985 e 1987 ha conseguito presso la New York University i titoli di M.S. e Ph.D. in Computer Science.
Dal 1987 al 1989 è stato Visiting Professor presso la New York University.
Nel 1990 è stato responsabile per lo sviluppo del database del sistema orientato agli insiemi Cantor, in qualità di Consultant Engineer.
Nel 1990 ha preso servizio presso l'Università di L'Aquila in qualità di professore ordinario e dal 1991 è professore ordinario di informatica presso l'Università di Catania.
Dal 1994 è presidente del C.C.d.L. in Informatica di Catania.
Fa parte del Consiglio Direttivo della rivista Le Matematiche.
È membro dell'A.C.M. (Association for Computing Machinery).
È stato più volte Visiting Scholar presso la New York University, la Stanford University, l'I.C.S.I. (International Computer Science Institute, Berkeley), le università di Freiburg e di Karlsruhe.
I suoi interessi scientifici includono: teoria computabile degli insiemi, deduzione automatica in varie teorie matematiche, verifica di correttezza di programmi, ingegneria degli algoritmi.
È co-autore di due monografie su Computable Set Theory.
Dal 1992 è stato responsabile scientifico locale di svariati contributi di ricerca del C.N.R., di progetti MURST ex 40% e di un progetto cofinanziato dal MURST (1998-1999), nonché, nel biennio 1998-1999, di un progetto bilaterale con l'università di Karlsruhe nell'ambito del programma Vigoni. Le tematiche interessate sono state: calcolo simbolico, deduzione automatica, decidibilità in teoria degli insiemi.
Dal 1995 al 1997 ha coordinato il progetto nazionale CNR denominato SETA su tematiche di computazione con insiemi.
Attualmente coordina un progetto nazionale CNR, log(SETA), su tematiche di computazione con insiemi.

Testo inglese

Domenico Cantone received his bachelor degree in Mathematics from the University of Catania in 1982.
In 1985 and 1987 he received the degrees of M.S. and Ph.D. in Computer Science from New York University.
From 1987 to 1989 he has been a Visiting Professor at New York University.
In 1990 he has been responsible for the development of the database for the set oriented system Cantor, as Consultant Engineering.
In 1990 he became professor at the University of L'Aquila and from 1991 he has been professor in Computer Science at the University of Catania.
From 1994 he is the Director of the undergraduate studies in computer science at the University of Catania.
He is member of the Board or Directors of the journal Le Matematiche.
He is member of A.C.M. (Association for Computing Machinery).
He has been several times Visiting Scholar at New York University, Stanford University, I.C.S.I. (International Computer Science Institute, Berkeley), Freiburg University and Karlsruhe University.
His main scientific interests include: computable set theory, automated deduction in various mathematical theories, program verification, and algorithmic engineering.
He co-authored two monographs on Computable Set Theory.
From 1992 he has been the local project leader for several C.N.R. research contracts, MURST projects ex 40%, a MURST co-funded project (1998-1999), and for a bilateral project with Karlsruhe University within the Vigoni program. The research subjects have been: symbolic computation, automated deduction, decidability in set theory.
From 1995 to 1997 he has coordinated the national C.N.R. project SETA on set computing.
Currently he coordinates another national C.N.R. project, log(SETA), on set computing.

1. CANTONE D., OMODEO E.G., POLICRITI A. (2001). Set Theory for Computing: From decision procedures to declarative programming with sets. Text and Monographs in Computer Science. In corso di pubblicazione. : Springer-Verlag (UNITED STATES).
2. CANTONE D., FERRO A., OMODEO E. (1989). Computable Set Theory. (vol. Vol. 6, pp. 347). ISBN: 0198538073 International Series of Monographs on Computer Science International Series of Monographs on Computer Science. OXFORD: Clarendon Press (UNITED KINGDOM).
3. CANTONE D., OMODEO E.G., URSINO P. (2001). Formative processes with applications to the decision problem in set theory. INFORMATION AND COMPUTATION. In corso di pubblicazione.
4. CANTONE D., FORMISANO A., OMODEO E.G., ZARBA C. (2001). Compiling dyadic first-order specifications into map algebra. THEORETICAL COMPUTER SCIENCE. In corso di pubblicazione.
5. CANTONE D., FERRO A. (1995). Techniques of computable set theory with applications to proof verification. COMM. PURE APPL. MATH. vol. XLVIII, pp. 1--45 ISSN: 0010-3640 .

Nº	Responsabile scientifico	Qualifica	Settore disc.	Università	Dipart./Istituto	Mesi uomo

Testo italiano

Il progetto è articolato nelle tre seguenti tematiche principali:

1. Teoria computabile degli insiemi e decidibilità in sistemi formali (Coordina: Catania; Concorre: L'Aquila; Collaborazioni esterne: New York University, Stanford University).
Nell'ambito della presente tematica di ricerca, si perseguiranno obiettivi sia teorici che pratici. Sul piano teorico, la ricerca in teoria computabile degli insiemi si concentrerà sul problema di unificare in un'unica teoria decidibile vari frammenti la cui decidibilità è già nota. In tale contesto si intendono studiare estensioni della teoria ground di base MLS con gli operatori insieme-potenza e singoletto, con il predicato di finitezza e con gli operatori di insieme-potenza, unione unaria e singoletto. Infine, si attaccherà il problema della decisione per frammenti insiemistici in presenza del prodotto cartesiano.
Su un piano più pragmatico, ci occuperemo di estendere le recenti tecniche di decisione basate su tableaux analitici a frammenti più espressivi. Si investigheranno euristiche che possano ottimizzare ulteriormente il problema della decisione. Intendiamo, infine, implementare e sperimentare gli algoritmi di decisione più promettenti.
Riguardo alle questioni di decidibilità in altri sistemi formali, si cercheranno procedure di decisione per
- frammenti della teoria dei grafi con costrutti di raggiungibilità e di aciclicità;
- frammenti della teoria delle liste, con le relazioni di inclusione, di prefisso e di suffisso e con una nozione di lunghezza;
- frammenti dell'analisi reale elementare con funzioni continue in cui, oltre a valutazioni puntuali, somme, prodotti, predicati di monotonicit$agrave; e di convessità e additività su funzioni, sono ammessi il predicato di stretta convessità e nozioni legate alle derivate prime e seconde. A tal fine si utilizzeranno tecniche di interpolazione alternative.
Si intende inoltre intraprendere uno studio che porti alla generalizzazione del metodo di Nelson-Oppen al caso della combinazione di procedure di decisione per teorie ground con segnature non disgiunte.
Un ulteriore obiettivo nell'ambito della presente tematica consiste nella stesura di una prima bozza di una monografia sull'applicazione dei principali risultati di decidibilità alla verifica di correttezza di teoremi e di programmi e nella progettazione ed implementazione di un sistema prototipale di verifica in SETL-IDE, un sistema di programmazione orientato agli insiemi in fase di sviluppo presso la New York University.
Linee di ricerca attigue a questa tematica riguardano il principio di risoluzione contestualizzato a teorie del I ordine ed il calcolo mappale:

1') Principio di risoluzione contestualizzata a teorie del I ordine (Coordina: L'Aquila; Concorre: Catania).
In quest'ambito, si intende approfondire lo studio di metodi di dimostrazione che, pur restando fedeli all'idea ispiratrice del principio di risoluzione di Robinson, integrino tale principio con sapere specifico sul dominio. Ciò allo scopo di rimuovere una delle cause principali di inefficienza dei sistemi di dimostrazione automatica. Si intende inoltre raffinare la T-risoluzione di Policriti-Schwartz in metodi di prova "informati". La T-risoluzione verrà messa a confronto con metodi ibridi di dimostrazione quali la theory-resolution di Stickel, e verrà integrata con metodi di decisione per frammenti di vari ambiti matematici, nonché potenziata da raffinamento ed euristiche.
L'integrazione di algoritmi di decisione in un sistema basato sulla T-risoluzione avverrà prioritariamente su casi desunti dalla teoria degli insiemi o dalla teoria delle algebre di relazione (vedi 2.).
2. Calcolo mappale di Tarski-Givant (Coordina: L'Aquila; Concorre: Catania; Collaborazioni esterne: IASI/CNR a Roma, Azione COST 274 (denominata TARSKI) che sta avendo avvio con un finanziamento europeo.).
Il calcolo mappale è un formalismo logico-algebrico che consente assiomatizzazione finite di teorie con schemi di induzione separazione rimpiazzamento e simili. Inoltre ha strumentazione più facile di quella del calcolo predicativo del I ordine.
Sia per il calcolo mappale che per la T-risoluzione (tematica 1'), la dimostrazione di efficacia dell'approccio richiede un esteso piano di sperimentazione per sviluppare tecniche di traduzione che conducano da un formalismo all'altro (ove possibile).
Il calcolo mappale sarà applicato al ragionamento sulle gerarchie di ereditarietà fra classi, in specie classi algebriche, da supportare con metodi di calcolo algebrico-simbolico.
Ci si prefigge inoltre di studiare le principali tecniche di rappresentazione visuale proposte in letteratura, con l'obiettivo immediato di individuare quali caratteristiche peculiari un sistema di rappresentazione e deduzione visuale debba avere. Altro obiettivo consiste nel raffinare e nel portare a completamento un già esistente, seppur parzialmente sviluppato, prototipo per la manipolazione visuale in . Questo prototipo è stato realizzato sfruttando le potenzialità e le funzionalità di un sistema di riscrittura di grafi (AGG) attualmente in sviluppo presso al Technische Univ. di Berlino.

3. Programmazione dichiarativa con vincoli su aggregati (Coordina: Parma; Concorrono: Catania e L'Aquila).
Si approfondiranno le ricerche inerenti la definizione, uso e realizzazione di linguaggi di programmazione che incorporano la nozione di insieme e le relative operazioni insiemistiche di base. In particolare, si intende:
- estendere lo studio ad altre forme di aggregati, in particolare a multi-insiemi e liste, ed integrare tali costrutti nel linguaggio logico con insiemi esistente CLP(SET);
- migliorare ed ampliare l'interprete del linguaggio logico a vincoli finora sviluppato, anche con l'utilizzo di strumenti di analisi statica di programmi;
- estendere lo studio relativo all'inserimento di vincoli insiemistici, dal contesto dei linguaggi logici a vincoli (CLP) a quello più ampio dei linguaggi dichiarativi;
- approfondire lo studio dei problemi connessi con la definizione e l'uso di insiemi intensionali, mediante rielaborazione della nozione di "intensional set constraint";
- valutare l'uso dei linguaggi con insiemi e multi-insiemi in diverse applicazioni, in particolare in quelle basate su tecniche di "multiset rewriting";
- progettare e sviluppare in Java un prototipo del nucleo di un linguaggio visuale che offra strumenti visuali di base per la definizione e manipolazione di oggetti insiemistici in accordo con un paradigma di riscrittura di insiemi/multi-insiemi.

Inoltre, utilizzando i formalismi e gli strumenti sviluppati nel presente progetto, si svilupperà uno scenario di dimostrazione dei passaggi salienti del Teorema dei Quattro Colori come caso emblematico di sperimentazione e di valutazione di proposte e risultati che matureranno nel progetto stesso. In particolare, si punterà a stimare l'adeguatezza di proposte di costrutti di programmazione dichiarativa con vincoli, e con varie forme di aggregati finiti e di operazioni su di essi, alla formulazione di algoritmi per la ricerca di soluzioni ad istanze del problema.


Le diverse tematiche del progetto presentano notevoli sovrapposizioni e interconnessioni, con preziose sinergie e collaborazioni tra le unità del progetto, secondo il seguente grafico:

Testo inglese

The project is structured in the following three main research themes:

1. Computable set theory and decidability in formal systems (Coordinator: Catania; Contributors: L'Aquila; Outer collaboration: New York University).
Within this topic the following research lines, both theoretical and practical, will be developed:
On the theoretical side, research in computable set theory will concentrate on the problem of unifying in a single decidable theory various decidable fragments of set theory. In this context we intend to study the extension of the MLS theory with powerset and singleton operators and with the finiteness predicate, and the extension of MLS with unary union and singleton operators. Finally, we will attack the decision problem for fragments of set theory involving the notion of cartesian product.
From a more pragmatic point of view, in the field of computable set theory we will extend the recent decision techniques based on analytic tableaux to the case of more expressive fragments. Some heuristics will be investigated which can further optimize the decision problem. We intend to implement, and to experiment with, the most promising algorithms.
Concerning the decision problem in other formal systems, we will study the decision problem for the following theory fragments:
- fragments of graph theory with constructs expressing reachability and acyclicity;
- fragments of the theory of lists with inclusion, prefix, and suffix relations of and with a length notion;
- fragments of elementary real analysis with continuous functions, which admit besides the notions of point evaluation, sum, product and monotonic predicates (both strict and non-strict) and of convexity (non-strict), additivity over functions, also the strict convexity-concavity predicate and references to first and second order derivatives. For this purpose alternative interpolation techniques will be considered.
We also intend to study a generalization of the Nelson-Oppen method to the case relative to the combination of decision procedures for ground theories whose signatures are not disjoint.
A further goal of the present research subject is the first draft of a monograph on the applications of the most relevant decidability results to the verification of theorem and program correctness and the design and implementation of a prototype verification system in SETL-IDE, a set-oriented programming environment which is being developed at the New York University.
Lines of research synergic with this topic deal with the contextualization of resolution to first-order theories and with map calculus:

1') Resolution principle contextualized to first-order theories (Coordinator: L'Aquila; Contributors: Catania).
The aim in this topic is to single out proof methods that, keeping faithful to the basic idea of Robinson's resolution, integrate it with domain specific knowledge in order to remove one of the main inefficiency causes of conventional automated proof systems.
We will start from Policriti-Schwartz T-resolution in order to develop "informed" proof methods. T-resolution will be compared with hybrid methods such as Stickel's theory-resolution. It will be further integrated with decision methods for fragments of various mathematical settings, and enhanced with refinements and heuristics. Case studies will be taken from set theories and relational algebra.
The integration of decision algorithms within a T-resolution-based system will be applied to case studies from set theories and map algebra (see 2.).

2) Tarski-Givant map calculus (Coordinator: L'Aquila; Contributors: Catania; Outer collaboration: IASI/CNR (Rome), European COST Action 274 (named TARSKI) which is about being started).
Map calculus is a logic-algebraic formalism that allows for finite axiomatizations of theories with, e.g., induction, separation and replacement schemata. Its framework should, presumably, be lesser than that for standard first order predicate calculus. Both for map calculus and T-resolution (topic 1'), demonstrating the effectiveness of the approaches requires an extended experimentation plan, aimed at developing translation techniques that map, if possible, one into the other.
Map calculus will be applied to reasoning on inheritance hierarchies over classes, especially algebraic classes, supported by symbolic algebraic methods.
We intend also to study the main techniques of visual representation, with the immediate goal of single out the peculiar characteristics which a visual representation and deduction system must have. Another goal consists in refining and completing a partially developed prototype for the visual manipulation . This prototype has been realized by exploiting the potentiality and functionality of a graph rewriting system (AGG), currently under development at the Technische Univ. of Berlin.

3. Declarative programming with aggregate constraints (Coordinator: Parma; Contributors: Catania and L'Aquila).
We will deepen the research concerning the definition, application, and implementation of programming languages that embed the notion of set and the relevant basic set-theoretical operations. In particular, the following topics will be addressed:
- enlarging our framework to different forms of data aggregates, in particular, multisets and lists, and integrate such constructs in the existing logic language CLP(SET);
- enhancing and optimizing the interpreter of the constraint logic programming developed so far, in particular by using static program analysis tools;
- widening the analysis on set constraint embedding, from the context of constraint logic programming (CLP) languages to the wider context of declarative languages;
- studying problems connected with the definition and use of intensional sets, by further elaborating and refining the notion of intensional set constraints;
- evaluating the use of our programming languages with sets and multisets in various applications, in particular those based on multiset rewriting techniques;
- designing and implementing in Java the core part of a visual language that provides basic visual facilities to define and manipulate set (and multiset) objects, according to a set (multiset) rewriting paradigm.

In addition, by using the formalisms and instruments developed within the present project, we will develop a proof scenario of the salient steps of the Four-Color Theorem as a representative example of experimentation and evaluation of the proposals and results relative to the project itself. In particular, we will estimate the adequacy of the proposed declarative programming constructs, together with various types of finite aggregates and operations on them, relative to the formulation of algorithms for searching solutions to different instances of the problem.


The different research subjects of the projects have remarkable overlappings and interconnections. This gives rise to valuable synergies and collaborations among the units of project, according to the following picture:

Testo italiano

La ricerca che punta a migliorare l'utilizzabilità dei sistemi di deduzione automatica e dei linguaggi di programmazione dichiarativa deve affrontare non solo i problemi, perlopiù ben noti ma non per questo di facile soluzione, che riguardano l'efficienza dell'implementazione degli strumenti di supporto a detti sistemi e linguaggi, ma anche quelli, di solito tecnicamente più vaghi, relativi al disegno di nuovi costrutti che facilitino la formulazione di concetti orientati al problema e semplifichino, al limite banalizzino, il ragionamento basato su di essi. Qui si intende questo progresso verso la banalizzazione nel senso proposto da Chaitin quale caratteristica evolutiva della matematica: mentre il primo conseguimento di un risultato difficile richiede sforzi immani, e spesso risulta comprensibile a pochi, l'ulteriore evoluzione del contesto del risultato stesso tende a rivelarne conseguenze non subito percepite e nuove connessioni, che ne promuovono riformulazioni più economiche, in una naturale tendenza a ridurlo a corollario banale di teorie più generali. Una significativa tendenza evolutiva attuale dei paradigmi dichiarativi investiga i modi in cui l'idea di programmare attraverso la formulazione di vincoli possa venir dotata di un buon corredo di costrutti insiemistici, tale appunto da semplificare sia il compito di formalizzare problemi e relativi algoritmi risolutivi, sia quello di sviluppare ragionamenti basati su tali formalizzazioni, con applicazioni alla verifica di correttezza o di altre proprietà di interesse. La meccanizzazione del ragionamento deduttivo su tali basi richiede peraltro investigazioni in un'area autonoma di ricerca, dove alla generalità di meccanismi tradizionali di deduzione automatica, quali il principio di risoluzione, possa accompagnarsi quale valore aggiunto il fatto di lavorare in particolari sottoteorie decidibili della teoria degli insiemi, il che richiede di poter dotare i meccanismi deduttivi di sensibilità parametrica a specifiche teorie. L'integrazione di progressi conseguiti in tali aree è poi da raccordare con quelli in una terza area di ricerca, in certo senso intermedia fra le due, che investiga teorie logico-algebriche e calcoli simbolici ritenuti meglio suscettibili di applicazioni informatiche. La motivazione di partenza di questo progetto risiede nella consapevolezza dell'utilità di coordinare gli sforzi di ricerca nelle tre aree suddette. Per ciascuna di esse, riassumiamo nel seguito la base di partenza delle sue interazioni con le altre nell'ambito di questo progetto. Concludiamo infine con l'argomentazione di un caso di studio che ben esemplifica le opportunità di forte interazione fra le tre aree, e per il quale si intende sviluppare uno scenario di dimostrazione inteso quale banco di collaudo di formalismi e strumenti sviluppati nel presente progetto.

1. Teoria computabile degli insiemi e deduzione automatica

1a. Decidibilità in teoria degli insiemi
La teoria computabile degli insiemi è stata attivamente studiata, e sono state prodotte sia procedure di decisione per frammenti significativi della teoria degli insiemi (si veda [CF95] e le monografie [COP01] e [CFO89]), sia risultati di indecidibilità (si veda [PP88], [CCP89]). Procedure di decisione per frammenti della teoria degli insiemi e algoritmi di unificazione insiemistica sono di basilare importanza per l'implementazione di sistemi di verifica e di linguaggi di programmazione dichiarativi basati sugli insiemi. La ricerca in teoria computabile degli insiemi, si è recentemente focalizzata su problemi di ottimizzazione [Can97] e su un nuovo approccio unificante [COU01]. Per ulteriori dettagli sullo stato dell'arte in proposito si rinvia alla documentazione dell'Unità di Catania.

1b. Decidibilità in teoria dei grafi
Le tecniche sviluppate in teoria computabile degli insiemi sono state adattate per la dimostrazione di risultati di decidibilità in teoria dei grafi. Recentemente, in [CC00] è stata dimostrata la decidibilità di un frammento della teoria dei grafi in cui è possibile esprimere la nozione di raggiungibilità e di aciclicità. Tali procedure di decisione trovano applicazione nella verifica di correttezza di software (es. compilatori).
1c. Decidibilità in altre teorie matematiche: liste, stringhe, analisi reale elementare
Le procedure di decisione in vari campi della matematica consentono di innalzare il livello di dettaglio nella verifica (semi-)automatica di correttezza di sistemi informatici. Ad esempio, liste e stringhe sono comunemente utilizzate come strutture dati di base in molte implementazioni. I risultati di decidibilità in analisi reale elementare trovano applicazione nella verifica di moduli di controllo in sistemi ibridi (si veda [MS98]). In [Biø98] viene descritto un risultato di decidibilità di una teoria di liste con la relazione di inclusione tra liste in assenza di programmazione lineare intera.

Per una maggiore efficacia, risulta importante riuscire a combinare tra loro più procedure di decisione. Recenti lavori in tal senso si notano nell'ambito dell'unificazione [BS96], [Bou93] ed in domini con vincoli, [BS98]. La combinazione di procedure di decisione per teorie aventi in comune simboli funzionali e predicativi oltre all'uguaglianza è più problematica.

2. Teorie logico-algebriche e calcoli simbolici

2a. Deduzione automatica con il calcolo mappale di Tarski-Givant
È concepibile che l'interazione uomo-macchina in un sistema di dimostrazione di teoremi possa essere organizzata mediante un linguaggio della logica del primo ordine che si interfaccia con l'utente ed un formalismo relazionale come quello di Peirce-Schroeder-Tarski [Tar41], [TG87], rivolto alle effettive attività dimostrative. Pertanto sono necessari algoritmi per la traduzione tra i due livelli. La traduzione da un linguaggio tipo (un'opportuna variante del linguaggio predicativo diadico del primo ordine) e uno tipo (un linguaggio equazionale senza variabili individuali) non è sempre possibile. In [CCO97] e [FOT00] è stato presentato un algoritmo che esegue tale traduzione in alcuni casi speciali. Ulteriori applicazioni sono indicate in [AFOT98].

2b. Specifica nel formalismo di Tarski-Givant
Il formalismo di Tarski-Givant è una sorta di linguaggio assembly per la logica equazionale, che si situa ad un livello più basso della logica predicativa del prim'ordine. I suoi costrutti operano su predicati diadici (qui chiamati mappe), proprio come i costrutti dell'algebra relazionale di Codd operano sulle relazioni di un database; in questo formalismo, tuttavia, i predicati possono avere cardinalità infinita, e la complementazione rispetto all'intero dominio del discorso è un'operazione consentita.
Intimamente connesse con questo formalismo, le algebre di relazione hanno subito adattamenti anche in direzione del ragionamento incerto [Due97]. Nel linguaggio di questo formalismo sono stati specificati [AFOT98, FOT00]) importanti tipi astratti di dato quali le liste nidificate e gli insiemi finiti basati su individui; sopra tali tipi è facile specificare ulteriori tipi di dato (ad es., un editor di righe). Anche la traduzione di modelli entità-relazione in specifiche si è rivelata possibile [DO01].
Paradossalmente, il formalismo in questione consente formulazioni semplici dell'intera teoria di Zermelo-Fraenkel [FO00], mentre altri contesti relativamente semplici, quali la teoria dei reticoli, pongono una sfida assai maggiore.

2c. Specifica e deduzione con la T-risoluzione
La T-risoluzione è una regola di inferenza introdotta in [PS95] come generalizzazione della risoluzione standard. Essa rappresenta un tentativo di evitare alcuni degli inconvenienti che conseguono dall'estrema versatilità della risoluzione.
In effetti, la generalità dei dimostratori di teoremi basati sulla risoluzione viene ritenuta in parte responsabile della loro mediocre efficienza nel trattare teoremi anche molto semplici; come rimedio, la natura specifica dei problemi che vengono affrontati dovrebbe entrare esplicitamente in gioco. Con l'approccio della T-risoluzione l'attività di ragionamento si sviluppa su due livelli differenti e disgiunti: 1) un ragionatore `di primo piano', che procede in modo affine alla risoluzione, per poter svolgere il suo passo d'inferenza fondamentale sfrutta 2) un T-decisore che opera `dietro la scena', esperto sulla soggiacente teoria T.
La regola generale di T-risoluzione è stata studiata in profondità: si rinvia alla documentazione dell'Unità dell'Aquila per dettagli sullo stato dell'arte e ulteriori riferimenti. Un'interazione della T-risoluzione con la Programmazione Logica che generalizza l'approccio "con vincoli" (CLP) a quest'ultima, è attualmente oggetto di ricerca [DFP97].

2d. Supporto grafico interattivo al ragionamento automatico
L'algebra delle relazioni binarie si presenta come un ottimo candidato a rivestire il ruolo di "linguaggio macchina" per la logica equazionale. Questa sua caratteristica, come detto, per certi versi favorevole, rende difficoltosa l'interazione tra il sistema e l'utente non familiare con il formalismo algebrico. Per sopperire a questa carenza sono state proposte [CL96,DG00,CFOZ00] varie rappresentazioni visuali basate prevalentemente sulla rappresentazione di espressioni come (multi-)grafi. Le regole di inferenza in vengono conseguentemente rese tramite regole di riscrittura di grafi. Lo stesso processo di traduzione da logica del primo ordine può essere descritto come un processo di riscrittura di grafi [CFOZ00]. Primi passi nella realizzazione di sistemi semi-automatici per il ragionamento visuale sono stati compiuti in [FOS01].

3. Programmazione dichiarativa con vincoli su aggregati
Negli ultimi anni si e' osservato un crescente interesse per l'utilizzo di varie forme di aggregazione dei dati e di costrutti insiemistici all'interno di vari paradigmi di programmazione e di specifica del software. Attualmente esistono vari linguaggi che offrono costrutti insiemistici come entita' di "prima classe", nei paradigmi più diversi (di cui si indicano in parentesi alcuni esempi rappresentativi di quanto appena detto, mentre si rinvia alla documentazione dell'Unità di Parma per i riferimenti bibliografici): imperativi (SETL), funzionali e logici (CLP(SET), CLPS, SETA), ad oggetti (CLAIRE), fino a paradigmi piu' specialistici adottati, ad esempio, nella specifica del software (Z) o in domini applicativi ristretti, come nei modelli di coordinamento (Gamma), nel "non-monotonic reasoning" (Smodels), o nelle applicazioni di database (LDL). Inoltre, molti altri linguaggi di programmazione (ECLiPSe, Oz, Escher) forniscono insiemi ed operazioni su essi nelle loro librerie.
Un utilizzo particolarmente interessante delle astrazioni di tipo insiemistico si ha in combinazione con i linguaggi dichiarativi. Infatti i costrutti insiemistici e le varie operazioni su insiemi sono per loro natura fortemente "dichiarativi", e permettono di descrivere in modo naturale soluzioni astratte a problemi anche complessi. Il fatto che le operazioni su insiemi possano venir trattate come vincoli permette di accrescere ulteriormente la loro "dichiaratività". L'idea alla base di questo stile di programmazione è che definizioni logiche di tipo insiemistico possono essere usate immediatamente come programmi eseguibili, ad es. per la prototipazione rapida del software, in cui normalmente l'efficienza non è di primaria importanza.
Recentemente è stata completata la definizione e realizzazione prototipale di uno di questi linguaggi - denominato CLP(SET) [DPPR00] - un linguaggio logico a vincoli che fornisce varie forme generali e flessibili di costrutti insiemistici con le relative operazioni di base per la loro manipolazione. Il linguaggio CLP(SET) descritto in [DPPR00] rappresenta un'evoluzione del linguaggio logico esteso {log} descritto in [DOPR96]. Ne è stato realizzato un interprete funzionante - implementato in SICStus Prolog. Va notato che parte del lavoro fin qui svolto - specificamente l'individuazione di particolari formule insiemistiche, i "set constraints", di cui si può decidere la soddisfacibilità - è prodotto diretto degli studi sulla teoria computabile degli insiemi. Allo stato attuale, nella letteratura vengono considerati anche altri tipi di aggregati, quali multi-insiemi e liste. Effettivamente, esistono varie interessanti applicazioni per le quali queste diverse forme di aggregato sembrano adattarsi più naturalmente alle caratteristiche del problema considerato. In particolare, i multi-insiemi - aggregati di oggetti in cui sono ammessi elementi ripetuti - vengono utilizzati in vari contesti. Molte recenti proposte, in vari campi anche distanti tra loro, si basano essenzialmente proprio sulla nozione di riscrittura di multi-insiemi, ad es. il "membrane computing" [Pau00], l'analisi di protocolli [CDML00], il modello di oggetti comunicanti [BPM00].
La ricerca sull'utilizzo di altre forme di aggregato deve affrontare innanzitutto il problema di una loro caratterizzazione formale precisa. Mentre si rinvia alla documentazione dell'Unità di Parma per un sommario dello stato dell'arte su questo problema [DPR98, DPR00], va osservato che i risultati teorici ottenuti nel merito, combinati con il fatto che le soluzioni e le tecniche adottate in CLP(SET) sono largamente generali e flessibili, dovrebbero permettere di estendere facilmente CLP(SET) - in cui sono stati considerati finora soltanto insiemi convenzionali - al caso più generale in cui si trattano altre forme di aggregato, in particolare multi-insiemi.

4. Un caso di studio: il Teorema dei Quattro Colori
Il Teorema dei Quattro Colori (T4C) costituisce un caso emblematico di potenziale applicabilità di metodi e risultati di questo progetto. Mentre si rinvia alla documentazione dell'Unità di Catania per brevi cenni sullo stato dell'arte in merito, si espongono qui le ragioni per cui il T4C offre un caso di confluenza delle tre aree di ricerca di questo progetto.
Teoria computabile degli insiemi [CFO89, COP01]: dà fondamenti teorici all'implementazione di linguaggi di programmazione con insiemi. Costituisce dunque un ambiente naturale per algoritmi basati su aggregati finiti, inerenti al T4C.
Programmazione dichiarativa con vincoli e insiemi [DPR00]: è il paradigma per eccellenza in cui formulare algoritmi caratterizzati da massima inerenza al problema, in quanto prospetta ottime opportunità di combinazione di diversi ingredienti atti allo scopo: dichiaratività, aggregati finiti, operazioni insiemistiche, quali non-appartenenza e diseguaglianza, preziose nel T4C.
Logica algebrica e teoria astratta dei modelli: la metamatematica ben si presta alla trasformazione del problema in varie forme. La logica algebrica dà fondamento a traslazioni di tal sorta ed è ricca di risorse promettenti, segnatamente il calcolo mappale [TG87], recentemente dotato di utili meccanismi di traduzione di teorie del primo ordine [CFOZ00]. La teoria astratta dei modelli consente poi di caratterizzare la traducibilità fra ambienti logici solo in termini di proprietà astratte [SS96]. Nel caso emblematico in questione, ci sembra stimolante partire da una formulazione del T4C quale teorema di consistenza di una logica ad hoc per la colorazione dei grafi.

Testo inglese

Research which aims at improving the usability of automated deduction systems and of declarative programming languages has got to cope not only with efficiency problems - which are mostly well-known, yet not so easy to solve - relating to the implementation of support tools for those languages and systems, but also with the somewhat vague problems which relate to the design of new constructs meant to assist one in formulating problem-oriented concepts and to simplify, tendentially to trivialize, the reasoning based upon them. This progress towards trivialization is understood here in the sense proposed by Chaitin, as an evolutionary feature of mathematics. While the first achievement of a difficult result takes immense efforts, and often proves accessible to few experts, the subsequent evolution of the context of that result tends to uncover its not immediately perceived consequences and reveals new connections, which promote its reformulation into more economical terms, within a natural trend towards its reduction to trivial corollary of more general theories. A significant evolutionary trend of current declarative paradigms investigates ways whereby the idea of constraint-oriented programming can be endowed with a rich equipment of set-theoretic constructs, such indeed as to simplify both the task of formalizing problems as well as their solution algorithms and the task of developing reasoning based upon those formalizations, with applications to the verification of correctness and other properties of interest. The mechanization of deductive reasoning on these grounds calls for further inquiry into another area of research on its own, where the generality of traditional mechanisms for automated deduction, such as the resolution principle, could be accompanied with the added value of awareness of working within specific, decidable subtheories of set theory. In order to get that awareness as an effective added value, deductive mechanisms need to be equipped with parametric sensitivity to specific theories. Moreover, joint progress in these areas needs further co-ordination with progress made in a third research area, placed in the middle in some sense, where logico-algebraic theories and symbolic calculi are investigated that seem well-suited to applications in computing. The starting motivation for this project comes from the awareness of the usefulness of co-ordinating research efforts in the three aforementioned research areas. For each of them, we are going to overview the background of its interactions with the other areas in the scope of the present project. We shall close with an outline of arguments for a case study which well exemplifies the opportunities of strong interaction between the three research areas, and for which we intend to develop a proof scenario meant as a testbed for formalisms and tools delivered by this project.

1. Computable set theory and automated deduction

1a. Decidability in set theory
The field of computable set theory has been actively studied, producing decision procedures for many fragments of set theory (cf. [CF95] and the monographs [COP01] and [CFO89]), as well as some undecidability results (cf. [PP88], [CCP89]). Decision procedures for fragments of set theory and set unification algorithms are of basic importance for the implementation of verification systems and declarative programming languages based on sets. Recently, research in computable set theory has focused on optimization issues [Can97] and on a new unifying approach [COU01]. We refer to the documentation of the Catania Unit for further details on the state of the art.

1b. Decidability in graph theory
The techniques developed in computable set theory have been adapted to also prove decidability results in graph theory. Recently, in [CC00] it has been shown the decidability of a fragment of graph theory in which it is possible to express a reachability notion and acyclicity. Such decision procedures have applications in the verification of software (e.g. compilers).
1c. Decidability in list and string theories and in elementary real analysis
Decision procedures in various fields of mathematics allow one to raise the detail levels in the (semi-)automated verification of correctness of information systems. For instance, lists and strings are commonly used as elementary data structures in several implementations. Decidability results in elementary real analysis have important applications in the verification of control modules in hybrid systems (cf. [MS98]). [Biø98] describes a decidability result of a theory over lists with the list inclusion relation, but with no integration of integer linear programming.

It is important to be able to combine together different decision procedures. Recent work in this direction is visible in the fields of unification [BS96], [Bou93], and of constraint domains [BS98]). The combination of decision procedures for non-disjoint theories, namely theories which share functional symbols or predicates besides equality, is more problematic.

2. Logico-algebraic theories and symbolic calculi

2a. Automated deduction with the Tarski-Givant map calculus
It is conceivable that the man-machine interaction in a theorem proving system can be organized with a first-order predicate language at the man interface and with a relational formalism as the Peirce-Schroeder-Tarski's one [Tar41], [TG87], executing the effective proof activities. Algorithms performing effective translations between the two levels are therefore needed. Translating [Image] (a suitable variant of a first-order dyadic predicate language) in [Image] (an equational language without individual variables) is not always possible. In [CCO97] and [FOT00], a thinning algorithm which performs such translation in some special cases has been introduced. Further applications have been reviewed in [AFOT98].

2b. Specification in the Tarski-Givant formalism
The Tarski-Givant formalism offers an assembly language for equational logic of a lower level than first-order logic. Its constructs operate on dyadic predicates (here called maps), very much like the constructs of Codd's relational algebra operate on the relations of a database; in , however, predicates can have an infinite cardinality, and complementation w.r.t. the full domain of discourse is available as an operation. Intimately related with this formalism, relation algebras underwent adaptations even in direction of uncertain reasoning [Due97]. Within the language of this formalism we have specified [AFOT98, FOT00]) important abstract data types such as nested lists and sets ultimately based on individuals, on top of which one can easily define further data types (e.g., an editor). Even the translation of entity-relationship models into such specifications proved possible [DO01]. Paradoxically, one can find simple formulations of full Zermelo-Fraenkel theory [FO00] within the formalism in question, whereas fairly simple frameworks such as lattice theory pose quite a bit of a challenge.

2c. Specification and deduction with T-resolution
T-resolution is an inference rule introduced in [PS95] as a generalization of standard resolution. It represents an attempt to avoid some of the drawbacks ensuing from the extreme versatility of resolution.
As a matter of fact, the generality of resolution-based theorem provers is deemed in part responsible for their low efficiency in dealing even with simple theorems; as a remedy, the specific nature of the problems being tackled should enter explicitly into play.
With the T-resolution approach the reasoning activity develops at two different and disjoint levels: 1) a foreground reasoner, which proceeds in a resolution-like fashion, in order to perform its basic derivation step exploits 2) a background T-decider, `expert' on an underlying theory T. The general T-resolution rule has been studied in depth. We refer to the documentation of the L'Aquila Unit for details about the state of the art and further references. An interaction with Logic Programming which generalizes the "constraints" approach (CLP) is a subject of current research [DFP97].

2d. Interactive graphical support to automated reasoning
The algebra of binary relations appears to be an excellent candidate to play the role of "machine-language" for equational logic. While this feature proves favourable in certain respects as mentioned above, it brings some difficulties into the interaction between the machine and the user who is not familiar with the algebraic formalism. In order to overcome this drawback, several visual representations have been proposed [CL96, DG00, CFOZ00], that are mostly based upon the representation of expressions as (multi-)graphs. Inference rules are consequently rendered by means of graph rewrite rules. The translation process from first-order logic itself may be described as a graph rewriting process [CFOZ00]. First steps towards the implementation of semi-automated systems for visual reasoning are made in [FOS01].

3. Declarative programming with set and multiset constraints
In the last few years we have observed a progressively increasing interest in the use of various forms of aggregations and set-theoretical constructions within programming and specification paradigms. A variety of languages have become available which provide set-theoretical components as first-class data formats, in the most diverse paradigms. Significant witnesses of this statement are mentioned in parentheses, while reference is made to the documentation of the Parma Unit for the bibliographic references: imperative languages (SETL), functional and (constraint) logic programming languages (SuRE, CLP(SET), CLPS, SETA), object-oriented languages (CLAIRE), besides more specialized paradigms adopted for software specification (Z) or for more restricted application domains, such as coordination models (Gamma), non-monotonic reasoning (Smodels), and database applications (LDL). Furthermore, many other programming languages (ECLiPSe, Oz, Escher) provide sets as part of their libraries.
A particularly interesting usage of set-theoretical abstractions is in conjunction with declarative programming languages. Indeed, set constructs and operations are by their own nature highly declarative entities. They provide a natural way to describe abstract solutions to complex problems. Dealing with them as constraints further enhances their declarativeness. The basic idea underlying this programming style is that many set-theoretical logical definitions can be readily used as executable programs, e.g. for rapid software prototyping, where usually efficiency is not a primary concern.
One such language - called CLP(SET) [DPPR00] - which provides one with very flexible and general forms of sets along with basic operations for set manipulation, has been recently defined and implemented. Sets in CLP(SET) are seen as primitive data objects of the language, namely first-order logic terms, whereas all the predefined predicates dealing with sets are viewed as primitive constraints of the language, handled through the use of suitable constraint solving procedures. The language in [DPPR00] represents an evolution of the extended logic programming language {log}, described in [DOPR96]. A CLP(SET) interpreter has been implemented in SICStus Prolog. It is to be noted that part of the work done so far - that is the singling out a special kind of first-order formulae, viz. the set constraints, for which satisfiability is decidable - is an outcome of the work in Computable Set Theory. Other classes of aggregates are also considered by current literature, such as multisets and lists. Indeed, there are several interesting applications for which these different kinds of aggregates seem to fit more naturally the problem requirements than sets. In particular, multisets - i.e., aggregates where elements are allowed to have multiple occurrences - are employed in various contexts. A number of recent proposals are based on some notion of multiset rewriting, ranging from membrane computing [Pau00] to security protocol analysis [CDML2000], and to communicating object models [BPM00].
The research on the use of different forms of aggregates must in the first place counter the problem of their precise formal characterization. While reference is made to the documentation of the Parma Unit for an account of the state of the art on this problem [DPR98, DPR00], it is to be noted that the theoretical results herein attained, along with the fact that the solutions and techniques adopted in CLP(SET) are quite general and flexible, should allow us to easily extend CLP(SET) - which is now limited to `conventional' sets - to the more general case where it is possible to deal with various kinds of aggregates simultaneously, in particular sets and multisets.

4. A case study: the Four-Colour Theorem
The Four-Colour Theorem (4CT) is a paradigmatic case of potential applicability of methods and results coming out of this project. While reference is made to the documentation of the Catania Unit for a brief mention of the relevant state of the art, here is an outline of the reasons why the 4CT offers a case of confluence of the three research areas involved in this project.
Computable set theory [CFO89, CPO01]: it gives theoretical foundations to the implementation of programming languages with sets. It thus forms a natural environment for algorithms based on finite aggregates, inherent to the 4CT.
Declarative programming with constraints and sets [DPR00]: it is the paradigm of choice for the formulation of algorithms which exhibit maximal inherence to the problem, since it promises optimal opportunities for combining diverse ingredients apt to the purpose: declarativeness, finite aggregates, such set operations, as nonmembership and inequality, that prove very useful in the 4CT.
Algebraic logic and abstract model theory: metamathematics is well-suited to transform the problem to various forms. Algebraic logic provides such translations with foundations and is rich of promising resources, viz. map calculus [TG87], recently endowed with useful mechanisms to translate first-order theories [CFOZ00]. Abstract model theory allows one to characterize translatability between logical frameworks in terms of abstract properties only [SS96]. In the paradigmatic case in question, we find it exciting to start from a formulation of the 4CT as the consistency theorem of an ad-hoc logic of graph colouring.

[AFOT98] E. Aureli, A. Formisano, E. Omodeo ad M. Temperini. Map Calculus: Initial application scenarios and experiments based on Otter. Rep. 466, IASI-CNR, 1998.
[Biø98] N.S. Bjørner. Integrating decision procedures for temporal verification. Ph.D. Thesis, Stanford University, 1998.
[Bou93] A. Boudet. Combining unification algorithms. J. of Symbolic Computation, 16(6):597-626, 1993.
[BPM00] J.-P. Bodeveix, C. Percebois, S. Majoul. An Object-Oriented Coordination Model based on MultisetRewriting. In Proc. of Ninth Int'l Conference on Parallel and Distributed Computing Systems.
[BS96] F. Baader and K.U. Shultz. Unification in the union of disjoint equational theories: Combining decision procedures. J. of Symbolic Computation, 21(2):211-243, 1996.
[BS98] F. Baader and K.U. Shultz. Combination of constraint solvers for free and quasi-free structures. Theoretical Computer Science, 192(1):107-161, 1998.
[Can97] D. Cantone. A fast saturation strategy for set-theoretic Tableaux. In Didier Galmiche, editor, Proceedings of the Int'l Conference on Automated Reasoning with Analytic Tableaux and Related Methods, volume 1227 of LNAI, pp. 122-137, Springer-Verlag, 1998.
[CC00] D. Cantone and G. Cincotti. The decision problem in graph theory with reachability related constructs. In P. Baumgartner, H. Zhang (Eds.) Proc. of Third International Workshop on First-Order Theorem Proving (FTP 2000), Technical Report 5/2000, Universität Koblenz-Landau, Institut fu"r Informatik, pp. 68--80, 2000.
[CCO97] D. Cantone, A. Cavarra, and E.G. Omodeo. On existentially quantified conjunctions of atomic formulae of . In Proc. of FTP97 Int. workshop on first order theorem proving, RISC-Linz Report Series No.97-50:45-52,1997.
[CCP89] D. Cantone, V. Cutello, A. Policriti. Set-theoretic reductions of Hilbert's tenth problem. LNCS, Springer-Verlag, Vol. 440, pp. 65-75, 1989.
[CDML00], [CDML2000] I. Cervesato, N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov. Relating Strands and Multiset Rewriting for Security Protocol Analysis. In P. Syverson, ed., 13th IEEE Computer Security Foundations Workshop - CSFW'00, pp. 35-51, 2000.
[CF95] D. Cantone and A. Ferro. Techniques of computable set theory with applications to proof verification. Comm. Pure Appl. Math., XLVIII:1-45, 1995.
[CFO89] D. Cantone, A. Ferro, and E. Omodeo. Computable Set Theory. Vol. no.6 Oxford Science Publications of International Series of Monographs on Computer Science. Clarendon Press, 1989.
[CFOZ00] D. Cantone, A. Formisano, E.G. Omodeo, and C.G. Zarba. Compiling dyadic first-order specifications into map algebra. In D. Heylen, A. Nijholt and G. Scollo (Eds.), Proc. of 16th Twente Workshop on Language Technology joint with 2nd AMAST workshop on Algebraic Methods in Language Processing (AMiLP 2000)}, TWLT 16, University of Twente, pp. 35-54, 2000.
[COP01] D. Cantone, E.G. Omodeo, and A. Policriti. Set Theory for Computing: From decision procedures to declarative programming with sets. Text and Monographs in Computer Science. Springer-Verlag, to appear, 2001.
[COU01] D. Cantone, E.G. Omodeo and P. Ursino. Formative processes with applications to the decision problem in set theory. To appear in Information and Computation, 2001.
[DFP97] A. Dovier, A. Formisano, A. Policriti. On T-Logic Programming. In J. Maluszynski, ed., Proc. of the Int. Logic Programming Symp. 1997. ILPS97. MIT Press.
[DG00] D. Dougherty, C. Gutierrez. Normal Forms and Reduction for Theories of Binary Relations. RTA2000, LNCS 1833, Springer, 2000.
[DO01] E. Doberkat, E. Omodeo. Algebraic semantics of ER models from the standpoint of map calculus. I: static view. RelMiS-ETAPS. W. Kahl ed., 2001.
[DOP99] A. Dovier, E.G. Omodeo, and A. Policriti. Solvable set/hyperset contexts: II. A goal-driven unification algorithm for the blended case. Applicable Algebra in Engineering, Communication and Computing, 9(4):293-332, 1999.
[DOPR96] A. Dovier, E. Omodeo, E. Pontelli, G. Rossi. {log}: A Language for Programming in Logic with Finite Sets. Journal of Logic Programming, Vol.28(1), North Holland, 1996, 1--55.
[DPPR00] A. Dovier, C. Piazza, E. Pontelli, and G. Rossi. Sets and Constraint Logic Programming, To appear in ACM Transaction on Programming Language and Systems.
[DPR98] A. Dovier, A. Policriti, and G. Rossi. A uniform axiomatic view of lists, multisets, and sets, and the relevant unification algorithms. Fundamenta Informaticae, 36(2/3):201-234, 1998.
[DPR00] A. Dovier, C. Piazza, and G. Rossi. A uniform approach to constraint-solving for lists, multisets, compact lists, and sets. Technical Report, Dipartimento di Matematica, Università di Parma, no. 235, July 2000.
[Due97] I. Duentsch. A logic for rough sets. TCS, 179(1-2), 1997.
[FO00] A. Formisano, E. Omodeo. An equational re-engineering of set theories. In G. Salzer and R. Caferra, eds., Automated Deduction in Classical and Non-Classical Logics, pp.176-191, Springer, LNCS 1761.
[FOS01] A. Formisano, E. Omodeo, M. Simeoni. A graphical approach to map reasoning. RelMiS-ETAPS. W.Kahl ed., 2001.
[FOT00] A. Formisano, E. Omodeo, M. Temperini. Goals and benchmarks for automated map reasoning. Journal of Symbolic Computation, 29(2):259-297, 2000.
[MS98] Z. Manna, H.B. Sipma. Deductive verification of hybrid systems using STeP. Int. Workshop on Hybrid Systems: Computation and Control, LNCS 1386, 1998.
[Pau00] G. Paun. Computing with Membranes. Journal of Computer and System Science, 61, 2000.
[PP88] F. Parlamento, A. Policriti. Decision procedures for elementary sublanguages of set theory. IX. Unsolvability of the decision problem for a restricted subclass of the -formulas in set theory. Comm. Pure Appl. Math., XLI:221-251, 1988.
[PS95] A. Policriti, J. Schwartz. T-Theorem Proving I. J. Symb. Comp., 20, 1995.
[SDDS86] J. Schwartz, R. Dewar, E. Dubinsky, E. Schonberg. Programming with Sets: An introduction to SETL. Texts and Monographs in Computer Science. Springer, 1986.
[SS96] A. Salibra and G. Scollo, Interpolation and compactness in categories of pre-institutions, MSCS 6 (1996) 261-286.
[Tar41] A. Tarski. On the calculus of relations. J. of Symbolic Logic, 6(3):73-89, 1941.
[TG87] A. Tarski and S. Givant. A formalization of Set Theory without variables. Vol. 41 of Colloquium Publications. AMS, 1987.

Fase 1

Durata:	12 mesi		Costo previsto:	0 M£		0 Euro

Descrizione:

Testo italiano

Durante la prima fase del progetto, la ricerca si articolerà nelle seguenti tematiche:

1. Teoria computabile degli insiemi e decidibilità in sistemi formali

1.1. Teoria computabile degli insiemi
1.1.1. Da un punto di vista pi˜ teorico, la ricerca in teoria computabile degli insiemi nel corso della prima fase si concentrerà sull'applicazione della metodologia dei processi formativi all'estensione della teoria ground di base MLS con gli operatori insieme-potenza e singoletto e con il predicato di finitezza.
1.1.2. Da un punto di vista pi˜ pragmatico, si cercherà di estendere le recenti tecniche di decisione basate su tableaux analitici al caso di frammenti pi˜ espressivi. In particolare, verrà considerato il problema della decisione in presenza di funzioni e predicati di monotonicità. Verranno anche investigate alcune euristiche per ottimizzare ulteriormente il problema della decisione in alcuni casi.
1.1.3. Si cercherà di esprimere mediante un calcolo per tableau l'algoritmo di unificazione (iper-)insiemistica sviluppato in [DOP99].
1.1.4. Infine, si cercherà di generalizzare al caso iper-insiemistico il calcolo decidibile per tableau per il frammento MLSS.

1.2. Decidibilità in teoria dei grafi
Si approfondirà lo studio del linguaggio presentato in [CC00] per esprimere alcuni costrutti di base della teoria dei grafi con nozioni di raggiungibilità e aciclicità.

1.3. Decidibilità in altri sistemi formali
1.3.1. Si utilizzerà il metodo di Nelson-Oppen per la combinazione di procedure di decisione, per studiare un linguaggio su liste in grado di esprimere oltre ad eventuali vincoli al primo ordine tra gli individui di un certo dominio, anche i seguenti vincoli su liste:
- lista vuota
- lista singoletta
- concatenazione di liste
- lunghezza di una lista
- appartenenza di un individuo ad una lista
- relazioni di prefisso, suffisso e inclusione tra liste
1.3.2. Si intende inoltre affrontare lo studio di problemi di decisione correlati al concetto di ricoprimento di stringhe.
1.3.3. Riguardo al problema della decisione in analisi reale elementare, si cercherà di estendere i risultati esistenti, riguardanti una teoria con funzioni continue, valutazione puntuale, somma, prodotto e predicati di monotonicità (stretta e non) e di convessità (non stretta), additività su funzioni mediante il predicato di stretta convessità-concavità, introducendo anche la possibilità di riferire i vari predicati a intervalli infiniti.
1.3.4. Si intende inoltre intraprendere uno studio che porti alla generalizzazione del metodo di Nelson-Oppen al caso della combinazione di procedure di decisione per teorie ground con segnature non disgiunte.

1.4. T-Risoluzione
Per quanto riguarda la T-risoluzione, s'intende approfondire un confronto con altri metodi "ibridi" di dimostrazione (quali la theory-resolution), generalizzare ed ottimizzare i risultati di completezza relativi a raffinamenti del metodo di base; verranno inoltre selezionati frammenti decidibili della teoria degli insiemi che possano essere integrati nella T-risoluzione; si cercherà, infine, di individuare frammenti della teoria delle algebre di relazioni che siano parimente decidibili e incorporabili nella T-risoluzione, e quest'ultimo discorso verrà allargato alle algebre di relazione "rough".

2. Calcolo mappale di Tarski-Givant
2.1. Per quanto riguarda il calcolo mappale, andranno approfonditi metodi di ragionamento mappale "sicuri" (ossia rivolti al trattamento di relazioni finite), tecniche per tradurre specifiche dichiarative con variabili individuali (in stile Prolog) in specifiche logico-algebriche; metodi di semplificazione di espressioni mappali e di rappresentazione e dimostrazione -anche in forme grafiche e diagrammatiche- di uguaglianze mappali.
2.2. Si cercherà inoltre di estendere il campo di applicabilità dell'algoritmo di Graph Thinning descritto in [CCO97] e [CFOZ00] e di caratterizzare il frammento del linguaggio traducibile in .
2.3 Per quanto riguarda il supporto automatico a ragionamento su gerarchie di classi, lo studio del primo anno consisterà principalmente nell'individuare gerarchie significative e variate (`scenari d'applicazione'), sperimentando con varie forme di specifica, sino a giungere alla formalizzazione (sintattico-semantica) stabile di un linguaggio per la specifica di gerarchie di classi munite di proprietà assiomatiche. Il tipo di ragionamenti su, e di ristrutturazioni di tali gerarchie, e conseguentemente il tipo di supporto automatico da fornire a tali attività, dovranno emergere in parte dallo studio dei detti scenari.
2.4. Relativamente all'approccio visuale al ragionamento in , ci si prefigge come primo compito lo studio e la comparazione delle diverse tecniche di rappresentazione visuale proposte in letteratura, con l'obiettivo immediato di individuare quali caratteristiche peculiari un sistema di rappresentazione e deduzione visuale debba avere. Altro obiettivo consiste nel raffinare e nel portare a completamento un già esistente, seppur parzialmente sviluppato, prototipo per la manipolazione visuale. Questo prototipo Ë stato realizzato sfruttando le potenzialità e le funzionalità di un sistema di riscrittura di grafi (AGG) attualmente in sviluppo presso al Technische Univ. di Berlino.
2.5. Sia per il calcolo mappale che per la T-risoluzione, la dimostrazione di efficacia dell'approccio richiede un esteso piano di sperimentazione; in vista di tale sperimentazione verranno acquisiti strumenti esistenti sul calcolo mappale quali Ralf, Relview e Libra.

3. Programmazione dichiarativa con vincoli su aggregati
3.1. Si completerà lo sviluppo del nuovo linguaggio CLP con insiemi e multi-insiemi ñ qui indicato col nome di {log}+. Inizialmente verrà completata la definizione e realizzazione dei risolutori di vincoli su multi-insiemi e liste; quindi si procederà ad inserirli ed integrarli nel linguaggio logico con insiemi esistente CLP(SET).
3.2. Si analizzerà l'utilizzo del linguaggio {log}+ per lo sviluppo di semplici applicazioni. In particolare prevediamo di confrontare il linguaggio {log}+ con il linguaggio GAMMA, analizzando l'uso del nostro linguaggio per realizzare computazioni basate su "multiset rewriting" quali quelle previste nel cosiddetto "membrane computing".
3.4. Si investigheranno le possibilità di "esportare" le tecniche utilizzate per la gestione di vincoli insiemistici e multi-insiemistici, e pi˜ in generale la nozione di programmazione basata su insiemi, a contesti diversi da quello strettamente CLP, soffermandoci in particolare sul linguaggio dichiarativo ALMA-0, in corso di sviluppo all'Università di Amsterdam.
3.4. Iniziare lo studio ed il progetto della parte centrale di un linguaggio di programmazione visuale, fortemente basato sulla nozione di insieme (e multi-insieme) che fornisca all'utente un insieme di "facilities" visuali per la definizione di oggetti insiemistici (e multi-insiemeistici) e la loro manipolazione in accordo con un paradigma di riscrittura di insiemi/multi-insiemi. Nel progetto di questo linguaggio cercheremo di trarre vantaggio il pi˜ possibile dall'esperienza maturata nello sviluppo dei linguaggi CLP con inseimi e multi-insiemi svolto in precedenza.
3.5. Si analizzerà la definizione e gestione degli insiemi intensionali. Questo richiederà di elaborare ulteriormente e raffinare la nozione di "intensional set constraint". Inoltre si intende sfruttare gli strumenti di analisi statica per eseguire controlli a tempo di compilazione che, da una parte, possano a priori la completezza delle computazioni effettuate e, dall'altra parte, possano aiutare nel selezionare la strategia di implementazione pi˜ adeguata per le operazioni di "set grouping" che possono essere richieste dalla valutazione di un insieme intensionale.
3.6. Si progetterà un nuovo linguaggio dichiarativo con insiemi "Alma-like". Il linguaggio ñ che indichiamo qui con il nome di L0 ñ dovrebbe fornire la maggior parte degli aspetti caratterizzanti di {log}+ (specificatamente, astrazioni di aggregati di dati, quali insiemi e liste, definite sia estensionalmente che intenzionalmente, constraint, computazioni non-deterministiche), ma incorporate in un ambiente pi˜ convenzionale, usando una sintassi e delle convenzioni Pascal-like, come avviene in Alma-0.

4. Caso di studio: il Teorema dei Quattro Colori
Nella prima fase si collocano tre attività: la prima consiste nello studio di letteratura di logica algebrica, al fine di individuare quei concetti e risultati che, a partire dalla formulazione delineata sopra del Teorema dei Quattro Colori quale teorema di consistenza di una logica delle colorazioni di grafi planari, possano dar corpo all'idea di reperirne una dimostrazione per questa via. Le altre due consistono nello studio degli aspetti algoritmici della migliore soluzione al Problema dei Quattro Colori oggi disponibile, e nella sperimentazione della loro formulazione nei costrutti di programmazione studiati in questo progetto.

Testo inglese

During the first phase of the project, the research will concern the following subject areas:

1. Computable set theory and decidability in formal systems

1.1. Computable set theory
1.1.1. From a more theoretical point of view, the main objective of the research in computable set theory will be to apply the methodology of formative processes to the extension of the ground theory MLS with the powerset and singleton operators and the finiteness predicate.
1.1.2. From a more pragmatic point of view, in the field of computable Set Theory we will extend the recent decision techniques based on analytic tableaux to the case of more expressive fragments. Some heuristics will be investigated which can further optimize the decision problem in some cases.
1.1.3. We will try to express by means of a tableau calculus the (hyper-)set unification algorithm developed in [DOP99]./i>
1.1.4. Finally, we will attempt to generalize to the hyperset case the decidable tableau calculus for the fragment MLSS.

1.2. Decidability in graph theory
We will further study the language presented in [CC00] to express some basic constructs of graph theory, including the notions of reachability and acyclicity.

1.3. Decidability in other formal systems
1.3.1 We will use the Nelson-Oppen method for combining decision procedures to study a language on lists which allows to express besides first-order constraints, also the following lists constraints:
- empty list
- singleton list
- list concatenation
- length of list
- membership of an individual to a list
- prefix, suffix, and inclusion relations among lists
1.3.2. We also intend to study various decision problems concerning the concept of string covering.
1.3.3. Concerning the decision problem in elementary real analysis, we will try to extend the results relative to a theory with continuous functions, point evaluation, sum, product and monotonicity predicates (strict and not) and of convexity (not strict), additivity over functions by means a predicate expressing strict convexity-concavity. We also intend to introduce the possibility to refer the various predicates also to infinite intervals.
1.3.4. We intend to study a generalization of the Nelson-Oppen method to the case relative to the combination of decision procedures for ground theories whose signatures are not disjoint.

1.4. T-Resolution
As regards T-resolution, we intend to run a detailed comparison with other "hybrid" proof methods, namely Theory resolution, and to generalize/optimize the completeness results to refinements of the base method. Also, we will select and integrate within T-resolution some decidable fragments of set theory. Finally, we will try to characterize fragments of relational algebra theories that are both decidable and suitable to be embodied into T-resolution, and the latter topic will be broadened so as to take rough algebras too into account.

2. Tarski-Givant map calculus
2.1. Concerning map calculus, the focus will be on "safe" map reasoning methods (meaning, basically, methods based on the implicit assumption that all maps are finite), on techniques for translating Prolog-style declarative specifications with individual variables into logic-algebraic specifications; methods for simplifying map expressions and for proving equalities. We intend to publish these results into an extended research report, from which one or more journal papers will be extracted.
2.2. We intend to extend the applicability of the algorithm described in [CCO97] and to implement it. We will also try to characterize the fragment of the language that can be translated in .
2.3. Concerning automated support for reasoning about hierarchies of classes, in the first year we intend, essentially, to characterize several relevant hierarchies (scenarios for applications) and experiment with different specification styles, so as to reach a satisfactory definition (syntax and semantics) of a language for specifying classes subject to explicit axiomatic properties. The kind of reasoning to be performed on such hierarchies, and the sort of re-structurings to be applied to them, will emerge mainly from the analysis of such scenarios; the analysis of scenarios will also provide a characterization of the automated support that is needed in order to automatize these activities.
2.4. As far as visual reasoning in is concerned, the first task is studying and comparing the variety of proposals for graphic representation that can be found in the literature, with the immediate goal of singling out the peculiar features which are desirable in a system which represents and visualizes deductions. Another goal is to refine and bring to completion a prototype which already exists (but which has been only partly developed) for visual manipulation. This prototype has been realized by exploting potential and funzionalities of a system for graph rewriting (AGG) which currently is under development at the Technische Univ. of Berlin.
2.5. Both for the map calculus and for T-resolution, proving the effectiveness of the approach will require planning and running an extensive testing activity; in view of that, we will acquire tools for map reasoning such as Ralf, Relview and Libra.

3. Declarative programming with aggregate constraints
3.1. We will complet the development of the new CLP language with sets and multisets ñ here named {log}+. First we shall complete the definition and implementation of the constraint solvers for multisets and lists; then we shall proceed to embed them into the existing logic language with sets CLP(SET).
3.2. We will analyze the use of {log}+ to develop simple applications. In particular, we plan to compare the language {log}+ with the language GAMMA, studying the use of our language to describe multiset rewriting based computations, such as those required in "membrane computing".
3.3. We will investigate the possibility to "export" our techniques for set and multiset constraint handling to contexts other than those provided by the usual CLP scheme. In particular we plan to focus our attention on the declarative language Alma-0, recently developed at the University of Amsterdam.
3.4. We will start the study and design of the core part of a visual programming language, strongly based on the notion of set (and multiset), which provides the user with visual facilities for the definition of set (multiset) objects and for their manipulation, according to a set (multiset) rewriting paradigm. In the design of this language we will try to take advantage as much as possible from the experience gained in the development of the former CLP languages with sets and multisets.
3.5. We will investigate the definition and management of intensional sets. This will require to further elaborate and refine the notion of intensional set constraints. Moreover we plan to exploit the static analysis tools to perform compile-time checks which, on the one hand, may ensure "a priori" completeness of the computations carried on, and, on the other hand, may help in automatically selecting the most adequate implementation strategy for the set collection operation possibly required by intensional sets evaluation.
3.6. We will design a new "Alma-like" declarative language embedding sets. The language ñ here named L0 ñ should provide most of the features of {log}+ (namely, data aggregate abstractions, such as sets and lists, both extentionally and intensionally defined, constraints, non-deterministic computations), but embedded in a more conventional framework, using Pascal-like syntax and conventions, like in Alma-0.

4. A case study: the Four-Color Theorem
In this phase the following activities will be carried out: the first one consists in the study of the relevant literature in algebraic logic, in order to single out those concepts and results which are more promising in a possible alternative proof of the Four-Color Theorem as a consistency theorem in a logic of planar graph colorings. The other two activities, consist in the study of the algorithmic aspects of the best solution to the Four-Color Problem available today and in the experimentation of their formulation using the aggregate constructs studied in the present project.

Risultati parziali attesi:

Testo italiano

I risultati parziali attesi alla fine della prima fase sono raggruppati di seguito per tematica.

1. Teoria computabile degli insiemi e decidibilità in sistemi
formali

1.1. Teoria computabile degli insiemi
1.1.1. Procedura di decisione per MLS con gli operatori insieme-potenza e singoletto e con il predicato di finitezza.
1.1.2.1. Sistema a tableaux decidibile per un frammento della teoria degli insiemi in presenza di funzioni e predicati di monotonicità.<\i>
1.1.2.2. Proposta di nuove euristiche per ottimizzare ulteriormente il problema della decisione.
1.1.3. Sistema a tableaux per l'algoritmo di unificazione (iper-)insiemistica sviluppato in [DOP99].
1.1.4. Sistema a tableaux per la versione iperinsiemistica della teoria MLSS.

1.2. Decidibilità in teoria dei grafi
Estensione della procedura di decisione contenuta in [CC00].

1.3. Decidibilità in altri sistemi formali
1.3.1. Procedura di decisione per un linguaggio su liste in grado di esprimere oltre ad eventuali vincoli al primo ordine tra gli individui di un certo dominio, anche svariati vincoli su liste.
1.3.2. Risultati di decidibilità sul ricoprimento di stringhe.
1.3.3. Procedura di decisione per una frammento dell'analisi reale elementare con funzioni continue, valutazione puntuale, somma, prodotto, predicati di monotonicità e di convessità, e additività su funzioni.
1.3.4. Nuovo metodo per la combinazione di procedure di decisione per teorie ground con segnature non disgiunte.

1.4. T-Risoluzione
Generalizzazione/ottimizzazione dei risultati di completezza relativi a raffinamenti del metodo di base; integrazione di frammenti decidibili della teoria degli insiemi nella T-risoluzione; individuazione di frammenti della teoria delle algebre di relazioni che siano parimente decidibili e incorporabili nella T-risoluzione.

2. Calcolo mappale di Tarski-Givant
2.1. Metodi di ragionamento mappale "sicuri" (ossia rivolti al trattamento di relazioni finite); tecniche per tradurre specifiche dichiarative con variabili individuali (in stile Prolog) in specifiche logico-algebriche; metodi di semplificazione di espressioni mappali e di rappresentazione e dimostrazione -anche in forme grafiche e diagrammatiche- di uguaglianze mappali. Il risultato di questa attività sarà un esteso rapporto di ricerca, dal quale verranno estratti uno o piu` articoli da sottomettere a rivista scientifica.
2.2. Estensione dell'algoritmo di Graph Thinning descritto in [CCO97] e [CFOZ00] e caratterizzazione del frammento del linguaggio traducibile in .
2.3 Specifiche di un linguaggio di programmazione object-oriented specificamente rivolto a linguaggi per il calcolo algebrico simbolico; specifiche di gerarchie di classi algebriche in detto linguaggio, con particolare enfasi sulla definizione di proprietà degli oggetti.
2.4. Raffinamento e completamento di un prototipo per la manipolazione visuale.
2.5. Ampia sperimentazione del calcolo mappale e della T-risoluzione con gli strumenti esistenti sul calcolo mappale quali Ralf, Relview e Libra.

3. Programmazione dichiarativa con vincoli su aggregati
3.1. Completamento dello sviluppo del nuovo linguaggio CLP con insiemi e multi-insiemi ñ qui indicato col nome di {log}+.
3.2. Confronto del linguaggio {log}+ il linguaggio GAMMA, analizzando l'uso di {log}+ per realizzare computazioni basate su "multiset rewriting" quali quelle previste nel cosiddetto "membrane computing".
3.4. Esportazione ad ALMA-0 delle tecniche utilizzate per la gestione di vincoli insiemistici e multi-insiemistici, e più in generale la nozione di programmazione basata su insiemi, a contesti diversi da quello strettamente CLP.
3.4. Studio e progetto di un linguaggio di programmazione visuale, fortemente basato sulla nozione di insieme (e multi-insieme) che fornisca all'utente un insieme di "facilities" visuali per la definizione di oggetti insiemistici (e multi-insiemeistici) e la loro manipolazione in accordo con un paradigma di riscrittura di insiemi/multi-insiemi.
3.5. Definizione e gestione degli insiemi intensionali; applicazione degli strumenti di analisi statica per eseguire controlli a tempo di compilazione per selezionare la strategia di implementazione più adeguata per le operazioni di "set grouping" che possono essere richieste dalla valutazione di un insieme intensionale.
3.6. Progettazione di un nuovo linguaggio dichiarativo con insiemi "Alma-like" (L0) che incorpori la maggior parte degli aspetti caratterizzanti di {log}+ in un ambiente Pascal-like.

4. Caso di studio: il Teorema dei Quattro Colori
Individuazione dei concetti di logica algebrica che consentono di formulare il Teorema dei Quattro Colori come teorema di consistenza di una logica delle colorazioni di grafi planari; studio degli aspetti algoritmici legati alla soluzione del Problema dei Quattro Colori oggi disponibile; formulazione di tali algoritmi con i costrutti di programmazione studiati in questo progetto.

Testo inglese

The partial results expected at the end of the first phase are grouped below according to their research subject.

1. Computable set theory and decidability in formal systems

1.1. Computable set theory
1.1.1. Technical report on a decision procedure for MLS with the powerset and singleton operators and the finiteness predicate.
1.1.2.1. Decidable tableau calculus for a fragment of set theory involving function symbols and monotonicity predicates.
1.1.2.2. Proposal of new heuristics for the optimization of the decision problem.
1.1.3. Tableau calculus for the (hyper-)set unification algorithm developed in [DOP99].
1.1.4. Tableau calculus for the hyperset version of the theory MLSS.

1.2. Decidability in graph theory
Extension of the decision procedure presented in [CC00].

1.3. Decidability in other formal systems
1.3.1 Decision procedure for the language on lists which allows to express besides first-order constraints, also various lists constraints.
1.3.2. Decidability results on string covering.
1.3.3. Decision procedure for a fragment of elementary real analysis involving: point evaluation, sum, product, monotonicity and convexity predicates, and additivity over functions.
1.3.4. New method for the combination of decision procedures for ground theories whose signatures are not disjoint.

1.4. T-Resolution
Generalization/optimization of the completeness results to refinements of the base method; integration of some decidable fragments of set theory within T-resolution; characterization of fragments of relational algebra theories that are both decidable and suitable to be embodied into T-resolution.

2. Tarski-Givant map calculus
2.1. "Safe" map reasoning methods (meaning, basically, methods based on the implicit assumption that all maps are finite); techniques for translating Prolog-style declarative specifications with individual variables into logic-algebraic specifications; methods for simplifying map expressions and for proving equalities. We intend to publish these results into an extended research report, from which one or more journal papers will be extracted.
2.2. Extension of the Graph Thinning algorithm described in [CCO97] and characterization of the fragment of the language that can be translated in .
2.3. Description of an object-oriented programming language tailored for algebraic symbolic manipulation systems; specifications of hierarchies of algebraic classes in the mentioned language, with an emphasis on defining object properties.
2.4. Refining and completion of a prototype for visual manipulation.
2.5. Extensive testing of the map calculus and T-resolution with the tools for map reasoning such as Ralf, Relview and Libra.

3. Declarative programming with aggregate constraints
3.1. Completion of the development of the new CLP language with sets and multisets ñ here named {log}+.
3.2. Comparison of {log}+ with the language GAMMA, and study of the use of {log}+ to describe multiset rewriting based computations, such as those required in "membrane computing".
3.3. "Export" to Alma-0 of our techniques for set and multiset constraint handling to contexts other than those provided by the usual CLP scheme.
3.4. Study and design of a visual programming language, strongly based on the notion of set (and multiset), which provides the user with visual facilities for the definition of set (multiset) objects and for their manipulation, according to a set (multiset) rewriting paradigm.
3.5. Definition and management of intensional sets; application of static analysis tools to perform compile-time checks to help in the selection of the most adequate implementation strategy for the set collection operation possibly required by intensional sets evaluation.
3.6. Design of a new "Alma-like" declarative language embedding sets (L0), which provides most of the features of {log}+ within a Pascal-like framework.

4. A case study: the Four-Color Theorem
Singling out of concepts of algebraic logic which allow to formulate the Four-Color Theorem as a consistency theorem in a logic of planar graph colorings; study of the algorithmic aspects relative to the solution to the Four-Color Problem; formulation of such algorithms using the aggregate constructs studied in the present project.

Unita' di ricerca impegnate:

Fase 2

Durata:	12 mesi		Costo previsto:	0 M£		0 Euro

Descrizione:

Testo italiano

Durante la seconda fase del progetto, la ricerca si articolerà nelle seguenti tematiche:

1. Teoria computabile degli insiemi e decidibilità in sistemi
formali

1.1. Teoria computabile degli insiemi
1.1.1. Capitalizzando l'esperienza guadagnata durante la prima fase, nel corso della seconda fase si cercherà di applicare la metodologia dei processi formativi all'estensione di MLS con gli operatori di insieme-potenza, unione unaria e singoletto ed al trattamento del prodotto cartesiano.
1.1.2. Verranno anche investigate alcune euristiche per ottimizzare ulteriormente il problema della decisione con il metodo dei tableaux analitici.
1.1.3. Infine, si implementeranno e sperimenteranno nell'ambiente SETL-IDE gli algoritmi di decisione più efficienti prodotti nel corso del primo anno del progetto.

1.2. Decidibilità in teoria dei grafi
Si applicheranno i risultati ottenuti nel corso della prima fase a possibili scenari di verifica di correttezza (es. Teorema dei Quattro Colori).

1.3. Decidibilità in altri sistemi formali
1.3.1. Si cercherà di generalizzare i risultati di decidibilità conseguiti durante la prima fase riguardanti la teoria delle liste anche al caso del dominio degli interi e del dominio delle liste di individui.
1.3.2. Si generalizzeranno gli eventuali risultati su ricoprimento di stringhe ottenuti nel corso della prima fase.
1.3.3. Nell'ambito della dimostrazione automatica in analisi reale elementare, si cercherà di estendere ulteriormente il risultato ottenuto nella prima fase del progetto mediante alcuni predicati facenti riferimento alle derivate prime e seconde.
1.3.4. Si continuerà lo studio delle tecniche di combinazione di procedure di decisione per teorie ground con segnature non disgiunte.

1.4. T-Risoluzione
L'integrazione di algoritmi di decisione in un sistema basato sulla T-risoluzione avrà come suoi casi di studio prioritari casi desunti dalla teoria degli insiemi o dalla stessa teoria delle algebre di relazioni.

2. Calcolo mappale di Tarski-Givant
2.1. Le sperimentazioni da effettuarsi nel secondo anno del progetto prevedono: l'utilizzo di strumenti quali Otter ed EQP (dell'Argonne National Laboratory), per la logica del primo ordine; delle implementazioni SETL della T-risoluzione, per ragionamento in contesti specializzati (in particolare teorie degli insiemi); della piattaforma Schroeder (uno tra gli obiettivi del presente progetto) e degli strumenti Ralf, Relview e Libra, per il ragionamento mappale.
2.2 Il campo di validazione dei metodi di dimostrazione automatica che verranno studiati e messi in opera sarà principalmente il ragionamento sulle gerarchie di ereditarietà fra classi, ed in particolare classi algebriche da supportare con metodi di calcolo algebrico simbolico.
2.3. Sia per il calcolo mappale che per la T-risoluzione, la dimostrazione di efficacia dell'approccio richiede lo sviluppo di software di supporto alla sperimentazione. Per quanto riguarda l'abbinamento dei due approcci, è particolarmente necessario sviluppare tecniche di traduzione che conducano da un formalismo all'altro (nella misura in cui ciò è possibile). Questo perchè il formalismo del calcolo predicativo resta comunque più espressivo di quello mappale, e più vicino all'utente, mentre l'altro è più vicino alla macchina.
2.4. Relativamente all'approccio visuale al ragionamento in , ci si porrà come principale obiettivo lo sviluppo e la realizzazione completa di un sistema interamente basato su tecniche visuali per la traduzione da logica del primo ordine a e per il ragionamento automatico e semi-automatico in .

3. Programmazione dichiarativa con vincoli su aggregati
3.1. Si cercherà di migliorare le prestazioni dell'interprete del linguaggio {log}+ con l'utilizzo e la messa a punto di sofisticati strumenti di analisi statica di programmi. In particolare si intende avvalersi dell'analizzatore per programmi CLP China. Prima di tutto, questo strumento verrà impiegato per individuare porzioni particolarmente "critiche" nell'interprete {log}+ su cui intervenire per migliorarne l'efficienza complessiva. Quindi, si esplorerà la possibilità di utilizzare l'analisi statica per effettuare, ove possibile, una traduzione automatica di constraint {log}+ in constraint CLP(FD), il che dovrebbe comportare una riduzione sensibile dei tempi di esecuzione. Inoltre, si intende avvalersi dell' analisi statica di programmi in congiunzione con l'implementazione degli insiemi intensionali.
3.2. Si testerà l'implementazione di {log}+ su esempi non banali.
3.3. Si implementerà un semplice prototipo per il linguaggio L0. L'implementazione sarà basata su una traduzione diretta da programmi L0 a programmi {log}+, utilizzando l'interprete {log}+ per fornire l'ambiente di esecuzione dei programmi L0. Questo dovrebbe permetterci di raggiungere il nostro obiettivo in un tempo relativamente breve, sebbene rinunciando completamente a considerazioni di efficienza.
3.4. Si implementerà un semplice prototipo di un linguaggio visuale con insiemi (e multi-insiemi), progettato nella prima fase. L'implementazione si focalizzerà soltanto su quella parte del linguaggio riguardante la rappresentazione e manipolazione di insiemi e multi-insiemi, assumendo di utilizzare tecniche e linguaggi convenzionali (specificatamente, Java) per rappresentare tutte quelle situazionii non direttamente esprimibili in termini di operazioni di manipolazione di insiemi/multi-insiemi. Come linguaggio di implementazione si intende avvalersi del linguaggio Java ed, in particolare, di sfruttare le possibilità di manipolazione di oggetti grafici che esso fornisce. Intendiamo anche sfruttare le possibilità di risoluzione di vincoli fornite da {log}+ se nella progettazione del linguaggio visuale sarà possibile anche introdurre la possibilità di definire vincoli sugli aggetti visuali che è possibile manipolare.

4. Caso di studio: il Teorema dei Quattro Colori
Attraverso la valutazione dei risultati ottenuti negli esperimenti condotti nella corrispondente attività nel corso della prima fase, si cercherà di mettere in luce gli aspetti metodologici di maggior rilievo.

5. Realizzazione di un sito WEB su "Algoritmi di decisione e
programmazione dichiarativa con vincoli insiemistici"
Si realizzerà un sito WEB nel quale confluiranno tutti i risultati del progetto e che conterrà anche i link alla letteratura su "Algoritmi di decisione e programmazione dichiarativa con vincoli insiemistici".

Testo inglese

During the second phase of the project, the research will concern the following subject areas:

1. Computable set theory and decidability in formal systems

1.1. Computable set theory
1.1.1. The techniques developed during the first phase of the project will be applied also to try to solve the decision problem for the extension of MLS with the powerset, unary union, and singleton operators and to start the treatment of the cartesian product.
1.1.2. Further heuristics for the optimization of the decision problem with the tableau method will be investigated.
1.1.3. Finally, we intend to implement and experiment in the SETL-IDE environment the most interesting decision algorithms which have been discovered during the first phase of the project.

1.2. Decidability in graph theory
We will apply the results obtained in the first phase of the project to some proof scenarios, such as the Four-Color Theorem.

1.3. Decidability in other formal systems
1.3.1. We will try to further generalize the results obtained during the first year of the project relative to list theory to different domains, such as the domain of integers and the domain of lists of individuals.
1.3.2. We will further generalize the results on string covering obtained during the first phase.
1.3.3. In the field of automated proving in elementary real analysis, we will try to further extend the result obtained during the first phase of the project by some predicates referring to first and second derivates.
1.3.4. We will also continue the study of techniques to combine decision procedures of ground theories having non-disjoint signatures.

1.4. T-Resolution
The integration of decision algorithms within a system based on T-resolution will be studied w.r.t. case studies taken from set theory and relational algebra theories.

2. Calcolo mappale di Tarski-Givant
2.1. The testing activity for map reasoning for the second year will exploit: i) tools such as Otter and EQP (both from the Argonne National Laboratory) for first-order logic; ii) SETL and T-resolution, for reasoning in specialized contexts, and particularly in set theories, iii) Schroeder (whose development is one of the goals of this project) and other existing tools such as Ralf, Relview and Libra.
2.2 The domain where the automated proof methods considered in this project will be validated is that of reasoning about inheritance hierarchies of classes. Special attention will be bestowed to algebraic classes supported by symbolic algebraic methods.
2.3. To prove the effectiveness of both map calculus and T-resolution requires the development and the extensive testing of support tools. Also, combining the two approaches necessitates development of techniques to translate ---to the extent in which this is possible--- map calculus and quantified first-order logic one into the other. In fact, predicate calculus remains inherently more expressive, and closer to the user, than map calculus; conversely, map calculus is closer to the machine level.
2.4. Concerning the visual approach to reasoning in , a main goal will be the development of a system which is completely based on visual techniques for the translation from first-order logic to and for the (semi-)automatic reasoning in .

3. Declarative programming with aggregate constraints
3.1. We will attempt to improve the {log}+ interpreter implementation by using powerful static program analysis tools. Specifically, we plan to exploit the China analyzer. First of all, this tool will be used to find out "critical" parts in the {log}+ interpreter code which deserve to be modified in order to gain global efficiency. Then, it will be explored the possibility to use static analysis to perform, whenever it is feasible, automatic translation of {log}+ constraints to CLP(FD) constraints [***], which may result in a sensible reduction of program execution times. Furthermore, static program analysis will be exploited in conjunction with intensional set implementation.
3.2. We will test the {log}+ implementation on non-trivial applications
3.3. We will implement a simple prototype for the L0 language. The implementation will be based on a straightforward translation of L0 programs to {log}+ programs, using the {log}+ interpreter to provide a suitable execution environment for L0 programs. This should allow us to achieve our goal in a relatively short time, though completely ignoring efficiency matters.
3.4. We will implement a simple prototype for the visual programming language with sets/multisets designed in the first phase. The implementation will focus on (only) that part of the language concerned with the visual representation and manipulation of sets and multisets, assuming conventional programming techniques and languages (specifically, Java) are used for expressing algorithms not directly representable in terms of set/multiset manipulation operations. We plan to use Java as the implementation language and, in particular, to exploit Java's facilities for managing graphical objects. We plan also to exploit the {log}+ constraint solving facilities if the design of the visual language will make it possible to express constraints over the visual objects it deals with.

4. A case study: the Four-Color Theorem
By a careful evaluation of the results obtained during the first phase of the project, we will try to single out the most relevant methodological aspects.

5. Implementation of a WEB site on "Decision algorithms and declarative
programming with set constraints"
We will implement a WEB site to collect all results of the project and which will contain all the relevant links to the literature on "Decision algorithms and declarative programming with set constraints".

Risultati parziali attesi:

Testo italiano

I risultati parziali attesi alla fine della seconda fase sono raggruppati di seguito per tematica.

1. Teoria computabile degli insiemi e decidibilità in sistemi
formali

1.1. Teoria computabile degli insiemi
1.1.1. Procedura di decisione per l'estensione di MLS con gli operatori di insieme-potenza, unione unaria e singoletto; trattamento del prodotto cartesiano.
1.1.2. Ulteriori euristiche per ottimizzare il problema della decisione con il metodo dei tableaux analitici.
1.1.3. Implementazione e sperimentazione nell'ambiente SETL-IDE degli algoritmi di decisione più efficienti prodotti nel corso del primo anno del progetto.

1.2. Decidibilità in teoria dei grafi
Applicazione dei risultati ottenuti nel corso della prima fase a possibili scenari di verifica di correttezza (es. Teorema dei Quattro Colori).

1.3. Decidibilità in altri sistemi formali
1.3.1. Generalizzazione dei risultati di decidibilità conseguiti durante la prima fase riguardanti la teoria delle liste anche al caso del dominio degli interi e del dominio delle liste di individui.
1.3.2. Generalizzazione dei risultati di decidibilità su ricoprimento di stringhe ottenuti nel corso della prima fase.
1.3.3. Estendere del risultato di decidibilità in analisi reale mediante alcuni predicati facenti riferimento alle derivate prime e seconde.
1.3.4. Continuazione dello studio delle tecniche di combinazione di procedure di decisione per teorie ground con segnature non disgiunte.
1.3.5. Stesura di una prima bozza di una monografia sull'applicazione dei principali risultati di decidibilità alla verifica di correttezza di teoremi e di programmi.

1.4. T-Risoluzione
Sperimentazione dell'integrazione di algoritmi di decisione in un sistema basato sulla T-risoluzione.

2. Calcolo mappale di Tarski-Givant
2.1. Sperimentazioni mediante strumenti quali Otter ed EQP (dell'Argonne National Laboratory), per la logica del primo ordine; delle implementazioni SETL della T-risoluzione, per ragionamento in contesti specializzati (in particolare teorie degli insiemi); della piattaforma Schroeder (uno tra gli obiettivi del presente progetto) e degli strumenti Ralf, Relview e Libra, per il ragionamento mappale.
2.2. Sviluppo di tecniche di traduzione tra il formalismo del calcolo predicativo e quello mappale.
2.3. Implementazione di una piattaforma SETL denominata Schroeder, che sarà dotata di interfacce diagrammatiche verso l'utente, per la semplificazione di espressioni e dimostrazione di identità mappali; raccolta di compilatori e decompilatori fra calcolo predicativo (con quantificatori) e calcolo mappale implementati in Prolog.
2.4. Sviluppo e realizzazione completa di un sistema interamente basato su tecniche visuali per la traduzione da logica del primo ordine a e per il ragionamento automatico e semi-automatico in .

3. Programmazione dichiarativa con vincoli su aggregati
3.1. Ottimizzazione dell'interprete del linguaggio {log}+ con l'utilizzo e la messa a punto di sofisticati strumenti di analisi statica di programmi.
3.2. Sperimentazione di {log}+ su esempi non banali.
3.3. Implementazione di un semplice prototipo per il linguaggio L0.
3.4. Implementazione di un semplice prototipo di un linguaggio visuale con insiemi (e multi-insiemi), progettato nella prima fase.

4. Caso di studio: il Teorema dei Quattro Colori
Individuazione degli aspetti metodologici di maggior rilievo attraverso la valutazione dei risultati ottenuti negli esperimenti relativi allo scenario di dimostrazione del Teorema dei Quattro Colori.

5. Realizzazione di un sito WEB su "Algoritmi di decisione e programmazione dichiarativa con vincoli insiemistici"

Testo inglese

The partial results expected at the end of the first phase are grouped below according to their research subject.

1. Computable set theory and decidability in formal systems

1.1. Computable set theory
1.1.1. Decision procedure for the extension of MLS with the powerset, unary union, and singleton operators; treatment of the cartesian product.
1.1.2. Further heuristics for the optimization of the decision problem with the tableau method.
1.1.3. Implementation and experimention in the SETL-IDE environment of the most interesting decision algorithms which have been discovered during the first phase of the project.

1.2. Decidability in graph theory
Application of the results obtained in the first phase of the project to some proof scenarios, such as the Four-Color Theorem.

1.3. Decidability in other formal systems
1.3.1. Generalization of the results obtained during the first year of the project relative to list theory to different domains, such as the domain of integers and the domain of lists of individuals.
1.3.2. Generalization of the results on string covering obtained during the first phase.
1.3.3. Extension of the decidability result in elementary real analysis by allowing also some predicates referring to first and second derivates.
1.3.4. Prosecution of the study of techniques to combine decision procedures of ground theories having non-disjoint signatures.
1.3.5. First draft of a monograph on the applications of the most relevant decidability results to the verification of theorem and program correctness.

1.4. T-Resolution
Experimentation of the integration of decision algorithms within a system based on T-resolution.

2. Calcolo mappale di Tarski-Givant
2.1. Testing activity with the following tools: i) Otter and EQP (both from the Argonne National Laboratory) for first-order logic; ii) SETL and T-resolution, for reasoning in specialized contexts, and particularly in set theories, iii) Schroeder (whose development is one of the goals of this project) and other existing tools such as Ralf, Relview and Libra.
2.2. Development of techniques to translate between the formalism of quantified first-order logic and that of map calculus.
2.3. Creation of a SETL platform called Schroeder, endowed with diagrammatic user-interfaces, for simplifying map expressions and proving map identities; creating a repertory of Prolog-based compilers to and from predicate calculus (with quantifiers) and map calculus.
2.4. Development of a system which is completely based on visual techniques for the translation from first-order logic to and for the (semi-)automatic reasoning in .

3. Declarative programming with aggregate constraints
3.1. Optimization of the {log}+ interpreter implementation by using powerful static program analysis tools.
3.2. Test of the {log}+ implementation on non-trivial applications.
3.3. Implementation of a simple prototype for the L0 language.
3.4. Implementation of a simple prototype for the visual programming language with sets/multisets designed in the first phase.

4. A case study: the Four-Color Theorem
Singling out of the most relevant methodological aspects, through a careful evaluation of the results obtained in the experimentation with the Four-Color Theorem proof scenario.

5. Implementation of a WEB site on "Decision algorithms and declarative programming with set constraints"

Unita' di ricerca impegnate: