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