People

Research activity in 2001

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

(1) Proof methods for nonclassical logics.

(1a) Deduction methods for many-valued logics

An important issue in the area of many-valued and fuzzy logics is the development of analytic proof-systems in the style of the standard proof methods for classical logic (tableaux, sequent calculi, natural deduction etc.). We have developed a tableau method for Lukasiewicz infinite valued logic, which is one of the most important fuzzy-logic systems. The tableaux system is based on the possible world semantics of this logic developed by Urquhart-Scott and it provides an efficient reduction of validity in this logic to mixed integer programming. The investigation of the relation between many-valued logic and substructural logic, has lead us to study a proof-theoretical formulation of the lattice-ordered Abelian logic proposed by Meyer and Slaney as a foundation of relevance logic. Since Lukasiewicz logic can be naturally interpreted in Abelian logic, this research can provide an analytic proof theory for Lukasiewics logic.

(1b) Deduction methods for conditional logics

Conditional logics are a generalization of modal logic which have been used to represent hypothetical, counterfactual and nonmonotonic reasoning. Moreover, they have been studied to formalize belief revision and update. In collaboration with C. Schwind of Marseille University, we have developed labelled tableaux and sequent calculi for conditional logics based on the selection function semantics. These methods provide not only analytic proof methods and decision procedures for the logics under investigations, but have also allowed us to obtain some sharper complexity results for some logical systems, such as the minimal conditional logic CK.

(1c) Goal directed proof procedures for non-classical and modal logics.

Following the work of the past years, the research has been devoted to the study of goal-directed proof procedures for non-classical logics. The underlying idea of the methodology is to extend the paradigm of deduction typical of logic programming to several families of non-classical logics. We have carried on this research together with D. Gabbay of King's College, London. The current research is aimed to use the goal-directed methods to investigate properties of logical systems, such as interpolation and complexity bounds.

In collaboration with L. Giordano from the Universitą del Piemonte Orientale, we have studied the problem of capturing belief revision within a conditional logic. Finding a direct mapping between conditional logic and belief revision is problematic, as the well-known "triviality result" by Gärdenfors has shown. This research has lead us to discover a conditional logic BC wich represent belief revision in terms of a semantic mapping between revision systems and selection function models. These results, originally obtained for AGM reivision systems, have then been extended to iterated revision system as defined by Darviche and Pearl.

We have continued this line of research by studying how to provide a direct mapping between revision systems and conditional theories through the so-called Ramsey Test, without incurring in the triviality result. 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 objective, that is to say to non conditional formulas. We have shown that this weaker formulation is compatible with the Ramsey Test in the sense that there are non-trivial revision systems which satisfy it. We are currently investigated the conditional logic individuated by our restricted revision postulates and various versions of the Ramsey test.

The problem of enforcing security in heterogeneous/federated databases by means of logical formalisms has been addressed, in collaboration with professor Sushil Jajodia (George Mason University, Fairfax), professor Pierangela Samarati (Universitą di Milano) and professor V.S. Subrahmanian (University of Maryland, College Park). A general framework has been proposed, that allows multiple control mechanisms to be expressed within a single system. The framework is based on a language through which users can specify security policies to be enforced on specific accesses. The language allows the specification of both positive and negative authorizations and incorporates notions of authorization derivation, conflict resolution, and decision strategies. Different strategies may be applied to different users, groups, objects, or roles, based on the needs of the security policy. The overall result is a flexible and powerful, yet simple, framework which can easily capture many of the traditional access control policies as well as protection requirements that exist in real world applications, but are seldom supported by existing systems.

(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 theory for reasoning about actions which is 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 action theory allows to reason with incomplete initial states, to do postdiction, to deal with ramification and with nondeterministic actions. Planning can be modeled as satisfiability in DLTL. This theory has been extended to describe the behaviour of a network of sequential agents, which coordinate their activities through common actions.

(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 ramification problem, we have refined the agent logic programming language DyLOG both from a theoretical and a 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.

At the same time, we built a system, WLog, that allows web-based recommendation systems to be developed in a multi-agent setting. The system has been tested on an e-tutoring application, where students are supported in the process of developing study plans that will allow them to acquire some desired competence. The core of the architecture is a set of reasoning agents, implemented in DyLOG, which exploit the reasoning-about-action features supplied by the language both for planning study courses and to perform temporal projection in order to evaluate the correctness of study plans proposed by students. A first version of WLog has been implemented (documentation is available at the address: http://www.di.unito.it/~alice) and an improved version is under development.