A key property in the definition of logic programming languages is the completeness of goal-directed proofs. This concept
originated in the study of logic programming languages for intuitionistic logic in the (single-conclusioned) sequent calculus
LJ, but has subsequently been adapted to multiple-conclusioned systems such as those for linear logic. Given these developments,
it seems interesting to investigate the notion of goal-directed proofs for a multiple-conclusioned sequent calculus for intuitionistic
logic, in that this is a logic for which there are both single-conclusioned and multiple-conclusioned systems (although the
latter are less well known). In this paper we show that the language obtained for the multiple-conclusioned system differs
from that for the single-conclusioned case, show how hereditary Harrop formulae can be recovered, and investigate contraction-free
fragments of the logic.