The research activity in 2002 has mainly addressed the following topics.

Whereas the semantic foundations of fuzzy logics based on t-norms and their residua have been investigated in depth, the proof theory for this group of logics is still underdeveloped. In collaboration with G. Metcalfe from King's College, London, we have developed analytic proof systems for Lukasiewicz infinite-valued logic, one of the fundamental systems of fuzzy logics. Our strategy has been to take advantage of the embedding of this logic into abelian logic, introduced independently by Meyer and Slaney as a relevance logic, and by Casari as a comparative logic. We have first given several calculi (sequent calculi, hypersequent calculi, and labelled calculi) for abelian logic and then used the embedding to find calculi for Lukasiewicz logic. We have also started to investigate some termination, complexity, and optimization issues for all the systems covered.

The strategy of embedding fuzzy logics into suitable comparative could be possibly applied to discover proof methods for other systems in the neighborhood of fuzzy logics (such as product logic and Hajek's basic logic) lacking a natural proof-theory. This is object of the current research.

In collaboration with D. Gabbay from King's College, London, we have carried on our study of goal-oriented proof procedures for non-classical logics. The research has concentrated in the use of the goal-directed methods to investigate properties of logical systems, such as interpolation. In particular we have studied interpolation properties for a variety of implicational logics, covering intuitionistic and classical logic, substructural logics, and modal logics of strict implication. We have been able to provide a constructive proof of the interpolation property based on the goal-directed formulation of these logics. The investigation has also lead to formulate and study some useful generalizations of the standard interpolation property in the context of substructural logics, namely the notion of chain/iterated interpolation and the notion of structural interpolation.

In collaboration with L. Giordano from the Università del Piemonte Orientale, we have investigated how to capture belief revision within a conditional logic. Continuing the previous research we have shown how to provide a direct mapping between revision systems and conditional theories through the so-called Ramsey Test, without incurring in the well-known triviality result by Gärdenfors. To this aim, we have investigated a weaker formulation of the AGM postulates, where the "minimal change principle" which characterizes the revision operation, is restricted to non-conditional formulas.

We have then derived the conditional logic BCR from our revision postulates by means of a strong version of the Ramsey Test. This logic is sound, complete (with respect to its standard selection function models semantics) and decidable. It turns out that the logic BCR provides a logical formalization of belief revision in the language of conditional logic, as there is an isomorphism between belief revision systems and selection function models of this logic.

The problem of knowledge extraction and manipulation in the field of image databases has been studied, in conjunction with a group of researchers from the University of Napoli.

When dealing with image data, the traditional notion of "exact match" between the query values, and the ones appearing in the database, is replaced by a notion of "similarity", a notion which is strongly related with uncertainty.

A new relational model has been proposed, in which feature information automatically extracted from images, or manually given by human experts, are recorded, associated with some degree of fuzzyness. And new algebraic operators, with equivalence results, have been defined to properly combine fuzzy relations, and extract information out of them.

The problem of querying non structured information sources has also been studied in the context of multimedia presentations, in collaboration with the University of Venezia.

A class of multimedia presentations made of independent and synchronized media has been introduced, and a retrieval model, able to reconstruct the fragments of a presentation from the atomic components returned when querying multimedia presentation repositories, has been defined.

The retrieval model is based on an automaton which formally describes the presentation states entered by the events which trigger media playback. Retrieving a consistent fragment corresponds to building a new presentation with all the media related to the retrieved ones, with their original structural and synchronization relationships.

(4a) Reasoning about actions

With Laura Giordano from the Università del Piemonte Orientale and Camilla Schwind from the University of Marseille we have developed a logical framework for specifying and verifying systems of communicating agents, based on Dynamic Linear Time Temporal Logic (DLTL). DLTL is a simple extension of propositional temporal logic of linear time in which regular programs of propositional dynamic logic can be used for indexing temporal modalities. The framework provides a simple formalization of the communicative actions in terms of their effects and preconditions, and the specification of the interaction among agents by means of temporal constraints.

(4b) Agent programming languages and implementations

Following the work of the past years about a modal logic programming language for reasoning about actions, which mainly focuses on the ramification problem, we have refined the agent logic programming language DyLOG both from a theoretical and an implementative point of view. We have studied how to extend the language and its proof procedure for managing a multi-agent scenario, starting from a set of primitive communicative acts. We are currently implementing and studying communication protocols that we mean to exploit in future implementations.

After the work carried on in the last years on the DyLOG agent programming language, we have studied how to apply techniques from the research area of reasoning about actions and change to the design and implementation of adaptive tutoring systems. Such systems exploit planning, temporal projection and temporal explanation while interacting with the user with the aim of building personalized study plans or to verify the correctness user-built study plans. When a user-given plan is not correct or does not allow the user to reach his learning goals, the system explains the reasons of failure. The experience on the e-learning applications was very helpful in defining the basis of a framework for modeling and comparing adaptive hypermedia for tutoring applications, in a joint work with Nicola Henze, from the University of Hannover.

In collaboration with A. Messina and R. Del Pero, from RAI Radiotelevisione Italiana, Centro Ricerche e Innovazione Tecnologica, we have been developing a formal framework for the representation of audiovisial material produced or broadcasted by a TV company. Such a framework captures both features related to the making of audiovisiual objects and features related to their inner structure. A prototype of the framework has been implemented.