DIPARTIMENTO   DI   INFORMATICA
Università di Torino

Research Report Year 1999

Logic Programming and Automated Reasoning

  People   Research Activities   Publications   Software Products   Research Grants

People

Alberto Martelli

Full Professor Principal investigator

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 (from July 16)

baldoni(at)di.unito.it

Valentina Gliozzi

Ph. D. Student

gliozzi(at)di.unito.it

Viviana Patti

Ph. D. Student

patti(at)di.unito.it

Massimo Schenone

Ph. D. Student

schenone(at)di.unito.it

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.

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

ex 60%

Agenti Intelligenti: Interazione, ragionamento e Acquisizione di conoscenza

F. Turini (National Coordinator)

A. Martelli (Local Coordinator)

MURST

Project of National Interest (ex 40%)

Scambio culturale con ciclo di seminari con Prof. V.S. Subrahmanian - Univ. Del Maryland e Prof. S.Adali - Rensslaer Polytechnic Institute

M.L. Sapino

Università di Torino

Scambi Culturali

Activity and role in the scientific community

A. Martelli:
  • Member of the Executive Board of CINI (Consorzio Interuniversitario per la Ricerca in Informatica).

  • Member of Scientific Committee of COREP.

M. L. Sapino
  • Referee for the following international journals:
    • IEEE Transactions on Knowledge and Data Engineering

    • ACM International Journal on Multimedia Systems

  • Referee for the conference Appia-Gulp-Prode99

M. Baldoni
  • Referee for the following international conference:
    • TABLEAUX'99 - Analytic Tableaux and Related Methods

  • Referee for the following international book:
    • Labelled Deduction, Applied Logic Series of Kluwer Academic Publishers

N. Olivetti
  • Member of Programme Committee of the International Conference TABLEAUX'99 - Analytic Tableaux and Related Methods

  • International Cooperation:
    • Organization and Partecipation to the Bilateral Project with Vienna

    • Technical University on "Analytic Proof-Methods for fuzzy-logics"

  • Referee for International Conferences:
    • FCT'99 - Fundamental of Computation Theory

    • TABLEAUX'99 - Analytic Tableaux and Related Methods

  • Referee for International Journals:
    • Journal of Logic Programming

    • Journal of Logic and Computation

  • Referee for international books:
    • Labelled Deduction, Applied Logic Series of Kluwer Academic Publishers

  • One-term course (36hours) held at Vienna Technical University on Non-Classical Logics, Proof-Theory and Logic Programming

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 09, 2002