Home  Online Resources  Table of Contents

Journal of Logic and Computation, Volume 8, Issue 5, pp. 597-635: Abstract.

A modal extension of logic programming: modularity, beliefs and hypothetical reasoning

M Baldoni, L Giordano and A Martelli

Dipartimento di Informatica, Universita degli Studi di Torino, C.so Svizzera 185, I-10149 Torino, Italy. E-mail: {baldoni,laura,mrt}@di.unito.it

In this paper we present a modal extension of logic programming, which allows both multiple universal modal operators and embedded implications. We show that this extension is well suited for structuring knowledge and, more specifically, for defining module constructs within programs, for representing agents beliefs, and also for hypothetical reasoning. The language contains modalities [ai] to represent agent beliefs, and a modality [squ] which is a kind of common knowledge operator. It allows sequences of modalities to occur in front of clauses, goals and clause heads, and hypothetical implications to occur in goals and in clause bodies. We present a goal directed proof procedure for the language, and several examples of its use for defining modules are given. In particular, the language allows different proposals to be captured for module definition and composition presented in the literature. The modal logic, of which our programming language is a clausal fragment is introduced through its Kripke semantics. This has strong similarities with the possible world semantics for the (propositional) logics of knowledge and belief proposed by Halpern & Moses. A cut-free sequent calculus is also given for this logic, which proves the soundness and completeness of the goal-directed proof procedure by showing that goal directed proofs correspond to some sequent proofs.

Key words: Logic programming, modal logic, modularity, knowledge and beliefs, hypothetical reasoning


[ Oxford University Press]   [ Oxford Journals]   [ Comments & Feedback]   Copyright© Oxford University Press, 1998.