THEORY OF MODULES FOR LOGIC PROGRAMMING.

A logical language is presented 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. That is, a goal such as 'D implies G', is satisfied by a program P if the goal G is satisfied by the larger union of the program P and the set D. If the formula D is the conjunction of a collection of universally quantified clauses, we interpret the goal 'D implies 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 certain kinds of abstract datatypes. Both a model-theory and proof-theory are presented for this logical language. The author shows how to build a possible-worlds (Kripke) model for programs by a fixed point construction and shows that the operational meaning of implication mentioned above is sound and complete for intuitionistic, but not classical, logic.