Università di Torino

Research Report Year 1997

Logic Programming and Automated Reasoning

  People   Research Activities   Publications   Software Products   Research Grants



Alberto Martelli

Full Professor    Principal investigator


Piero Bonatti

Senior Researcher


Laura Giordano

Senior Researcher


Maria Luisa Sapino

Senior Researcher


Nicola Olivetti



Matteo Baldoni

Ph. D. student


Viviana Patti

Ph. D. student




Research activity in 1997

The research activity in 1997 has mainly dealt with the following topics.


(1) Proof methods for nonclassical and non-monotonic logics.


(1a) Proof methods for nonmonotonic formalisms.


Following the line of research started in 1996, we have carried on the program of developing uniform and analytic proof-methods for the major families of nonmonotonic logics. In 1997, we have extended our approach to circumscription, which is one of the most important nonmonotonic formalisms, and we have shown that our method can polinomially simulate derivations in one of the most efficient tableaux methods which is known so far. In previous work, we successfully applied our methodology to default logic. To complete our framework, we plan to extend it to autoepistemic logic. Moreover, we have developed an extension of resolution for the skeptical stable model semantics of logic program. This method enjoys three novel features: (i) it is not necessary to consider all the rules of the program; (ii) it is goal directed if the dependency graph of the program contains no cycles with an odd number of negative edges; (iii) variables are handled through unification.


(1b) 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.


(1c) Goal directed proof procedure for non-classical and modal logics.


Part of our research has been devoted to the study of goal-directed proof procedures for non-classical and modal logics. The underlying idea is to extend the paradigm of deduction typical of logic programming to several families of non-classical logics. This research has been carried on in collaboration with Prof. D. Gabbay of the Imperial College of London. The program has been successfully applied to modal logics of strict implication. We are currently extending it to the so-called substructural logics, a family of logics which includes relevance and linear logic, and has recently gained a great interest for the possible applications in computer science.

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.


(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 (University of Marseille), a modal action theory in which persistency is achieved by using a nonmonotonic formalism which maximizes persistency assumptions. Furthermore, we have studied the clausal fragment of this action theory by defining a modal logic programming language to reason about actions, where the frame problem is tackled by means of abduction. More recently, we have defined an extension of this language, called DyLOG, which allows to define procedures to build up complex actions from elementary ones.


(3) Applications of Logic Programming to Databases.


(3a) Applications of logic programming to security in heterogeneous/federated databases.


In collaboration with Prof. V. S. Subrahmanian (University of Maryland at College Park) in the framework of the HERMES project, a formal framework for integrating heterogeneous security policies in a mandatory framework has been developed. Two provably correct algorithmic approaches to this problem have been introduced, based on logic programming and graph algorithms, respectively. The computational complexity of various relaxation methods for interoperability constraints has been studied, and algorithms have been provided for the tractable cases.

The problem of integrating heterogeneous security specifications in a discretionary, role based framework is being tackled in collaboration with Prof. Elisa Bertino (University of Milano). 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.


(3b) Applications of logic programming to heterogeneous multimedia databases.


In collaboration with Prof. V.S. Subrahmanian (University of Maryland at College Park), a formal framework for integrating heterogeneous similarity measures is being developed. A relational similarity algebra has been introduced, which provides an abstract view of the search engines, together with operators to enrich and combine the enginesÕ output. It allows the specification of queries involving different search engines, based on the similarity between certain database object features and the query objects (which can be, among other things, text, images, video/audio signals). Such queries are optimized through formal techniques based on algebraic equivalences. For this purpose, cost models are being developed.



1997 Publications

M. Baldoni, C. Baroglio, D. Cavagnino, and G. Lo Bello. Extraction of Discriminant Features from Image Fractal Encoding. In M. Lenzerini, editor, In Advances in Artificial Intelligence LNAI 1321, pages 127-138. Springer-Verlag, 1997.

M. Baldoni, L. Giordano, A. Martelli, and V. Patti. An Abductive Procedure for Reasoning about Actions in Modal Logic Programming. In J. Dix, L. M. Pereira, and T. C. Przymusinski, editors, Proc. of the 2nd International Workshop on Non-Monotonic Extentions of Logic Programming, NMELP'96, LNAI 1216, pages 132-150. Springer-Verlag, 1997.

P. A. Bonatti. Proving negative premisses. In Proc. 1997 Joint Conference on Declarative Programming, APPIA-GULP-PRODE'97, 1997.

P. A. Bonatti. Resolution for skeptical stable semantics. In Proc. Logic Programming and Non Monotonic Reasoning, LPNMR'97, LNAI 1265 , pages 185-197. Springer Verlag, 1997.

P. A. Bonatti and N. Olivetti. A sequent calculus for skeptical default logic. In Proc. TABLEAUX'97, LNAI 1227, pages 107-121. Springer Verlag, 1997.

P. A. Bonatti and N. Olivetti. A sequent calculus for circumscription. In Preliminary Proc. CSL'97, volume NS-97-1 of BRICS Notes Series, pages 95-107, Aug 1997.

P. Bonatti, M. L. Sapino, and V. S. Subrahmanian. Merging Heterogeneous Security Orderings. Journal of Computer Security, 5(1):3-29, 1997.



Research grants

Title of project

Project leader

Funding Organization

Kind of grant

Ambienti e strumenti per la gestione di informazioni temporali

A. Martelli


Coordinated Project

Programmazione logica e ragionamento non monotono

A. Martelli

Universita' di Torino

ex 60%

Rappresentazione della conoscenza e meccanismi di ragionamento

A. Martelli (National Coordinator)

P. Torasso (Local Coordinator)


ex 40%




Activity and role in the scientific community


L. Giordano:

Member of the Executive Board of GULP (Italian Association for Logic Programming).

A. Martelli:

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

A. Martelli:

Chairperson of Scientific Committee of COREP.


Oral Presentations in Congresses and Conferences


P. Bonatti:

Joint Conference on Declarative Programming, APPIA-GULP-PRODE 1997, June 16-19, Grado, Italy.

P. Bonatti:

International Conference on Logic Programming and Non-Monotonic Reasoning (LPNMR’97).

A. Martelli:

International Joint Conference on Qualitative and Quantitative Pratical Reasoning (ECSQARU/FAPR’97), June 1997, Bonn, Germany

A. Martelli

ISMIS’97, Charlotte, North Carolina, October 15-18, 1997.


L. Giordano:

DYNAMICS on Transactions and Change in Logic Databases (International Logic programming Symposium Post-Conference Workshop, ILPS’97).


M. Baldoni:

V Congresso dell’Associazione Italiana per l’Intelligenza Artificiale, AI*IA’97, Sept. 16-19, Rome, Italy.

P. Bonatti:

Joint Conference on Declarative Programming, APPIA-GULP-PRODE 1997, June 16-19, Grado, Italy.

P. Bonatti:

International Conference on Logic Programming and Non-Monotonic Reasoning (LPNMR’97), July 28-31, Daghstul, Germany.

P. Bonatti:

Annual Conference of the European Association for Computer Science Logic (CSL’97), Aug. 23-29, Aarhus, Denmark.

N. Olivetti:

International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX’97), May, Pont-à-Mousson, France.



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: May 17, 2018