A MODAL RECONSTRUCTION OF BLOCKS AND MODULES IN LOGIC PROGRAMMING

In this paper we aim at giving a reconstruction of the language with blocks defined in [6,8] by interpreting it within modal logic S4. The language is an extension of Horn clause logic obtained by allowing hypothetical implications D = > G (where G is a goal and D is a set of clauses local to G) both in goals and in clause bodies. This language is syntactically similar to the ones proposed in [5] and [11], but it has different visibility rules for local clauses, mainly static (or lexical) visibility rules as in conventional block structured programming languages. The language in [5] and [11] has a straightforward modal characterization, since it has been proved sound and complete w.r.t. intuitionistic logic, which can be interpreted within S4 modal logic. We will show that our language with static blocks can also be interpreted within modal logic S4 in a simple way and, therefore, S4 modal logic can be regarded as the unifying framework in which different languages with blocks can be expressed. This makes quite easy the task of integrating the different kind of blocks within a single language. Finally we will show that modal logics (more precisely multimodal logics) are also well suited for supporting the notion of module.