DIPARTIMENTO   DI   INFORMATICA
Università di Torino

Research Report Year 2001

Computer Science

Artificial Intelligence and Human-Computer Interaction

  People   Research Activities   Publications   Software Products   Research Grants

Logic Programming and Automated Reasoning

People

Alberto Martelli

Full Professor

mrt[at]di.unito.it

Maria Luisa Sapino

Senior Researcher

mlsapino[at]di.unito.it

Nicola Olivetti

Senior Researcher

olivetti[at]di.unito.it

Matteo Baldoni

Researcher

baldoni[at]di.unito.it

Cristina Baroglio

Researcher

baroglio[at]di.unito.it

Valentina Gliozzi

Ph.D Student

gliozzi[at]di.unito.it

Viviana Patti

Short term researcher

patti[at]di.unito.it

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.

 

(2) Belief Revision and Conditional Logics

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.

 

(3) Applications of Logic Programming to security in heterogeneous/federated databases

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.

 

(4) Agent programming languages and reasonig about actions

(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.

2001 Publications

M. Baldoni, C. Baroglio, A. Chiarotto, and V. Patti. Programming Goal-driven Web Sites using an Agent Logic Language. In I. V. Ramakrishnan, editor, Proc. of the Third InternationalvSymposium on Practical Aspects of Declarative Languages,  Lecture Notes in Computer Science, vol. 1990 pages 60-75, Las Vegas, Nevada, USA, march 2001. Springer.

M. Baldoni, L. Giordano, A. Martelli, and V. Patti. Reasoning about Complex Actions with Incomplete Knowledge: A Modal Approach. In A. Restivo, S. Ronchi Della Rocca, and L. Roversi, editors, Proc. of Theoretical Computer Science, 7th Italian Conference, ICTCS'2001, Lecture Notes in Computer Science, vol. 2202 pages 405-425, Turin, Italy, 2001. Springer.

L. Giordano, A. Martelli, and C. Schwind. Reasoning About Actions in a Multiagents Domain. In Proc. of the 7th Congress of the Italian Association for Artificial Intelligence, AI*IA'01, volume 2175 of LNAI, pages 237-248, Bari, 2001.

L. Giordano, V. Gliozzi, and N. Olivetti. Belief Revision and The Ramsey Test: a solution. In Proc. AI*IA 2001, Italian Conference on Artificial Intelligence, volume 2175 of LNAI, pages 165-180, Bari, Italy, 2001. Springer.

N. Olivetti and C. Schwind. A sequent calculus and a complexity bound for minimal conditional logic. In A. Restivo, S. Ronchi Della Rocca, and L. Roversi, editors, Proc. of Theoretical Computer Science, 7th Italian Conference, ICTCS'2001, Lecture Notes in Computer Science, vol. 2202 pages 384-404, Turin, Italy, 2001. Springer.

L. Giordano, A. Martelli, and C. Schwind. Reasoning About Actions in Dynamic Linear Time Temporal Logic. Journal of the IGPL, 9(2):298-303, 2001.

S. Jajodia, P. Samarati, M. L. Sapino, and V. S. Subrahmanian. Flexible Support for Multiple Access Control Policies. ACM Transactions on Database Systems, 26(2):214-260, June 2001.

M. Baldoni, C. Baroglio, and V. Patti. Structereless, Intention-guided Web Sites: Planning Based Adaptation. In C. Stephanidis, editor, Universal Access in HCI: Toward an Information Society for All, Proceedings of the 9th International Conference on Human-Computer Interaction (HCII 2001), Symposium on Human Interfaces 2001, 4th Intrnational Conference on engineering Psychology and Cognitive Ergonomics, 1th International Conference in Human-Computer Interaction, volume 3, pages 237-241, New Orleans, LA, USA, August, 2001. Lawrence Erlbaum Associates, Inc.

M. Baldoni, C. Baroglio, A. Molia, and V. Patti. Exploiting planning capabilities of a rational agent in adaptive web-based recommendation systems: a case-study. In S. Pizzutilo, editor, Proc. of AI*IA 2001, Demo Session, pages 9-12, Bari, Italy, September 2001.

Software Products

Developers

Name of Product

Type

Brief Description

Year

Matteo Baldoni, Cristina Baroglio, Viviana Patti

WLog 1.0

Multiagent system

Multiagent system designed to implement recommandation systems

2001

Research Grants

Title of project

Project leader

Funding Organization

Kind of grant

Metodi di ragionamento basati su Logiche non-classiche e programmazione Logica

A. Martelli

Universitą di Torino

Local Research

 

Department home [Information] [People] [Research] [Ph.D.] [Education] [Library] [Search]
[Bandi/Careers] [HelpDesk] [Administration] [Services] [Hostings] [News and events]

Administrator: wwwadm[at]di.unito.it Last update: Apr 12, 2002