The purpose of this paper is to present a Gentzen style formulation for the fragment of intuitionistic propositional logic having only conjunction and implication, capturing the spirit of Gabbay's goal directed theorem prover for this logic [1], later modified into N-Prolog (cf.[2]), which, however, does not need loop checking.