Extending Horn clause logic with implication goals

The paper deals with the problem of extending positive Horn clause logic by introducing implication in goals as a tool for programs structuring. We allow a goal G_i in a clause G₁ ∧⋯∧ G_n → A to be not only an atom but also an implication D ⊃ G (we shall it an implication goal), where D is a set of clauses and G a goal. This extension of the language allows local definitions of clauses in logic programs. In fact, an implication goal D ⊃ G can be thought of as a block (D, G), where D is the set of local clause declarations. In this paper we define a language with blocks in which, as in conventional block structured programming languages, static scope rules have been chosen for locally defined clauses. We analyse static scope rules, where a goal can refer only to clauses defined in statically surrounding blocks, and we compare this extension with other proposals in the literature. We argue, on account of both implementative and semantic considerations, that this kind of block structured language is a very natural extension of Horn clauses when used as a programming language. We show it by defining an operational, fixpoint and model-theoretic semantics which are extensions of the standard ones, and by proving their equivalence. We show that static scope rules can be obtained by interpreting → as classical and ⇒ as intuitionistic implication with respect to Herbrand interpretations.