Research activity in 1999
The research activity in 1999 has mainly addressed the following topics.
(1) Proof methods for nonclassical logics.
(1a) 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 developed a prefixed analytic tableaux calculus and, by using it, we have shown some decidabilty results about multimodal logics.
(1b) Goal directed proof procedure 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. One of the main advantages of goal-directed proof-systems with respect to other traditional methods, is that they are more efficient and deterministic for the proof-search. This research has been carried on in collaboration with Prof. Gabbay of King's College of London. Continuing the work of the last years we have been able to capture within this framework a wide range of non classical logics, stretching from modal logics to substructural logics (relevance, linear logic etc…). We have further studied the extension of the framework to intermediate and many-valued logics, among them the logic of finite-height Kripke models and Dummett-Goedel logic LC which is considered one of the most important fuzzy logics.
This research has lead to the publication of a volume: “Goal-Directed Proof-Theory” by D. M. Gabbay and N. Olivetti which is currently in press by Kluwer Academic Publishers.
(1c) Deduction methods for many-valued logics and related systems
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 analytic proof methods for some finite and infinite many-valued logics, taking advantage of the connection between substructural, intermediate and many-valued logics. The proof methods we have developed are based on hypersequents, a useful generalization of ordinary sequents studied by Avron, which are suitable for expressing disjunctive properties in an analytic way.
On these issues we have promoted an Italian-Austrian research cooperation, involving D. Mundici of Milan University and M. Baaz and C. Fermüller of Wien Technical University. The title of the bilateral action is "Analytic Proof Methods for Fuzzy logics".
(2) 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 define a new logic language, DyLOG+, which extends the previous one allowing to define procedures as complex actions, to represent incomplete states and to deal with sensing actions. Complex actions are defined by means of Prolog-like clauses. They are defined in a recursive and non-deterministic way in terms of atomic and other complex actions and they allow to specify the behaviours of an agent. With this language we deal with both projection problem and planning problems, i.e. to extract from a procedure an execution path which leads to a terminating state where some goal holds. A goal directed proof procedure for the language is provided, which allows to reason about complex actions in presence of sensing and to generate conditional plans. The frame problem is given a non-monotonic solution by using persistency assumptions in an abductive setting.
(3) Iterated belief revision and conditional logics
Continuing the work of the past year, 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 are induced by a sequence of observations.
Firstly we have proposed a formalization of iterated belief revision systems by strengthening the postulates proposed by Darwiche and Pearl. In our setting, the 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. Each iterated belief revision system corresponds to a IBC-model and every IBC-model satisfying the covering condition determines an iterated belief revision system.
(4) Applications of logic programming to databases.
(4a) 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 (University of Milan). 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.
The results have been presented to the 13th IFIP WG 11.3 Working Conference on Database Security, Seattle, (whose proceedings will be published in a forthcoming book, edited by Kluwer) and to the conference Appia-Gulp-Prode99 Conference, L'Aquila,
(4b) Applications of logic programming to multimedia databases
In collaboration with Prof. VS Subrahmanian (University of Maryland at College Park) we have started developing an architecture for creating interactive multimedia presentation databases. In particular, we have 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 have 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 query language can also be used as an authoring tool for multimedia presentation archives. A number of host equivalence results for queries in this algebra, which may be used to optimize the queries, have been proved.
These results have been presented at the ACM SIGMOD Conference in Seattle, to the Fifth International Workshop on Multimedia Information Systems, MIS99, and have been accepted for publication in the ACM Multimedia Systems Journal – Special Issue on Multimedia Presentations.
(5) Image classification and recognition.
In cooperation with Cristina Baroglio and Davide Cavagnino, Matteo Baldoni has also studied the use of Iterated Function Systems in image representation for classification and recognition.
1999 Publications
Riviste
A. Ciabattoni, D.Gabbay, N. Olivetti. "Cut-free proof systems for logics of weak excluded middle", Soft Computing, 2(4): 147-156, 1999.
Atti di congressi internazionali
E. Bertino, P.A. Bonatti, E. Ferrari, M.L. Sapino, "Specifying and Computing Hierarchies of Temporal Authorizations", In pre-proceedings of the 13th IFIP WG 11.3 Working Conference on Database Security, Seattle, pp. 217-241, 1999.
S. Adali, M.L. Sapino, Subrahmanian, "A Multimedia Presentation Algebra", In SIGMOD RECORD Vol. 28 No. 2 - June 99 (special issue on SIGMOD 99), pp. 121-132, 1999.
S. Adali, M.L. Sapino, M. Schenone, V.S. Subrahmanian, "Finite Graph Algebras for Querying Multimedia Presentation Databases", In Proceedings MIS'99 - Fifth International Workshop on Multimedia Information Systems, 8 pag., 1999.
N. Olivetti, "Tableaux for nonmonotonic logics", In (M. D'Agostino et al. eds.) Handbook of Tableau Methods, Kluwer Academic Publishers, Dordrecht, pp. 469-528, 1999.
E. Bertino, P.A. Bonatti, E. Ferrari, M.L. Sapino, Specifying and Computing Hierarchies of Temporal Authorizations", In Proceedings Appia-Gulp-Prode99 Conference, L'Aquila, pp. 605-619, 1999.
