Research activity in 1998
The research activity in 1998 has mainly addressed the following topics.
(1) Proof methods for nonclassical logics.
(1a) Proof methods for multimodal logics.
We have studied the class of inclusion and incestual modal logics introduced by Catach which include, among the others, modal and multimodal systems characterized by serial, symmetric, transitive, and Euclidean accessibility relations. These systems can be non-homogeneous (i.e. every modal operator is not restricted to the same system) and can contain some interaction axioms (i.e. each modal operator is not necessarily independent from the others). For this class of logics we developed a prefixed analytic tableaux calculus, whose main feature is that it can deal in a uniform way with any multimodal logics in this class. We proved some (un)decidability results about multimodal logics, and we used the prefixed tableau method to show undecidability of a wide subclass.
(1b) Goal directed proof procedure for non-classical and modal logics.
Following the work of the past year, 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 modal logics of strict implication and of substructural logics. We are currently studying the extension of the framework to intermediate and many-valued logics, first of all Dummett-Goedel logic which is considered one of the most important fuzzy logics. We are also investigating how to obtain proof-procedures of optimal complexity based on goal-directed deductions.
Focusing on the specific class of multimodal logics which are characterized by inclusion axioms, we have defined a framework for developing modal extensions of logic programming which allow sequences of modalities to occur in front of clauses, goals and clause heads. A goal directed proof procedure for the language has been proposed, which is modular with respect to the properties of modalities.
(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. In a few words, a common feature of several systems of many-valued logics and intermediate logics is the fact they both satisfy some weakened form of excluded-middle principle. On the other hand, a common feature of several many-valued logics, such as Lukasiewicz logics and substructural logics, is the distinction between multiplicative (or monoidal) connectives additive (or lattice) connectives due to the rejection of the structural rule of contraction. 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) Reasoning about actions and change
Modal logic allows to formalize in a very natural way reasoning about a world that dynamically changes under effects of actions, by representing actions by means of modal operators. In this context, we have developed, in collaboration with Camilla Schwind of the Laboratoire d'Informatique de Marseille, CNRS, a modal action theory in which persistency is achieved by using a nonmonotonic formalism which maximizes persistency assumptions. The problem of ramification is tackled by introducing a modal causality operator which is used to represent causal rules. Furthermore, we have studied the clausal fragment of this action theory by defining a modal logic programming language to reason about actions. The language can be regarded as an extension of Gelfond and Lifschitz' high-level action language A.
In order to deal with concurrent actions, we have extended the action language by introducing two different modalities for dealing with "open'' and "closed'' actions. We have shown that causal rules play a crucial role for modelling concurrent actions.
More recently, we have defined a further extension of this language called DyLOG, which allows to define procedures, to build up complex actions from elementary ones. Moreover, it allows to specify action preconditions making use of existential modal operators. A goal-directed proof procedure for the language is provided. The frame problem is given a non-monotonic solution in the context of an abductive characterization.
(3) Belief revision and conditional logics
In spite of the similarities between the semantics of belief revision and the evaluation of conditionals, very intuitive acceptability criterion proposed by Ramsey (the Ramsey Test) leads to the well known Triviality Result by Gärdenfors, which claims that there are no significant belief revision systems that are compatible with the Ramsey test.
We have focused on the problem of capturing belief revision within a conditional system by moving to a less stringent formulation of the Ramsey test. More precisely, if we accept a conditional proposition with respect to a belief set K, this does not entail that we are willing to accept it with respect to every larger belief set. We have introduced a conditional logic BC to represent belief revision. Logic BC has a standard semantics in terms of possible worlds structures with a selection function and has strong similarities with Stalnaker's logic C2. Gärdenfors' Triviality Result does not apply to BC. We have provided a representation result, which shows that each belief revision system corresponds to a BC-model and every BC model satisfying the covering condition determines a 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 is being tackled in collaboration with Prof. Elisa Bertino (University of Milan). The specification model is independent from the database model, and hence it applies to many kinds of heterogeneous databases. 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 are being developed.
(4b) Applications of logic programming to multimedia databases
In collaboration with Prof. VS Subrahmanian (University of Maryland at College Park) we are developing an architecture for creating interactive multimedia presentation databases based on multimedia presentations. 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.
1998 Publications
S. Adali, P.A. Bonatti, M.L. Sapino, V.S. Subrahmanian, A Multi-Similarity Algebra, Proc. ACM SIGMOD98, Seattle, pp. 402-423, 1998
M. Baldoni, L. Giordano, and A. Martelli. A Tableau Calculus for Multimodal Logics and some (Un)Decidability Results. In H. de Swart, editor, Proc. of the International Conference on Analytic Tableaux Related Methods, TABLEAUX'98, volume 1397 of LNAI, pages 44-59. Springer-Verlag, 1998.
M. Baldoni, L. Giordano, A. Martelli, and V. Patti. A Modal Programming Language for Representing Complex Actions. In A. Bonner, B. Freitag, and L. Giordano, editors, Proc. 1998 JICSLP'98 Post-Conference Workshop on Transactions and Change in Logic Databases, DYNAMICS'98, pages 1-15, Manchester, UK, June 1998.
M. Baldoni, L. Giordano, and A. Martelli. On Interaction Axioms in Multimodal Logics: a Prefixed Tableau Calculus. In D. Basin and L. Vigano`, editors, Proc. of the First International Workshop on Labelled Deduction, LD'98, Freiburg, Germany, pp. 1-15, 1998.
M. Baldoni, L. Giordano, and A. Martelli. A Modal Extention of Logic Programming: Modularity, Beliefs and Hypothetical Reasoning. Journal of Logic and Computation, 8(5):597-635, 1998.
M. Baldoni, C. Baroglio, and D. Cavagnino.XFF: a simple method to eXtract Fractal Featuresfor 2D object recognition.In A. Amin, D. Dori, P. Pudil, and H. Freeman, editors,Adavances in Pattern Recognition, volume 1451 of LNCS, pages 382-389.Springer-Verlag, 1998.
M. Baldoni, C. Baroglio, D. Cavagnino, and L. Egidi.Learning to Classify Images by means of Iterated Function Systems.In M. M. Novak, editor, Fractals and Beyond: Complexities in the Sciences, Proc. of the 5th International Multidisciplinary Conference, FRACTAL'98, pages 173-182. World Scientific, 1998.
M. Baldoni, C. Baroglio, D. Cavagnino, and L. Saitta. IFS-based feature extraction for learning to classify objects. In R. Cucchiara and M. Piccardi, editors, Proc. of the Workshop: Artificial Intelligence and Pattern Recognition Techniques for Computer Vision, IAPRVA'98, pages 9-14, Ferrara, Italy, 1998.
M. Baldoni, C. Baroglio, D. Cavagnino, and L. Saitta. Towards Automatic Fractal Feature Extraction for Image Recognition. In H. Liu and H. Motoda, editors, Feature Extraction, Construction and Selection: a Data Mining Perspective, pages 357-373. Kluwer Academic Publisher, 1998.
P.A.Bonatti, N. Olivetti. A Sequent Calculus for Circumscription, Proc. of CSL'97, LNCS 1414, pp.98--114, Springer-Verlag, 1998.
P.A.Bonatti, S.Kraus, J. Salinas, V.S.Subrahmanian. Data-Security in Heterogeneous Agent Systems. In Cooperative Information Agents (Proc. of CIA-98), pp. 290-305, LNCS 1435, Springer Verlag, 1998.
Ciabattoni, D. M. Gabbay, and N. Olivetti. Cut-free proof systems for logics of weak excluded middle. Soft Computing, 2(4), pages 147-156. Special Issue of European COST 15 Action on Many-valued Logic for Computer-Science Application, 1998.
D. Gabbay and N. Olivetti. Goal-directed proof-procedures for intermediate logics. Proc. of LD'98 First International Workshop on Labeled Deduction, 1998, Freiburg.
D. M. Gabbay and N. Olivetti. Algorithmic proof methods and cut elimination for implicational logics - Part i, modal implication. Studia Logica, 61(2):237-280, 1998.
L. Giordano, V. Gliozzi, and N. Olivetti. A Conditional Logic for Belief Revision. In Proc. of the Sixth European Workshop on Logic in Artificial Intelligence, JELIA'98, volume 1489 of LNAI, pages 294-308, Dagstuhl, 1998.
L. Giordano, A. Martelli, and C. Schwind. Dealing with Concurrent Actions in Modal Action Logics. In H. Prade, editor, Proc. of the 13th European Conference on Artificial Intelligence, ECAI'98, pages 537-541, Brighton, UK, 1998. John Wiley & Sons.
L. Giordano and N. Olivetti. Combining Negation as Failure and Embedded Implications in Logic Programs. Journal of Logic Programming, 36(2):91-147, 1998.
D. Mundici and N. Olivetti. Resolution and model building in the infinite-valued calculus of Lukasiewicz. Theoretical Computer Science, (200):335-366, 1998.
