Research activity in 2000
The research activity in 2000 has mainly addressed the following topics.
a) Proof methods for nonclassical logics.
a.1) Proof methods for multimodal logics.
We have studied a class of multimodal systems (defined by Catach and also called "incestual modal logics") that can be non-homogeneous and can contain interaction axioms. For this class we have developed a prefixed analytic tableaux calculus and, by using it, we have shown some decidabilty results about multimodal logics.
a.1) Deduction methods for many-valued
An important issue in the area of many-valued and fuzzy logics is the development of analytic proof-systems on the style of the standard ones for classical logic (tableaux, sequent calculi, natural deduction etc.). We have developed a tableaux 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 a reduction of validity in this logic to integer programming.
We have carried on this research within the Italian-Austrian project started in 98, involving D. Mundici from the Università di Milano and M. Baaz and C. Fermüller from Wien Technical University.
a.2) 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 (see 2). 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.
a.3) 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. This research, carried on in collaboration with Prof. Gabbay of King's College of London, has lead to the publication of a volume: "Goal-Directed Proof-Theory" by D. M. Gabbay and N. Olivetti that has appeared by Kluwer Academic Publishers.
a.4) Proof-Methods for nonmonotonic logics
In collaboration with P.A. Bonatti from the Università di Milano, we have carried on the program (started a few years ago) of developing uniform and analytic proof-methods for the major families of nonmonotonic logics. The program aims to achieve a presentation of every nonmonotonic formalism in terms of simple sequent calculi. The essential features of these proof methods are that they are analytic, they comprise an axiomatic rejection method (in the form of a sequent calculi by itself), and that they make use of provability assumptions. After default logic and circumscription, we applied this methodology to autoepistemic logic, and we have provided a proof-theoretic formalization of both skeptical and credulous autoepistemic reasoning.
b) 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. We have concentrated on the study of iterated belief revision systems, where a sequence of changes to the knowledge bases is induced by a sequence of observations. We have proposed a formalization of iterated belief revision systems by strengthening the postulates proposed by Darwiche and Pearl.
In our setting, belief revision process is a function of epistemic states rather than of belief sets, where an epistemic state can be intuitively identified with a theory together with a set of revision strategies. We have then proposed a conditional logic IBC for representing iterated belief revision. The conditional logic IBC itself has a standard semantics in terms of selection function models and it provides a natural representation of epistemic states.
To this regard, we have obtained a representation result, which establishes a one-to-one correspondence between iterated belief revision systems and IBC-models (satisfying a covering condition). By this result, one can explicitly define (iterated) revision operators by means of conditional theories.
We are currently studying 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.
c) Agent programming languages
The problems related to the development of intelligent agents have been the mainstream of our researches about knowledge representation and reasoning. In particular, our formalization is based on a modal approach in a logic programming setting. Following the work of the past years about a modal logic programming language to reasoning about actions, which mainly focuses on ramification problem, we have defined a new logic language, DyLOG, which extends the previous one allowing to define procedures (possibly non-deterministic) as complex actions, to represent incomplete states and to deal with sensing actions. The fundamental characteristic that makes this language particularly interesting for agent programming is that, being based of a formal theory of actions, it can deal with reasoning about actions' effects in a dynamically changing environment and, as such, it supports planning, i.e. extraction from a procedure of an execution path (sequence of primitive actions) which leads to a terminating state where some goal holds. An interpreter for our language has been implemented by means of Sicstus Prolog 3 and it is available on the Web at the address http://www.di.unito.it/~alice.
Finally, from an application point of view, we have studied how DyLOG can be used to implement adaptive presentation on the Web, where personalized dynamic site generation is guided by user needs. Adaptation at the navigation level is realized by dynamically building a presentation plan for solving the problem of assembling a computer.
d) Applications of logic programming to databases.
d.1) Applications of logic programming to security in heterogeneous/federated databases.
The problem of integrating heterogeneous security specifications in a discretionary, role based framework has been tackled in collaboration with Prof. Elisa Bertino, Prof. Piero Bonatti and
Dr. Elena Ferrari, from the Università di Milano. A specification model independent from the underlying database model has been formalized. A number of formal properties of our mechanisms for granting/revoking authorizations have been studied, in terms of specific safeness properties of corresponding logic programs. Authorizations are periodic, their validity is specified through periodic temporal expressions, and they can be inherited according to role and object hierarchies. Formal methods to merge heterogeneous hierarchies without violating the security of data have been developed. A methodology for supporting temporal authorizations in heterogeneous, distributed systems is provided.
The results are accepted for publication on the Journal of Computer Security.
d.2) Applications of logic programming to multimedia databases
In collaboration with Prof. Sibel Adali (Rensselaer Polytechnic Institute, Troy, NY), and Paolo Terenziani (Università del Piemonte Orientale), we have extended our architecture for creating interactive multimedia presentation databases, whose definition had been proposed in 1999. In the original architecture, we defined the concept of an interactive multimedia database, that consists of static as well as dynamic interactive presentations, and developed a set of algebraic operations on these databases (including very general versions of select, project and join type operations from the relational algebra). Then we defined a notion of validity, shown how validity can be preserved for different operations, and developed methods for implementing different operations in the algebra.
The extended architecture provides an efficient treatment of temporal constraints possibly defined on the multimedia presentation.
e) Image classification and recognition
In cooperation with Davide Cavagnino, Matteo Baldoni and Cristina Baroglio have also studied the use of Iterated Function Systems in image representation for classification and recognition.
2000 Publications
Adali S., Console L., Sapino M.L., Schenone M. and Terenziani P. Representing and Reasoning with temporal constraints in Multi Presentations. IEEE INTERNATIONAL WORKSHOP ON TEMPORAL REPRESENTATION AND REASONING-TIME, IEEE Computer Society Press, Cape Breton, Nova Scotia, pp. 3-11, Canada, Luglio, 2000.
Adali S., Sapino M.L., Subrahmanian V.S. An Algebra for Creating and Querying Multimedia Presentations"-MULTIMEDIA SYSTEMS, Vol. 8, pp. 212-230, 2000.
Baldoni M. Normal Multimodal Logics with Interaction Axioms, in "Labelled Deduction". editors: D. Basin, M. D'Agostino, D. M. Gabbay, S. Matthews e L. Viganò, Kluwer Academic Publisher, pp. 33-57, The Netherlands, 2000.
Gabbay D.M. and Olivetti N. Goal-Directed Proof Theory. pag. 266, Kluwer Academic Publisher, Dordrecht, The Netherlands, 2000.
Giordano L., Martelli A. and Schwind C. Reasoning About Actions in Dynamic Linear Time Temporal Logic. FAPR - FORMAL AND APPLIED PRACTICAL REASONING, Technical Report Imperial College ISSN 1469-4166, pp. 117-129, Londra - U.K., Settembre, 2000.
Giordano L., Martelli A., Schwind C. Ramification and Causality in a Modal Action Logic, JOURNAL OF LOGIC AND COMPUTATION, Vol. 10, No. 5, pp. 625-662, 2000.
Olivetti N. Tableaux for Lukasiewicz infinite-valued logic. MEMORIAM P.MIGLIOLI CONSTRUCTIVISM IN NON-CLASSICAL LOGICS AND COMPUTER SCIENCE, pp. 0-4, Mantova, Italia, Ottobre, 2000.
Olivetti N., Gliozzi V. and Giordano L. A Conditional Logic for Iterated Belief Revision. ECAI - EUROPEAN CONFERENCE ON ARTIFICIAL INTELLIGENCE, IOS Press, pp. 28-32, Berlino, Germania, Agosto, 2000.
Olivetti N., Sapino M.L. Gabbay D., Giordano L., Martelli A. Conditional Reasoning in Logic Programming. JOURNAL OF LOGIC PROGRAMMING, Vol. 44, pp. 37-74, 2000.
Patti V., Martelli A., Chiarotto A., Baroglio C. and Baldoni M. Intention-guided Web Sites: A New Perspective on Adaptation. ERCIM-WORKSHOP USER INTERFACE FOR ALL, pp. 68-82, Firenze, Italia, Settembre, 2000.
Patti V., Martelli A., Giordano L. and Baldoni M. Modeling Agents in a Logic Action Language. FAPR - FORMAL AND APPLIED PRACTICAL REASONING, pp. 0-7, Londra, U.K., Settembre, 2000.
Sapino M.L., Liepins J. and Adali S. Dynamic Graph Structured Document Databases. WORKSHOP ON MULTIMEDIA INFORMATION SYSTEMS, pp. 187-196, Chicago, USA, Ottobre, 2000.
