A logical analysis of modules in logic programming

We present a logical language which extends the syntax of positive Horn clauses by permitting implications in goals and in the bodies of clauses. The operational meaning of a goal which is an implication is given by the deduction theorem: a goal D ⊃ G is provable from a program P if the goal G is provable from the larger program P ∪ {D}. This paper explores the qualitative nature of this extension to logic programming. For example, if the formula D is the conjunction of universally quantified clauses, we interpret the goal D ⊃ G as a request to load the code in D prior to attempting G and then unload that code after G succeeds or fails. This extended use of implication provides a logical explanation of parametric modules, some uses of PROLOG's assert predicate, and aspects of abstract datatypes. Both a model theory and proof theory are presented for this logical language. In particular, we show how to build a Kripke-like model for programs by a fixed-point construction and show that the operational meaning of implication mentioned above is sound and complete for intuitionistic logic. We also examine a weak notion of negation which is easily implemented in this language and show how database constraints can be represented by it.