Structuring logic programs: a modal approach

Extensions of logic programming languages with structuring constructs have been extensively studied in the last years. A particularly clean approach consists in allowing implication goals to occur in goals and in clause bodies. Implication goals are implications of the form D ⇒ G, where D is a set of clauses and G is a goal. The clauses in D are intended to be local to G, as they can be used only in the proof of G. So implication goals can be regarded as blocks of conventional programming languages and such an extension provides different kinds of block structured languages according to the visibility rules chosen for the local clauses. The choices are mainly two: either lexical (static) visibility rules or dynamic visibility rules. A further distinction can be made between closed and open blocks. In this paper we aim at showing that modal logic provides a unifying framework in which different logical languages with blocks and modules can be expressed. We show this by interpreting the different block languages within modal logic S4. Moreover, we will consider different kinds of modules that can be defined from blocks by introducing some syntactic sugar and compare them to other proposals in the literature.