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 [a(i)] to represent agent beliefs, and a modality square 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.
